核心观点 - 大语言模型与形式化数学的结合正在引发数学研究领域的范式变革，从定理证明向自主化Proof Engineering Agent转型是必然趋势 [2][23][42] 形式化数学的挑战与机遇 - 现代数学证明规模远超传统人工审阅能力，动辄数百页的证明挑战同行评审极限，暴露人工验证的缓慢与脆弱性 [20][28] - 黑尔斯开普勒猜想证明长达300页，即使多年专家反复审阅仍无法彻底消除怀疑 [28] - LLM的“幻觉”问题在数学领域尤为严重，未经严格验证的生成内容会降低研究成果可靠性 [28] - 形式化数学通过严格逻辑语言和计算机辅助验证，能有效解决传统方法难以克服的逻辑盲点 [29][30] 形式化定理证明的核心应用 - Flyspeck项目使用Isabelle/HOL和HOL Light彻底形式化验证了开普勒猜想，消除了所有疑虑 [31][32] - 液体张量实验利用Lean证明工具迅速完成凝聚态数学关键技术引理的形式化验证 [33] - PFR猜想众包验证通过Lean 4工具与社区众包方式高效完成形式化证明子任务 [34] - 形式化方法在数学理论证明和软件工程代码验证中均可确保实现与规格的高度一致性 [34] LLM驱动的形式化数学最新进展 - AlphaProof模型在国际数学奥林匹克题目形式化证明中达到银牌级别水平 [35] - DeepSeek-Prover V2在miniF2F数学基准中达到近90%成功率 [35] - LEGO-Prover项目利用LLM自动化识别并生成可复用的数学知识单元 [35] - 前沿研究开始探索LLM主动提出数学猜想、发现抽象结构的潜力 [2][35] - 2026年1月GPT-5.2 Pro和Aristotle用Lean证明了埃尔德什第728号问题，为首个AI系统自主解决的埃尔德什问题 [13] - 2026年5月AlphaProof Nexus在353个未解埃尔德什问题中解决9个，并证明492个OEIS猜想中的44个 [13] - 2026年5月OpenAI通用推理模型推翻平面单位距离问题核心猜想 [13] - 2026年7月Claude Fable 5找到雅可比猜想三维情况反例 [13] - 2026年8月Claude将黎曼猜想临界线上零点比例下界从41.6%提高到67.2% [13] - 2026年9月Claude用11天完成费马大定理全程Lean形式化，写出约1300万行形式化代码 [14] - 2026年9月OpenAI内部模型调度约一万个并行智能体，88小时内形成纳维-斯托克斯方程分析证明，随后由GPT-6 Astra在7小时完成Lean形式化与验证 [10] 从Theorem Prover到Proof Engineering Agent - 当前形式化方法面临人工成本高、协作效率低、长期维护困难等挑战 [36] - Flyspeck项目耗费数十人年工作量，seL4项目历经多年才完成完整验证 [36] - 下一代形式化工具需向具备自我规划、自我修复和自我知识积累能力的Proof Engineering Agent转型 [23][36] - APE-Bench以真实Proof Engineering需求为基础，评估语言模型在长期动态维护场景下的表现 [36][37] - APE-Bench采用Mathlib4历史修改记录，通过自然语言指令和Lean代码修改任务再现实际场景 [37] - APE-Bench分三阶段实施：单文件局部修改、跨文件多模块一致性维护、完全自主Agent模式 [38][39] 未来展望 - LLM与形式化方法结合将提升数学证明验证效率，使研究人员更多关注理论创新 [42] - APE-Bench有望推动形式化验证在操作系统内核、编译器、智能合约等高安全要求软件中的普及 [42] - 形式化验证与动态学习机制结合将催生Certified AI，具备更高可信性与可解释性 [42] - 从Theorem Prover到Proof Engineering Agent的转型将彻底重塑知识生产方式 [42]