Anthropic 发布费马大定理 Lean 4 机器检查完整证明并开源

350年前困扰人类的难题，今天被AI翻开了新一页。

1637年，费马在书边空白处写下那句著名的话："我想到了一个绝妙的证明，可惜这里空白太小写不下。"此后三百多年，无数数学家为它熬白了头，直到1995年怀尔斯给出人类证明版。现在，Anthropic 把这段证明用机器语言重新走了一遍——不是帮忙搭把手，是完整地、被机器逐行检查过地走了一遍，并且开源给所有人。

什么叫"机器检查过"

数学证明最怕什么？怕错。一个论证几十页，中间某一步藏了个没人发现的隐含假设，整套结论就悬在半空。Lean 4 这种证明助手，就像一个永远不打瞌睡的阅卷老师：你写下的每一步推理，它都要求你补全依据，逻辑链一断立刻打回。

这次 Anthropic 发布的，是基于 Lean 4.33.1 和 Mathlib（数学库）的完整机器检查证明，遵循 Frey、Serre、Ribet、Wiles 到 Taylor-Wiles 的经典论证路线。换句话说，怀尔斯当年那份人类证明被"翻译"成了机器能验证的形式，并且每一步都过了机器这一关。

可能有人会问：怀尔斯1995年就证明过了，现在再让机器走一遍图什么？图的不是结论，而是"信任的传递"。人类证明里那些用"显然""众所周知"一笔带过的地方，机器一个都不放过。它不比人聪明，但它较真。正是这种较真，让后人敢在这块地基上继续往上盖楼，而不用担心哪一天发现底层裂了缝。

为什么开源比"证明成功"更重要

这次的关键不只是"AI参与了"，而是它以 Apache 2.0 协议开源，仓库里给了完整验证链路和自查脚本，你甚至可以离线把它跑一遍、自己复现。

这意味着什么？以前说"AI帮数学家证明了定理"，很多人半信半疑——是不是模型自己脑补的？现在不是口头宣称，而是把整个实验台交给你：脚本在这儿，环境在这儿，你怀疑就自己跑。科学精神里最硬核的那块——可复现性——这次被AI证明补上了。

我的观点：这不是替代数学家，是给数学装显微镜

我不认为这件事意味着数学家要失业。恰恰相反，它像给整个数学研究装上了一台显微镜：人类负责提猜想、找方向，机器负责盯紧每一步逻辑漏洞。费马大定理这种"纪念碑级"的定理被完整形式化，更像是一次"练兵"——让机器吃透人类最硬的一段证明，为它将来参与更前沿、还没人能走完的问题铺路。

真正的看点是：当机器能替你检查证明的那天，数学家的工作重心会从"别写错"转向"该证什么"。费马本人当年大概也想不到，自己一句书页上的留白，会逼出人类数学三百多年的接力；而现在，接力棒第一次递到了一个不睡觉、不偷懒的机器手里。

你觉得，AI帮着把老定理重新验证一遍，和AI独立证明一个人类从没碰过的新难题，哪个更让你震撼？

人工智能 科技 AI数学 人工智能