随着大语言模型在内容创作、代码生成与科学问答等领域掀起巨大变革浪潮，以严谨逻辑与精密结构著称的数学领域也迎来了深刻的转型契机。
当前，数学理论的复杂性不断提升，许多重要定理的证明规模已远超传统人工审阅的能力边界。动辄数百页的证明不仅挑战了同行评审的极限，更暴露出人工验证过程的缓慢与脆弱性。针对这一困境，形式化数学方法开始成为重要的解决路径。这一方法通过将数学命题严格表达为形式逻辑语言，并借助计算机进行自动化验证，有效地提升了定理证明的准确性和可靠性。
在形式化数学日益成为趋势的背景下，来自爱丁堡大学的博士研究生辛华剑自2022年起致力于将大语言模型技术与形式化数学方法结合，曾分别在DeepSeek和字节跳动Seed团队进行相关研究。
2025年5月9日，辛华剑在由剑桥中国AI协会、锦秋基金、清华大学学生通用人工智能协会、清华大学学生创业协会联合举办的主题分享会上，以《大语言模型时代的形式化数学革命》为题，详细阐述了形式化数学的历史演进、现状挑战以及未来发展方向。
他认为：
数学研究面临传统人工验证瓶颈，形式化数学成为有效解决途径。
LLM与形式化数学的结合大幅降低验证成本，推动数学的发展。
从传统的Theorem Prover向自主化的Proof Engineering Agent转型，是形式化数学未来的必然趋势。
自动化证明工程基准（APE-Bench）为形式化数学的长期演进提供实际评测工具。
以下内容为此次报告的整理与深化，经由分享人本人审阅补充。
引言
当大语言模型（LLM）以空前规模席卷内容创作与科学研究等领域之际，数学研究领域也正经历一场前所未有的范式变革。随着现代数学理论日趋复杂，许多关键性定理的证明已远远超出传统同行评审与人工验证的能力范畴。形式化数学，这种以严格逻辑和计算机辅助证明为核心的方法，开始展现出巨大的潜力，为解决数学领域验证难题提供了一条切实可行的路径。
面对规模巨大且逻辑严密的数学证明，单纯依靠人类专家进行审阅已显得力不从心。越来越多的数学成果证明动辄数百页，其验证周期漫长且错误风险高企，人类直觉与经验式方法的局限性日益凸显。由此，形式化数学范式逐渐兴起，以严格的公理系统和逻辑语言表达数学内容，并借助计算机系统进行推理验证。这种方法不仅能够显著提升验证的可靠性，也逐步成为推动数学研究持续发展的重要引擎。
一、生成式智能的挑战与形式化数学的机遇
近年来，大语言模型凭借出色的推理与生成能力，在数学证明生成与代码开发等智力密集型领域中迅速达到甚至超越了人类专家的表现。然而，LLM广泛存在的“幻觉”问题，即模型可能生成看似合理但存在隐藏逻辑错误或事实性缺陷的内容，严重限制了人们对生成内容的信任。这种问题在逻辑严密性要求极高的数学研究领域尤为明显：未经严格验证的生成内容不仅难以直接使用，更会显著降低研究成果的可靠性。
数学证明的审稿与验证一直是制约数学成果传播效率的重要瓶颈。一些经典案例，如黑尔斯（Thomas Hales）提出的开普勒猜想证明，其最初发表时长达300页，即使经过多年专家反复审阅，仍无法彻底消除对其正确性的怀疑。这类问题在现代数学界屡见不鲜，说明依靠传统人工验证方式的数学审稿流程已逐渐达到其能力极限，迫切需要一种更严格、更可靠的替代方法。
形式化定理证明方法正是在这种背景下展现出其独特的优势。通过将数学证明转化为严格的形式化语言，借助计算机工具进行自动或半自动化的推理验证，可以有效解决传统方法难以克服的逻辑盲点，提升证明的可靠性和验证效率。实践表明，这种严格的机器验证方法不仅解决了人力审阅无法攻克的难题，更为数学研究的长期演进提供了坚实的逻辑基础。
二、形式化定理证明及其核心应用
形式化定理证明是一种基于公理系统和逻辑推理规则的验证方法，通过将数学陈述完全表达为计算机可验证的形式化语言，并使用定理证明工具（如Lean、Coq、Isabelle/HOL）进行推理验证。这种方法无需依赖经验判断或穷举试验，能够为数学理论提供高度确定性的验证结果。
在数学领域，形式化方法的成功应用已有多个典型案例，彰显了其独特的价值：
Flyspeck项目：该项目使用Isabelle/HOL和HOL Light证明助手，彻底形式化验证了黑尔斯提出的开普勒猜想证明。原本依靠传统人工方法无法彻底确认正确性的证明，经由严格的机器验证彻底消除了所有疑虑，成为形式化数学历史上的标志性成果。
液体张量实验（Liquid Tensor Experiment）：针对舒尔茨与克劳森提出的凝聚态数学关键技术引理，学界利用Lean证明工具迅速完成了形式化验证。这不仅消除了对该理论正确性的质疑，也极大地推动了理论的后续发展与推广。
PFR猜想众包验证：由陶哲轩领导的多项式弗莱曼-鲁沙猜想验证项目，通过Lean 4工具与社区众包方式，在极短的时间内高效地完成了形式化证明的子任务。这种模式充分展示了形式化定理证明降低大规模数学协作门槛的潜力。
形式化定理证明的强大之处不仅在于验证单个复杂证明，更在于它所具备的通用性与可扩展性。无论是数学领域的理论证明，还是软件工程的代码验证，形式化方法均可在逻辑层面确保实现与规格之间的高度一致性，突破了传统方法依靠经验和直觉验证的局限，正逐步成为跨领域验证的坚实底座。
三、LLM 驱动的形式化数学最新进展
随着大语言模型技术的快速进步，形式化定理证明领域也展现出显著的发展潜力。当前先进的LLM，特别是AlphaProof和DeepSeek-Prover V2，已在竞赛级的数学问题解决中取得卓越表现。例如，AlphaProof模型凭借强化学习技术，在国际数学奥林匹克题目的形式化证明任务中表现出色，达到了银牌级别的水平；而DeepSeek-Prover V2在标准化的miniF2F数学基准中更是达到了近90%的成功率，远超此前同类系统的表现。
更重要的是，当前的研究正在逐步从单纯的证明生成转向长期的知识积累与理论体系构建。例如，LEGO-Prover项目利用LLM自动化地识别并生成可复用的数学知识单元，逐步构建起易于维护的数学知识库。这标志着形式化数学正从单一问题求解，迈向长期的库级理论构建与管理阶段。
与此同时，部分前沿研究也开始探索LLM主动提出数学猜想、发现抽象结构的潜力，这种探索使得形式化数学逐渐具备更高层次的创造性能力。尽管这一方向尚处于初期阶段，但它清晰地指向了未来形式化数学与生成式智能结合的巨大空间。
四、从Theorem Prover到Proof Engineering Agent
虽然形式化定理证明方法在数学和软件领域已有诸多成功案例，但其大规模推广仍面临人工成本高、协作效率低、长期维护困难等现实挑战。例如，数学领域的Flyspeck项目耗费数十人年的工作量，而软件领域的seL4项目同样历经多年才完成完整验证。这种模式难以适应快速变化的实际需求，亟需进行范式转型。
下一代的形式化工具需要从当前静态的“Theorem Prover”向具备自我规划、自我修复和自我知识积累能力的“Proof Engineering Agent”转型。这种自主Agent模式可显著降低人力成本，提高长期维护效率，并更有效地支持大规模跨模块协作与动态知识管理。
为推动这种转型，建立新的自动化评测基准成为必然需求。APE-Bench便是在此背景下诞生的，以真实的Proof Engineering需求为基础，评估和推动语言模型在长期动态维护场景下的表现。
五、APE-Bench：自动化证明工程基准
APE-Bench的设计初衷是填补当前形式化数学领域评测工具的空白，将评测从单一的孤立定理证明拓展到长期维护、跨文件协作等实际工程化任务。具体而言，APE-Bench采用真实数学库（如Mathlib4）中的历史修改记录，通过明确的自然语言指令和Lean代码修改任务，真实再现实际的Proof Engineering场景。
基准的实施分为三个阶段：
第一阶段（APE-Bench I）聚焦单文件范围内的局部修改任务。
第二阶段（APE-Bench II）扩展到跨文件、多模块的一致性维护。
第三阶段（APE-Bench III）则实现完全自主的Agent模式，包括自主规划、问题修复与知识积累。
通过精确的编译验证与语义评估双重机制，APE-Bench不仅确保了评测的准确性，也推动了语言模型向真正智能化Proof Engineering Agent转型，进而支持形式化数学的长期动态演化与规模化应用。
六、影响与未来展望：迈向Certified AI
LLM与形式化方法的结合，将为数学研究与相关工业应用带来高效、可信且可持续的变革。首先，在数学领域，通过自动化形式化工具，证明验证效率将显著提升，研究人员得以更多关注理论创新和概念探索，推动数学知识的快速演进。
其次，在工业领域，以APE-Bench为代表的自动化Proof Engineering方法有望推动形式化验证的广泛普及。例如，在高安全要求的软件系统（如操作系统内核、编译器、智能合约等）中，LLM辅助形式化验证能极大提升系统的安全性与可靠性。
长远来看，这种形式化验证与动态学习机制的结合将催生出新型的生成式智能——Certified AI。这种经过严格验证的智能系统将具备更高的可信性与可解释性，成为人类知识生产和决策制定的可靠伙伴。
通过形式化数学与LLM融合，我们正站在知识生产新范式的起点。从Theorem Prover到Proof Engineering Agent的转型，不仅将提升数学和软件领域的验证效率，更有望彻底重塑知识生产方式。展望未来，一个高效、可信与普惠的智能时代即将到来，人类知识探索的步伐将因此加速迈进。
