Claude 11天自动形式化证明费马大定理
推荐指数 75.0 NO. 011 · 2026.09.05
发布2026/09/04Score187Comments107
为什么值得看
Anthropic 发布首个经计算机完全验证的费马大定理形式化证明，由 Claude 在 Lean 语言中高度自主完成。这标志着 AI 首次独立完成顶级数学难题的形式化验证，可能改变数学研究的工作流。
编辑判断
形式化证明一直是数学界的瓶颈：Wiles 1995年的原始证明有数百页，人类专家花了数年才消化，而 Lean 社区此前尝试形式化 FLT 估计需要数十人年。Claude 这次的核心突破不是"会证定理"，而是自主规划并执行一个需要 200+ 引理、跨越代数几何和数论多个分支的复杂工程。
这对 AI 从业者的直接启示是：长程自主任务规划能力正在从 coding agent 向科研 agent 跃迁。如果你在做 AI for Science 或自动化研究，Lean/MetaMath 这类形式化语言正在成为新的"执行层"，值得投入学习。形式化验证赛道（如验证智能合约、芯片设计）可能会率先出现商业化落地。
社区反馈
正面 107 条评论
核心争论：AI形式化证明的效率与成本颠覆传统数学研究模式，但Lean语言可读性存疑
Impressive! Buzzard's group[1] got scooped. [1] https://github.com/ImperialCollegeLondon/FLT
Seems to have taken it in good spirit: > We shared the resulting proof with Kevin Buzzard, who said: > > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along t
I suggest also reading Kevin Buzzard's blog post on this as well which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment and what it means but also doesn't mean.