费马大定理形式化：Lean 4如何验证数学史上最难证明

引子：三个半世纪的数学传奇

费马大定理（Fermat's Last Theorem）是数学史上最著名的问题之一。1637年，法国数学家皮埃尔·德·费马在书页边缘写下那句让后世数学家魂牵梦绕的话：当整数 n > 2 时，方程 x^n + y^n = z^n 没有正整数解。他还补充说自己找到了一个绝妙的证明，只是页边太窄写不下。

这个定理的特殊之处在于它的表述极其简洁——任何学过勾股定理的中学生都能理解其含义。它本质上是说，勾股定理中 x²+y²=z² 的整数解（如经典的3,4,5或5,12,13）在指数升高到3及以上时就彻底消失了。正是这种「易于理解、难以证明」的特性，使其成为数学史上吸引业余爱好者和专业数学家最多的问题之一。

在费马提出猜想后的三百多年间，数学家们对特定指数的情形进行了逐一攻克。费马本人证明了 n=4 的情形——这也是他唯一留下完整证明的特例。欧拉在1770年左右证明了 n=3 的情形，尽管其证明中包含一个漏洞，后来被他人修补。狄利克雷和勒让德在1825年合作证明了 n=5 的情形，拉梅则证明了 n=7 的情形。19世纪中叶，库默尔引入了理想数（ideal numbers）的概念，一举证明了所有「正则素数」指数下的费马大定理。这是一个划时代的突破，不仅大幅推进了费马大定理的进展，还直接催生了代数数论中理想理论的发展——可以说费马大定理在被证明之前，就已经深刻推动了数学本身的演进。到20世纪末，借助计算机验证，费马大定理对所有小于400万的指数都已被确认成立，但一个适用于所有指数的通用证明仍需全新的数学框架。

这个「页边太窄」的传奇困扰了数学界358年。直到1994年，英国数学家安德鲁·怀尔斯（Andrew Wiles）借助现代代数几何、模形式与椭圆曲线理论，最终给出了完整证明。怀尔斯的证明并非直接攻击费马方程本身，而是绕了一条深刻而迂回的路径。他实际证明的是半稳定椭圆曲线的模性定理（即谷山-志村-韦伊猜想的一个特殊情形）。

这条逻辑链条的起点来自格哈德·弗雷（Gerhard Frey）在1985年的关键洞察。弗雷指出：假设费马方程 x^p + y^p = z^p 存在一组正整数反例 (a, b, c)，则可以构造一条椭圆曲线 y² = x(x - a^p)(x + b^p)，即后来以他名字命名的弗雷椭圆曲线（Frey curve）。这条曲线的判别式极其巨大且具有极端的算术性质，弗雷猜想它不可能是「模的」——即不可能对应任何模形式。让-皮埃尔·塞尔（Jean-Pierre Serre）将这一猜想精确化为ε-猜想，随后肯尼斯·里贝特（Kenneth Ribet）于1986年证明了它（后称里贝特定理）。这意味着整个问题被归约为一个更宏大的命题：证明所有半稳定椭圆曲线都是模的。如果模性定理成立，那么弗雷曲线就必须是模的，与里贝特定理矛盾，从而反例不存在，费马大定理成立。怀尔斯正是沿着这条路径，花了七年秘密研究，最终完成了这一关键步骤。

而如今，一个新的挑战正在展开——将这个宏大的证明用形式化证明助手 Lean 4 完整地编码和验证。

什么是Lean 4形式化项目

近期在Hacker News上引发讨论的「Fermat's Last Theorem in Lean 4」项目，由数学家凯文·巴扎德（Kevin Buzzard）领衔发起。凯文·巴扎德是伦敦帝国理工学院的数论教授，也是形式化数学运动最具影响力的布道者之一。他在2017年前后开始接触Lean，此后不遗余力地推动专业数学家拥抱形式化工具。他曾公开挑战数学界「同行评审就够了」的信念，指出现代数学论文中引用链条之长、相互依赖之深，使得任何单一审稿人都不可能完全验证一个复杂结果的正确性。他发起的前置项目——如液态张量实验（Liquid Tensor Experiment），成功将彼得·舒尔茨（Peter Scholze）一个凝聚态数学中的关键定理形式化——已经证明了这种方法的可行性，并为费马大定理的形式化积累了宝贵经验。

此次项目的目标是用计算机可验证的方式，将怀尔斯的证明（以及后续泰勒-怀尔斯等人的完善工作）逐行翻译成Lean 4能够检查的形式化语言。

为什么需要形式化

怀尔斯的证明早在1994年就被同行评审接受，为什么还要花巨大精力去做形式化？答案涉及现代数学的一个深层焦虑。

所谓形式化证明（formal proof），是将数学证明的每一个推理步骤都用严格的形式逻辑语言书写，使得计算机程序（称为证明检查器或证明助手）能够机械地验证其正确性。与人类阅读论文时可能依赖直觉、跳过「显然」步骤不同，形式化证明不允许任何模糊性——每一步都必须有明确的逻辑依据。

