费马大定理的机器检查证明开源：AI 辅助数学首次覆盖完整经典难题

费马大定理是人类数学史上最著名的猜想之一。1994 年，安德鲁·怀尔斯在剑桥给出证明，轰动一时；之后三十年，数学家一直想把这份证明搬进形式化系统，让计算机逐行验证。最近，Anthropic 把一件酝酿中的工作正式推到台前：基于 Lean 4 与 Mathlib 的费马大定理完整机器检查证明，并以 Apache 2.0 协议开源。

简单说，这是一份能被 Lean 4 检查器“逐行打勾”的证明文本。它沿着 Frey、Serre、Ribet、Wiles 与 Taylor–Wilkes 的论证路线，把谷山–志村猜想与费马大定理之间的桥梁完整重建，并补齐到机器可验证的水准。

这件事的特殊性在于“完整”。过去几年，AI 与形式化方法社区已经拿过 IMO、Putnam 等赛题的若干证明片段做实验，但费马大定理这种横跨数论、几何、模形式与代数几何的整链条问题，从未真正被机器端到端验证过。

为什么是 Anthropic

Anthropic 一向把“长链推理 + 形式化验证”当成模型训练的核心测试场。从早期与数学家合作的形式化项目，到如今把费马大定理搬上 Lean，这家公司明显想抢下一块旗子：让外界把 Anthropic 与“可验证的硬核推理”绑在一起，而不是只把它看作消费级聊天产品的供应商。

开源协议是 Apache 2.0，意味着任何人都可以下载、改写、商用。这条线与多数高校内部的形式化项目不同，后者往往停留在 GitLab 私有仓库或论文附件里，外人很难二次开发。这次把整个仓库摆出来，对 Mathlib 社区是一次重要补血。

对开发者和数学工作者的实际影响

对形式化爱好者来说，最直接的红利是“省了几百万人时”。复现怀尔斯证明历来是读论文者的高山：每一处 mod p Galois 表示、每一个 Hecke 算子，都要自己在脑中展开。把证明变成 Lean 代码后，研究者可以借助编译器直接定位可疑环节。

对 AI 从业者来说，这份证明是一份罕见的、长度极长的“真值数据”。它既包含人类数学家三十年的论证骨架，又包含 Lean 的形式化胶水代码。训练新模型、做检索增强、做定理证明评测，都可以拿它当高质量样本。

对内容创作者和科普作者来说，这是一个可讲一整年的故事：AI 不会自己证明费马大定理，但能把人类已有的证明变成可执行、可审查、可拆解的程序。这种“人写思路、机查细节”的分工，可能比任何口号更能说明 AI for Math 现在到底走到了哪里。

中文用户应该看什么

第一，不必焦虑也不用神化。整份证明是 AI 辅助 + 数学家主导的成果，而不是大模型自己摸出怀尔斯思路。任何把它包装成“AI 拿下费马”的报道，都是把长链条的协作简化成了营销话术。

第二，有动手能力的读者可以尝试本地构建。仓库要求 Lean 4.33.1 与 Mathlib 的对应版本，Linux/macOS 用户通常半小时内能跑通 Windows 用户建议用 WSL，避免原生工具链的坑。

第三，关注后续配套物料。Lean 代码只是骨架，真正能讲清每一步为何成立，需要依赖同期发布的解释文档、教学视频与 Mathlib PR。把它们一并读完，才能看出这份工作的真实份量。

后续值得观察的点

短期看，Mathlib 社区是否会把这套代码合并进主线，是衡量它“活起来”还是“被束之高阁”的关键。如果只是开源仓库放着没人维护，再轰动也只是一次发布。

中期看，是否会有第二个难题被同一路线攻下。BSD 猜想、abc 猜想、Langlands 纲领中的若干局部问题，都是潜在的下一个试验场，谁先跑通，谁就能把 AI for Math 推向新阶段。

长期看，形式化证明会和 LLM 形成怎样的工作流。如果模型负责草稿、Lean 负责把关，未来数学论文的同行评审也许会从“看人”变成“看代码 + 看人”。这场变革才刚刚开始。