05 / Claude 完成费马大定理的形式化
AI 科研 · 9/10 · 9 月 4 日公布 · 建议深挖
Anthropic 公布，Claude 用约 11 天完成了费马大定理的完整 Lean 形式化。费马大定理早已有了证明；这次的工作是把既有数学推理翻译成代码，交给 Lean 逐步检查。
多个 Agent 分工处理概念和中间定理，再复用已完成的结果，推进更复杂的证明。模型负责写，工具负责查，证明中的依赖关系决定了工作怎样拆开。这让一个规模很大的数学工程能够持续推进。
它的价值在于减轻核验负担。AI 写出一段看似严谨的推导，人仍需要逐步审查；形式化可以把其中一部分工作交给机器。若这种能力继续成熟，研究者就有机会更快检查既有文献，也更容易核验新生成的数学结果。
机器检查通过，仍需要确认定理表述与原数学问题一致。这项工作依赖既有数学成果和大量计算资源，也包含人的高层指导。11 天不能直接换算成普通用户处理同类问题的时间与成本。
*Juju Radar 绘制的概念示意，非官方流程图。*