Lean 4正是这样一款由微软研究院的Leonardo de Moura团队开发的新一代定理证明器和编程语言。它的逻辑基础是依赖类型理论（Dependent Type Theory），具体而言是归纳构造演算（Calculus of Inductive Constructions, CIC）的一个变体。在这个框架中，命题即类型、证明即程序——这被称为Curry-Howard同构。一个数学命题被视为一个类型，而该命题的一个证明则是该类型的一个「居民」（inhabitant）。例如，命题「2+2=4」对应一个类型，而验证这个等式的计算过程就构成了一个该类型的项。依赖类型允许类型依赖于值，使得系统能够表达极其精细的规范——例如「长度为n的列表」本身就是一个依赖于自然数n的类型。Lean 4的核心证明检查器非常小（仅数千行代码），这意味着信任基础（trusted computing base）极小——即使Lean的上层系统存在bug，只要内核正确，验证结果就是可靠的。相比其前身Lean 3，Lean 4在性能、元编程能力和用户体验上都有质的飞跃，并且具备完整的通用编程能力，使其不仅是证明工具，也是一门实用的编程语言。

怀尔斯的原始证明长达上百页，依赖于大量前置理论和其他数学家的成果。真正能够完整理解并审查这个证明的专家在全世界屈指可数。事实上，怀尔斯最初提交的证明包含一个漏洞，经过一年多努力（与理查德·泰勒合作）才最终补全。

形式化的意义在于：一旦证明被Lean 4完整验证，就相当于机器逐条检查了每一个逻辑推理步骤，不存在任何人为疏漏的可能。这为数学真理提供了前所未有的确定性保障。

挑战的规模与难度

数学珠穆朗玛峰般的攀登

将费马大定理形式化的难度，远远超过大多数已完成的形式化项目。此前Lean社区已经形式化了诸如四色定理、开普勒猜想（Flyspeck项目用HOL Light完成）等著名成果，但费马大定理证明所调用的现代数学机器（modern machinery）之复杂，堪称登峰造极。

回顾这些已完成的里程碑有助于理解挑战的尺度。四色定理的形式化（2005年，Georges Gonthier使用Coq完成）是数学形式化的早期里程碑，证明了任何平面地图只需四种颜色就能使相邻区域不同色。开普勒猜想的形式化（Flyspeck项目，2014年，Thomas Hales团队使用HOL Light和Isabelle完成）验证了球体最密堆积的结论，这个项目耗时约20人年。更近期的里程碑包括完美图定理的形式化，以及前述的液态张量实验。值得注意的是，这些项目的规模和复杂度在逐步升级——从四色定理到开普勒猜想再到液态张量实验，所涉及的数学抽象层次越来越高，而费马大定理代表了迄今为止最具野心的形式化目标。

证明需要构建的前置理论包括：椭圆曲线理论、模形式、伽罗瓦表示、谷山-志村-韦伊猜想（模性定理）等。这里有必要展开解释这些概念。

椭圆曲线并非椭圆，而是形如 y² = x³ + ax + b 的三次曲线方程所定义的代数结构（名称来源于历史上计算椭圆弧长时出现的积分）。它们拥有一种自然的群结构——曲线上两个点可以通过几何方法「相加」得到第三个点——这使其成为数论中极其丰富的研究对象。椭圆曲线的算术性质与素数分布等深层问题紧密相关，著名的BSD猜想（Birch and Swinnerton-Dyer conjecture，千禧年七大问题之一）就是关于椭圆曲线上有理点的结构。在应用层面，椭圆曲线密码学（ECC）已被广泛部署，比特币使用的ECDSA签名算法、TLS协议中的密钥交换等都依赖于椭圆曲线离散对数问题的计算困难性。

模形式则是复分析中一类具有极高对称性的函数，定义在上半复平面上，在模群SL₂(ℤ)（或其子群）的作用下满足特定的变换性质和增长条件。直觉上，模形式可以理解为「在大量对称性约束下仍然存在的函数」，这种极端对称性使其携带了丰富的算术信息。每个模形式都有一个傅里叶展开（q-展开），其系数往往编码了深刻的数论数据。

谷山-志村-韦伊猜想（现称模性定理，已由布勒伊、康拉德、戴蒙德和泰勒在2001年完整证明）断言每条有理数上的椭圆曲线都对应一个模形式——更精确地说，椭圆曲线的L-函数等于某个权为2的新形式的L-函数。这在两个看似毫无关联的数学领域之间建立了深刻联系。这一联系被视为朗兰兹纲领（Langlands program）的一个重要实例。朗兰兹纲领由加拿大数学家罗伯特·朗兰兹在1967年提出，是当代数学中最宏大的统一愿景之一，它预言在数论中的算术对象（如伽罗瓦表示，编码素数在代数扩张中的分裂行为）与分析中的对称对象（如自守形式）之间存在系统性的对应关系。朗兰兹本人因这项工作获得了2018年阿贝尔奖。当前数学界在几何朗兰兹纲领方面取得了重大突破——2024年Arinkin、Gaitsgory等人宣布完成几何朗兰兹猜想的证明——而费马大定理的形式化也可被视为朗兰兹纲领数论分支走向机器验证的第一步。

