核心观点 AI在数学研究中的能力正快速提升，已能解决部分未解难题，但其“广度”与人类专家的“深度”高度互补，AI加速了证明生成与验证，却未同步提升人类的理解与消化速度，可能导致“证明消化不良”和下一代科学家培养的缺失 AI数学能力进展 - AI驱动的自主智能体在88小时内生成三维纳维-斯托克斯方程有限时间爆破问题的证明，并用Lean完成形式化验证，这是AI首次宣称攻破克雷数学研究所悬赏100万美元的“千禧年大奖难题”之一[4] - 过去四年AI数学能力从解初中数学题逐步提升至解研究生资格考试题，近期开始解决人类研究者长期未能解决的问题，如围绕单位距离问题的相关成果已被人类借鉴[35] - 在“First Proof挑战”中，用十道研究级数学题测试最新模型，表现最好的模型能解出五六道[36] - AI解题成功率与成本尚不透明，私营公司未公开投入资源，计算费用可能是十万美元或一百万美元，成功率未知[36] AI与人类能力的互补性 - 人类专家注重深度，会挑选有难度但非完全不可能的问题深挖，而AI擅长广度，能并行尝试大量问题，搜索不同领域方法，寻找被遗漏的组合[21][22] - AI可能没有先入为主的偏见，能发现专家普遍认同的错误看法，有时能找到所有人都漏掉的解法[22] - 将一千道题交给AI，即使只解出5%也是五十道题，在解题数量上已能超过人类数学家[22] - 数学界需利用AI大范围解决部分问题的新能力，与人类慢慢深挖少数深度问题的能力配合[23] AI对科学过程的冲击 - AI加速了实验、代码、证明生成的速度，但人类理解和消化知识的速度没有同步提高，导致“证明消化不良”[5][33] - AI生成的证明可能花大量篇幅解释简单事，却对最有意思的部分一笔带过，因为AI分不清哪里容易哪里难[32] - 开普勒发现行星运动定律的过程说明，科学研究需要时间消化理论，AI太快可能导致“过拟合”，构建出与现实中真正发生的事情无关的复杂模型[25][28] - 风险在于将AI用于科学时优化了错误的目标，纸面上取得惊人成果，但科学并未像以前那样真正向前推进[29] AI作为研究伙伴的局限性 - 陶哲轩预测到2026年AI可能成为数学研究中“值得信赖的合著者”，但对他本人而言，攻克核心难点的过程并未发生同等程度的改变，纸和笔仍是重要工具[6][7] - AI会犯错，有时会一味迎合用户，且目前互动更偏向单人使用，无法像人类合作者那样形成思维默契和自然流畅的对话[43] - AI有一定的上下文记忆能力，但无法像人类合作者那样持续学习或重新接上很久以前的思路[43] - 陶哲轩更常将AI用于辅助任务，如检索文献、检查证明、写代码或校对，而非真正解题过程[43] 对下一代科学家的影响 - 研究生训练过程中，AI已能处理许多训练性问题并产出论文，若用AI取代研究生，将无法培养下一代研究者[49] - 若不继续消化AI产出并整理成知识基础，整个科学共同体可能停滞，只优化现有技术能做的事，却不再发展原创性新想法[50] - 需要更公开讨论基础科学的价值，以及由人组成的研究群体探索未知的重要性，即使进展慢或方法不如AI高效[50]

核心观点 - 大语言模型与形式化数学的结合正在引发数学研究领域的范式变革，从定理证明向自主化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]