费马大定理的机器检查证明，不是预告，是结果。Anthropic 直接放出了一个 GitHub 仓库，里面装着基于 Lean 4.33.1 和 Mathlib 的完整形式化证明——不是某个引理，不是某段关键步骤，而是从怀尔斯到 Taylor-Wiles 的整条论证链，全部被搬进了机器能逐行检查的世界。Apache 2.0 许可，任何人都能拉下来看。换句话说，那个困扰数学家三百多年的尾巴，终于被 LaTeX 之外的另一种语言彻底收编了。
那个曾被认为无法验证的证明，如今被拆给了编译器
从手算到机械验证：一个仓库里发生了什么
你打开这个仓库，首先看到的不是密密麻麻的数学公式，而是一个清晰的目录结构：形式化证明的源头文件、依赖清单、以及一套允许你离线复现的脚本。核心文件基于 Lean 语言写成，Lean 是一种交互式定理证明器，它不像数学论文那样依赖“读者应该能理解”，而是强制你给出每一步推理，直到每一个符号都经过规则检查。这个仓库里的几万行代码，对标的正是 Wiles 当年那篇长达上百页的论文——只不过把“确信”从人的共识换成了编译器的判定。
值得强调，这个证明不是另辟蹊径，而是老老实实沿着经典路线走：Frey、Serre、Ribet、Wiles 和 Taylor-Wiles。这意味着机器并没有发明新数学，它只是完成了人类数学史上最严酷的一次“审稿”——每一次化简、每一处简写、每一个“显然”，都被打回原形，补成了机器能懂的细节。对数学家来说，这种展开本身就具有极高的审视价值。
Anthropic 为什么要碰这种硬骨头
一家以 AI 模型闻名的公司，做纯数学形式化，听起来跨界，其实是一条明确的战略路径。大语言模型经常在符号推理上摔跟头，而 Lean 这种环境天然适合测试模型在严格规则下的长链条推理能力。Anthropic 选择费马大定理，等于把最难啃的推理题当成了算法试验场：如果他们能训练出能辅助构造这种规模证明的模型，那就说明模型在逻辑一致性上有了实质突破。
仓库本身没有急于宣传 AI 的角色，更多是在展示“人机协作”的成品。但有心人看得出，这种规模的形式化工程不可能单靠人类手工完成，背后一定有大量 AI 辅助的证明搜索与重构。只不过他们选择先让作品说话，而不是先把聚光灯打到模型上。
路线图：Frey、Serre、Ribet 与 Wiles 如何被装进一套逻辑骨架
反证法的尖刀：费马曲线与椭圆曲线
费马大定理的现代证明，核心是反证：假设存在非平凡解 aⁿ+bⁿ=cⁿ（n>2），那么可以构造一条半稳定椭圆曲线，也就是著名的 Frey 曲线。Serre 后来又提出模性猜想的一个特殊情形，指出这类椭圆曲线如果存在，将无法匹配任何模形式。于是问题被扭转——要证明费马大定理，先得证明所有半稳定椭圆曲线都是模的。Wiles 正是靠重振这一路线完成的突破。形式化团队需要把这条环环相扣的链条，翻译成一个依赖树：先定义椭圆曲线、模形式、Galois 表示，再证明每个桥接定理都不缺边角。
在 Lean 的数学库里，这些定义已经部分存在。Mathlib 是 Lean 生态的“数学地基”，其中有抽象代数、数论、多项式等等。但费马大定理需要的许多高级模块，比如模形式的深层性质，必须从零搭建或大幅扩展。所以这个仓库不仅是证明的堆积，也是 Mathlib 的扩展总集。
Ribet 的桥梁与模形式的深渊
Ribet 的工作在其中扮演的角色，是把 Serre 猜想里的可能性变成必然性：他证明了只要 Frey 曲线存在，就一定存在某个来自特定权层的模形式，然后这个模形式会与已知的伽罗瓦表示发生矛盾。这套“下降法”之所以困难，是因为它横跨代数数论、Galois 表示与模形式理论。而形式化之后，你会发现每一步依赖十几个前置定理。一旦一个定理的适用条件没有被精确定义，机器就立刻拒绝通过。
人类数学家依赖“心领神会”的地方，恰恰是形式化最耗时间的地方。比如“同时满足某种局部与整体条件”这类话，写在论文里，读者会自动补充细节；写在 Lean 里，你必须定义一个完整的谓词，然后证明所有局部性质能拼成整体性质。这种琐碎却被需要的劳动，正是这台机器的价值所在——它不是用智力碾压人，而是用绝不遗忘的规则死死咬住每一步。
Lean 4.33.1 与 Mathlib：语言束缚下的自由
数学语法 vs 机器语法
Lean 不是人类数学语言的镜像。你在黑板上写的漂亮公式，转化成 Lean 之后往往很啰嗦。但这是一种有益的“翻译代价”：它迫使你把模糊的概念精确化。比如说“有限群”“正规子群”“不可约表示”等等，它们不是一串名字，而是层层嵌套的结构。Lean 对类型的要求极其严格，一个差之毫厘的定义会让后续证明彻底失效。
Anthropic 这次选用 Lean 4.33.1 和对应版本的 Mathlib 作为基座，并非心血来潮。Lean 4 相比前代有更好的扩展性，Mathlib 经过多年积累，已经覆盖大量现代数学核心成果。版本锁定也很关键：机器证明对版本极其敏感，依赖项稍有变动，整个证明可能跑不通。他们的做法是提供一个可完美复现的环境——如果你照手册操作，计算机给出的结果应该与原始验证保持一致。这正是可复现性的硬定义。
为什么说这件事比证明本身更耗神
数学界早就认了：Wiles 的证明原始文本在专家手里也需要反复推敲，许多细节在后来的讲座和综述中才逐步补完。一旦进入机器证明，你就得把所有补丁全部摊开。每一个“由命题 2.3 显然可得”，可能对应 Lean 中约一百行逻辑序列。有人估算过，把一篇现代高水平论文完整形式化，成本往往是原文表达成本的十倍以上。费马大定理这种级别的论文，消耗更难以估量。
这也解释了为什么该仓库能引起大量关注：它用事实告诉大家，Lean 已经从“形式化初等数论玩具”进化到“能承载当代核心数学”的引擎。也许不是所有数学家都愿意投入这种翻译工作，但它为未来的自动化证明奠定了基础——任何需要调取费马大定理结论的下游证明，都可以把这个仓库当作可检查的假设源。
开源仓库的深层意义：可复现、可审计、可再开发
一台能离线跑完的“数学录音机”
仓库的核心价值，在于它不依赖云服务、不依赖魔法网络。只要安装 Lean 4.33.1 和相应版本的 Mathlib，一个人就可以在自己的电脑上重新跑一遍全程验证。自查脚本的存在，让“相信”变得不必要：你不会因为名气而信，而是运行后得到与仓库一致的输出。这种机制和零知识证明在哲学上有点接近——不暴露思考过程的全貌？不，它暴露了一切。任何审阅者都可以逐条查看证明的依赖项，找出某个公理意外引入的裂缝。
下一步：机器能发现新数学吗
这一步完成后，更诱人的问题浮出水面：机器能不能从这条路中推导出新的定理？假设你修改一处假设条件，机器会告诉你哪里卡住。这种“卡住”其实就是研究线索。比如将半稳定条件放松，你也许能测试更广泛的猜想版图。机器不会主动提出好问题，但它能把坏路径提前筛掉，让人少走弯路。
Anthropic 这次没有说要造出自动证明费马大定理的 AI，但任何尝试构造此类证明的人都会感受到：人机协作的边界正在后撤。过去的协作是人类写论文，机器改语法；现在协作是机器盯完整逻辑链，人类提供方向和局部引理。我们可以把这次发布视为一次里程碑，但不必把它神话成“AI 自己证明了费马大定理”。更准确的描述是：AI era 里的证明基础设施，已经能装下 20 世纪最壮丽的数学成就之一。
读完这个仓库，我心里冒出来一句话：数学证明的最终裁判，可能不再是某位权威教授，而是一串会自动报错但从不撒谎的代码。这不是数学的终结，恰恰是新形态数学史的开端——在那个世界里，每一步脚印都留下档案，每一条引理都可供检索。费马大定理的机器检查证明只是第一个重量级样本，它已经用行动宣告：秘密的证明过程将成为过去。