这意味着形式化团队不仅要证明定理本身，还需要先在Lean的数学库 Mathlib 中建立起整座现代代数几何与数论的大厦。

蓝图驱动的协作方式

巴扎德采用了一种被称为「蓝图」（blueprint）的方法论来组织这项庞大工程。蓝图方法最早由帕特里克·马瑟（Patrick Massot）开发工具链支持。具体而言，数学家先用LaTeX撰写传统风格的数学证明，同时在其中嵌入特殊标记，将证明分解为一系列具有明确依赖关系的原子性声明（引理、定义、命题）。工具链会自动生成一个可交互的依赖关系图，每个节点用颜色编码：蓝色表示已在Lean中完成形式化，绿色表示LaTeX证明已写好但尚未形式化，灰色表示尚未开始。

整个证明被拆解成一个有向依赖图，每个节点是一个引理或定义，标注出哪些已经完成、哪些正在进行、哪些还依赖于尚未建立的前置结果。

这种可视化的方式让全球的贡献者能够并行工作，各自认领可以独立完成的子任务。这种方法的革命性在于它将一个看似不可能的庞大任务分解为成百上千个可独立攻克的小问题，极大降低了参与门槛——一个研究生甚至可能只需要掌握某个局部领域就能为项目做出贡献。这也体现了现代形式化数学的一个显著特征——它越来越像一个开源软件工程项目，而非孤独天才的个人英雄主义。

Lean与Mathlib生态的崛起

数学家的新工具箱

Lean 4作为一门函数式编程语言兼定理证明器，近年来在数学界的影响力急速攀升。其核心优势在于强大的依赖类型系统和活跃的社区支持。Mathlib 作为Lean的统一数学库，已经收录了从本科到研究生级别的海量数学定理，成为迄今为止最庞大的形式化数学知识库之一。

截至2024年底，Mathlib已包含超过17万个定理和15万个定义，代码量超过180万行，由数百位贡献者协作完成。它覆盖的数学领域包括群论、环论、拓扑学、测度论、概率论、组合数学、线性代数、范畴论等。Mathlib采用严格的编码规范和持续集成系统，每次代码提交都必须通过完整的编译检查和格式审查。这个库的维护本身就是一项浩大的工程——由于Lean语言和Mathlib内部结构都在演化，经常需要进行大规模的重构（refactoring），这类似于大型软件项目的技术债务管理。Mathlib的存在使得新的形式化项目不必从公理体系开始构建，而是可以直接调用已有的数学基础设施，极大地加速了形式化进程。

费马大定理项目的推进，本质上会反哺整个Mathlib生态。为了证明这个终极目标，团队被迫补全大量中间层的现代数学理论，这些成果将永久留存于Mathlib中，供未来所有形式化工作复用。

AI时代的形式化数学

形式化数学正与人工智能产生深刻的交汇。近年来，DeepMind的AlphaProof、以及各类基于大语言模型的定理证明辅助工具，都开始尝试自动生成Lean证明。

AI辅助定理证明领域近年来进展迅猛。DeepMind的AlphaProof在2024年国际数学奥林匹克（IMO）中展示了强大的竞赛数学问题求解能力，它结合了AlphaZero风格的强化学习与Lean形式化验证——系统在形式化环境中不断尝试证明策略，通过与证明检查器的反馈循环来学习。Meta的研究团队则开发了HyperTree Proof Search，在Lean和Metamath中自动证明了大量此前未被形式化的定理。此外，基于GPT-4等大语言模型的工具（如LeanDojo、Copilot for Lean）正在探索用自然语言提示生成形式化证明策略（tactics）。然而，当前AI在处理需要深层数学直觉和创造性构造的证明时仍然力不从心——它们擅长的是填充「显然但繁琐」的中间步骤，而非提出关键的证明思路。形式化数学的独特价值在于，它为AI提供了一个完美的训练和评估环境：证明要么通过要么不通过，没有模糊地带，这比自然语言数学中的评判标准精确得多。

费马大定理这样规模的项目，为AI辅助证明提供了极具价值的训练场与试金石。项目中存在大量繁琐的中间步骤，恰好是AI辅助的理想应用场景。

可以预见，人类数学家撰写蓝图、AI辅助填充繁琐的证明细节、Lean内核最终验证——这种人机协作的模式，或许正是未来数学研究的雏形。

结语：确定性的追求

尽管Hacker News上的讨论热度相对温和（41点赞、10条评论），但这个项目的象征意义远超其表面关注度。它代表着数学界对绝对确定性的不懈追求，也标志着形式化证明从边缘工具走向主流的历史进程。

费马在页边写下那句名言时，恐怕无法想象358年后，人类会用一种叫做「编程语言」的东西来彻底、无可辩驳地封印他留下的谜题。当Lean 4最终打出那个绿色的验证通过标志时，或许才是这个数学传奇真正画上句号的时刻。

核心要点

核心要点