Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our proof strategy language based on a meta-tool approach. Then, we propose an AI-based approach to drastically improve proof automation for Isabelle, while identifying three major challenges we plan to address for this objective.
Isabelle/PIDE平台解决了LCF系列的证明助手是否适合作为教育工具的技术基础的问题。像HOL、Coq或Isabelle这样的系统传统上强大的逻辑基础到目前为止已经被TTY（或像著名的Proof General / Emacs接口这样的小变体）的一些不可访问的交互所抵消。因此，数学教育工具与完全正式的背景理论的基本问题，往往是否定的回答，由于现有的证明引擎偶然的弱点。“PIDE”（意为“ProverIDE”）的理念是将现有的证明器（如Isabelle）集成到一个更大的环境中，以方便最终用户和其他工具的访问。我们使用Scala将ML中的证明引擎公开给JVM世界，那里已经存在许多用户界面、编辑器框架和教育工具。这将最终导致组合数学助手，其中逻辑引擎是在后台，而不妨碍形式化方法，形式化数学，特别是数学教育的应用程序的看法。
Southwest University（西南大学）；Aarhus University（奥胡斯大学）；University of York（约克大学）；Centro de Informática, Universidade Federal de Pernambuco (UFPE)（伯南布哥联邦大学信息中心）；University of Lancaster（兰卡斯特大学）
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
State Key Laboratory of Novel Software Technology, Nanjing University, China（南京大学新型软件技术国家重点实验室）；School of Computer Science, Nanjing University, China（南京大学计算机科学学院）；Department of Computer Science, ETH Zurich, Switzerland（苏黎世联邦理工学院计算机科学系）；School of Computing and Mathematical Sciences, Birkbeck, University of London, UK（伦敦大学伯克贝克学院计算与数学科学学院）
Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
Department of Computer Science, University of Sheffield, United Kingdom（英国谢菲尔德大学计算机科学系）；Department of Informatics, King’s College London, United Kingdom（英国伦敦国王学院信息学院）；Department of Computer Science, University of Copenhagen, Denmark（丹麦哥本哈根大学计算机科学系）
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
College of Computer Science and Technology Zhejiang University（浙江大学计算机科学与技术学院）；Siebel Center for Computer Science University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校计算机科学中心）
Munkres' General Topology Autoformalized in Isabelle/HOL
Independent（独立研究者）；Aalborg University（奥尔堡大学）；University of Melbourne（墨尔本大学）；AI4REASON and University of Gothenburg / Chalmers University（AI4REASON 和哥德堡大学 / 查尔姆斯理工大学）
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
Shenzhen Campus of Sun Yat-sen University（中山大学深圳校区）；City Univeristy of Hong Kong（香港城市大学）；Sun Yat-sen University（中山大学）；The University of Hong Kong（香港大学）；Huawei Noah’s Ark Lab（华为诺亚方舟实验室）；MBZUAI（Mohamed bin Zayed 人工智能大学）；DarkMatter AI Research（DarkMatter AI 研究院）
