# Claude 用 11 天完成费马大定理的 Lean 形式化证明

- 来源：Rohan Paul (@rohanpaul_ai)
- 发布时间：2026-09-05 04:00
- AIHOT 分数：74
- AIHOT 链接：https://aihot.virxact.com/items/cmtne1zcw0553rog14z85fjto
- 原文链接：https://x.com/rohanpaul_ai/status/2095965328669053054

## AI 摘要

Anthropic 宣布 Claude 完成费马大定理的首个完整机器验证证明，Claude 在 11 天内以多个智能体将基于 Wiles 的证明转化为 Lean 代码。

## 正文

Another serious win for AI in mathematics: Claude formalized Fermat’s Last Theorem in 11 days.

AI may now finally be able to automate the extremely labor-intensive job of turning advanced human mathematics into proofs that software can check line by line.

The process took 11 days despite expectations that formalizing Fermat's Last Theorem would take years, producing 13 million lines of Lean and 29,500 intermediate theorems used in the final proof.

dozens of Claude agents took the existing Wiles-based proof and converted all the missing logical details into Lean code that a computer could check.

and Lean successfully verified the finished proof.

So now AI can automate an enormous amount of the painstaking work required to turn advanced human mathematics into machine-checkable mathematics.

### 引用推文

> Anthropic：Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants li...