目前结论
Anthropic宣布，其AI系统Claude使用Lean证明助手帮助完成了费马大定理的形式化证明。该项目基于Darmon–Diamond–Taylor对Wiles–Taylor–Wiles论证的阐述，涉及Langlands–Tunnell定理与Ribet水平降低定理等步骤。 这是AI辅助数学领域的里程碑，展示了Claude能够协助将一项著名而艰深的人类证明转化为机器可检查的形式证明。Anthropic认为，这种速度意味着现在可以对数学的很大一部分进行形式化，从而有助于发现既有证明中的错误，并减轻审稿人的负担。 此次形式化并未采用数学家Kevin Buzzard正在形式化的现代证明，而是通过Darmon–Diamond–Taylor路线重现了最初的Wiles–Taylor–Wiles突破。在此过程中，代码库还发展了Fontaine理论，并展开了Mazur关于Eisenstein理想的研究，以处理Frey曲线。
进展时间线
1 次实质进展- #01
Anthropic的Claude协助在Lean中形式化费马大定理
Anthropic宣布，其AI系统Claude使用Lean证明助手帮助完成了费马大定理的形式化证明。该项目基于Darmon–Diamond–Taylor对Wiles–Taylor–Wiles论证的阐述，涉及Langlands–Tunnell定理与Ribet水平降低定理等步骤。 这是AI辅助数学领域的里程碑，展示了Claude能够协助将一项著名而艰深的人类证明转化为机器可检查的形式证明。Anthropic认为，这种速度意味着现在可以对数学的很大一部分进行形式化，从而有助于发现既有证明中的错误，并减轻审稿人的负担。 此次形式化并未采用数学家Kevin Buzzard正在形式化的现代证明，而是通过Darmon–Diamond–Taylor路线重现了最初的Wiles–Taylor–Wiles突破。在此过程中，代码库还发展了Fontaine理论，并展开了Mazur关于Eisenstein理想的研究，以处理Frey曲线。
来源依据：jlebar