Claude 自主工作 11 天,产出首个费马大定理机器验证证明
scaling01 · x · 2026-09-05
Anthropic 官方发布:Claude 在 11 天内基本自主工作,产出了费马大定理(FLT)的首个端到端、计算机验证的完整证明。
背景
- FLT 于 1637 年由费马提出,1995 年 Andrew Wiles 的证明长达 129 页,需数月人工验证。
- 此后数学界推进「形式化」:2024 年伦敦帝国理工 Kevin Buzzard 发起多年的 Lean 社区工程。
本次工作
- 由 Anthropic 研究员 Tianyi Peng(其哥伦比亚大学团队研究 AI 形式化)发起,测试 Claude 能否推进 FLT 形式化。
- 结果远超预期:11 天、大部分自主运行,Claude 写下约 1300 万行 Lean 代码,证明了 29,500 个中间定理,完成端到端机器可查证明。
- Kevin Buzzard 评价其为「非凡的自动形式化成就」。
Anthropic 同时探讨了对研究数学的意义:AI 或能把形式化从数年社区工程压缩到天级任务。
所属事件:Claude 完成 1300 万行 Lean 代码形式化证明费马大定理(20 条相关)→
「漫话AGI」频道最新
- 学者交锋:agent 洪水或「无法防控」,互联网防线存疑 — sethlazar · 2026-09-05
- 研究者推测今夏多起模型安全事件同源于 AstraBase 底座 — gleech · 2026-09-05
- Anthropic 自动化 AI 研发进程加速,完整自动化或仅剩两年 — ResultBackground2450 · 2026-09-05
- 教模型敬畏造物主：GPT-5.6 一段关于能力与责任的回应走红 — Ronald-Obvious · 2026-09-05
- Seth Lazar 长文反驳「AI 夺权」论：应看能力外推而非单次攻击 — sethlazar · 2026-09-05
- 「AI 将崩溃」论战续篇:Soda 撰文回应称 AI 长期无虞 — wordgrammer · 2026-09-05