Anthropic 上传基于 Lean 4 的费马大定理机器校验证明，Ethan Mollick 指出文档仍带有 Claude 文风
It is funny that the Fermat's Last Theorem proof description, short as it is, still smells so much o...
AI 导读Anthropic 在 GitHub 上传了费马大定理的 Lean 4 完整机器校验证明（https://github.com/anthropics/fermats-last-theorem），基于 Mathlib（Lean 4.33.1、Mathlib v4.33.0），论证路线为 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles。Ethan Mollick 转发并评论称，该证明的描述虽短，但 PROOF-PATH.md 中"为每一步命名并标注对应 Lean 定理"的写法仍很像 Claude 的产出。仓库标注为研究产物，不维护且不接受贡献。
另有 3 家信源报道
- Anthropic 宣布 Claude 用 11 天完成费马大定理首个端到端形式化证明IT之家·人工智能 · 9 月 5 日
- Claude 用 11 天完成费马大定理的 Lean 形式化证明Rohan Paul · 9 月 5 日
- Claude 完成 Fermat 大定理的形式化证明，生成超 1300 万行 Lean 代码Anthropic · 9 月 5 日
来源：Ethan Mollick · x.com
事件后续1
查看事件全部- Claude 完成 Fermat 大定理的形式化证明，生成超 1300 万行 Lean 代码Anthropic · 9 月 5 日