Anthropic公布Claude在十一天内完成费马大定理的端到端形式化，用Lean写出约一千三百万行代码，并证明大量中间定理。这里的新意不是重新发现Wiles的数学证明，而是把复杂的人类证明转成证明助手可以逐步检查的形式。项目显示AI能显著降低形式化成本，也暴露了多Agent容易丢失项目状态的问题。
一、形式化与普通证明的区别
数学论文会省略专家认为显然的步骤，Lean要求每个逻辑连接都明确，并只接受已定义对象和规则。最终通过检查意味着机器确认推导符合公理和库，而不是语言模型觉得“看起来正确”。这使形式化成为验证AI数学结果的重要工具。
二、为何需要大量中间定理
费马大定理依赖代数、几何、数论和分析等复杂基础。Agent不能直接从结论跳到证明，必须构建数万条可复用结果。巨大的代码量反映了形式化细节，不等于人类解释更清楚。最终仍需要面向数学家的可读说明。
三、最初协作为什么失败
多个Agent早期很快失去项目全局状态，重复工作并难以利用他人成果。项目后来使用Prove2Me维护定理有向无环图，把声明与证明分开，并为每个节点提供自然语言描述。结构化依赖让Agent知道下一步做什么，也能并行而不互相覆盖。
四、证明助手提供确定性验收
生成式模型可能幻觉，但Lean内核用确定规则检查证明项。只要信任内核、公理和声明，错误步骤不能蒙混通过。项目还需确认形式化的定理陈述与数学界认定的费马大定理一致，否则可能严谨证明了一个偏离目标的命题。
五、成本与规模仍然巨大
项目消耗数十亿输出Token和大量多Agent运行资源，不能直接推断普通数学题都值得这样处理。应把形式化优先用于影响大、复核困难或可长期复用的成果。随着工具和库完善，后续项目成本可能下降，但仍要透明报告资源。
六、对科研流程的影响
未来论文可能同时提交人类可读证明与机器可检查版本，AI帮助补齐细节、复用库和定位缺口。审稿人可把时间更多用于理解新思想，而不是手工检查每条推导。但形式化不会判断研究问题是否重要，也不能替代数学直觉和解释。
七、企业开发的启示
这项工作再次说明复杂Agent任务需要依赖图、单一事实源、独立验证器和明确完成条件。软件工程也可把大目标拆成可测试节点，用编译器和测试而不是模型自评验收。AI越能生成大量产物，确定性验证就越重要。
八、仍需保留人类可读解释
机器证明可以确认逻辑成立，却不自动告诉读者关键思想、为什么采用某条路径以及结果有何意义。科研交付应同时提供形式化文件、依赖说明和面向人的论文。可检查性与可理解性相互补充，任何一方都不应被另一方取代。
