震惊！清华学子用 Claude 证明费马大定理

luyuanhong

震惊！清华学子用 Claude 证明费马大定理

原创  梓若  梓若 AI  2026 年 9 月 6 日 11:41  湖南

清华学生用 Claude 用 11 天“证明”费马大定理：AI 开始写数学的“单元测试”

费马大定理又上了热搜，但这次的主角不是某位独立研究数年的数学家，而是 Claude 。

据 X 上多个相关帐号转发的消息，一支由清华大学“姚班”校友彭天翼带领的团队，利用 Anthropic 的 Claude 大模型，在 11 天内完成了费马大定理的端到端形式化证明。传出的数据包括：生成约 1300 万行 Lean 代码，并由计算机验证了约 2.95 万条定理。



这里最容易被误解的词是“证明”。费马大定理并不是今天才被发现，英国数学家安德鲁·韦尔斯在 1994 年完成了它的严格证明。这次的突破，更准确地说，是把人类已经拥有的证明重新编写成 Lean 可读、可检查、可复现的形式化证明。

可以把它理解成：AI 在给数学写“单元测试”。传统证明依赖数学家逐行阅读论证；形式化证明则要把每一个定义、引理和推导都交给计算机检查。如果代码中有一步不成立，验证就会停下来。

这也解释了为什么这项工作会被称为“规模最大的自动形式化尝试”之一。它的价值不在于让 AI 替代数学家，而在于把极其复杂的数学知识变成机器能反复执行的工程。对研究者来说，这可以减少检查长证明的时间；对 AI 来说，也意味着它要从“会说”走向“每一步都能被验证”。

当然，“11 天”和“1300 万行代码”仍然需要更多原始论文、代码仓库和实验记录来完整核对。但这个方向已经清晰：未来的 AI 数学助手，不仅要给出结论，还要交出一份计算机能逐条验收的证明。



梓若 AI