让AI理解费马大定理的证明，两个月过去了，进展如何？_费马大定理费马证明出来了吗

声明：本文来自于微信公众号机器之心，授权转载发布。

1637年，费马在阅读丢番图《算术》拉丁文译本时，曾在第11卷第8命题旁写道:将一个立方数分成两个立方数之和，或一个四次幂分成两个四次幂之和，或者一般地将一个高于二次的幂分成两个同次幂之和，这是不可能的。关于此，我确信我发现一种美妙的证法，可惜这里的空白处太小，写不下。

这就是著名的费马大定理（FLT，也叫费马最后定理）:

当整数 n >2时，关于 x， y， z 的不定方程 xⁿ + yⁿ = zⁿ 无正整数解。

此后，无数数学家和数学爱好者都尝试过证明这个定理;甚至对该定理的证明一度成为民间数学家最爱挑战的难题之一，这个现象让数学历史学家霍华德・伊夫斯（Howard Eves）忍不住感慨:费马大定理的独特之处在于它是迄今为止发表错误证明最多的数学问题。

对费马大定理的首个完整证明直到358年之后的1995年才真正发表。为此，英国数学家安德鲁・怀尔斯（Andrew Wiles）使用了一系列复杂的数学工具和理论。整体而言，怀尔斯的证明建立在模形式和椭圆曲线之间的深刻联系(即谷山 - 志村猜想的一部分)之上，整个证明非常复杂，论文《Modular elliptic curves and Fermat’s Last Theorem》就有109页。

近日，伦敦帝国学院数学教授 Kevin Buzzard 在自己的博客上分享了一个非常有趣的项目:教计算机理解费马大定理的证明。这项工作可以帮助验证对费马大定理的证明，修正其中可能存在疏漏的部分。虽然计算机还没有完全理解，但也确实取得了一些进展。

这篇博客在 Hacker News 上吸引了大量讨论，很多人都分享了自己的见解或经历，尤其是关于数学形式化的重要性。

以上截图均来自 Hacker News 和谷歌翻译，更多讨论请访问:

https://news.ycombinator.com/item?id=42399397

以下是 Buzzard 教授的博客全文（原文段落较长，这里进行了适当拆分和调整）。

费马大定理 —— 进展如何?

我已经花了两个月时间来教计算机理解马大定理（FLT）的一个证明。

大部分的进展如何解释起来都相当繁琐且技术性:长话短说，怀尔斯证明了R=T定理，而到目前为止的大部分工作都是教计算机理解什么是 R 和 T;我们仍然还没有完成这两者中任何一个的定义。

但是，我的博士生 Andrew Yang 已经证明了我们需要的抽象可交换代数结果（如果抽象环(abstract rings）R 和 T 满足许多技术条件，则它们相等)，这是令人兴奋的第一步。

我们使用的系统是 Lean 及其数学软件库 mathlib，该软件库由 Lean 证明器社区维护。如果你对 Lean 和数论有所了解，可以考虑阅读贡献指南、查看项目仪表板并认领一个问题。

下面是一些相关链接:

• 蓝图和进展:https://imperialcollegelondon.github.io/FLT/blueprint/

• Lean:https://lean-fro.org/

• mathlib:https://github.com/leanprover-community/mathlib4

• 贡献指南:https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md

• 项目仪表盘:https://github.com/orgs/ImperialCollegeLondon/projects/102

• 问题:https://github.com/ImperialCollegeLondon/FLT/issues

蓝图页面截图

如前所述，我们已经进行了两个月。但是，我们已经有一个我认为值得分享的有趣故事了。谁知道这是否预示着某个未来。

我们的目的并不是形式化1990年代那个 FLT 证明。自那以后，已经有很多人（Diamond/Fujiwara、Kisin、Taylor、Scholze 等人）对该证明进行了泛化和简化。我的部分动机是要证明这些更通用、更有力的结果。为什么这是因为如果 AI 真的可以变革数学(有可能)，并且 Lean 被证明是一个重要的组成部分(也有可能)，那么计算机将能够更好地帮助人类突破现代数论的界限。对于这种形式化工作，计算机能够以它们理解的方式来获得关键的现代定义。

怀尔斯的原始证明中没有使用的一个概念，在我们正在形式化的证明中使用了，它就是晶体上同调（crystalline cohomology）。

这是20世纪六七十年代在法国巴黎发展起来的理论，其基础是由数学家 Berthelot 根据另一位数学家 Grothendieck 的思想搭建的。基本思想是经典指数和对数函数在微分几何（例如 Lie 代数和 Lie 群）发挥关键作用，特别是在理解德拉姆上同调(de Rham cohomology，)中，不过它们在更多的算术情况下不起作用(例如在特征 p 中)。

20世纪六十年代，Roby 在一系列精彩的论文中提出了除幂结构（divided power structures），在构建可用于算术情况的类函数中发挥了至关重要的作用。注:我们要想教计算机晶体上同调，首先需要教它除幂理论。

数学领域的研究者 Antoine Chambert-Loir（简称 Antoine）和 Maria Ines de Frutos Fernandez(简称 Maria Ines)一直在教 Lean 除幂理论，而整个夏天，Lean 都时而出现一种令人恼火的情况:它会抱怨标准文献中人为提出的论证，并经过仔细检查发现人为论证有待改进，特别是 Roby 的工作中有一个关键引理似乎不正确。当 Antoine 告诉我这件事时，他觉得我会认为这很有趣，而他收到的回复中一长串大笑的表情符号确实证实了这一点。

然而，Antoine 比我更专业，认为我不应该发推讨论这个问题（反正我也不发，我已经抛弃了推特并转向了社交平台 bluesky），而应该尝试解决这个问题。

我们以完全不同的方式来处理这个问题，Antoine 把它列入了自己的工作清单，而我却完全忽略了它，只是偶尔向人们提及这个证明有问题，是弱证明。我之所以说是弱证明，是因为这一观察必须放在某种背景下。

根据我目前对数学的观察（作为形式主义者），当 Antoine 发现这个问题时，整个晶体上同调理论就从文献中消失了，并带来巨大的附带损害(例如数学家 Scholze 的大量工作就消失了，整本的书籍和论文都化为乌有)。但这种消失只是暂时的，晶体上同调在实际意义上并没有错误。这些定理毫无疑问仍然是正确的，只是就我而言，证明是不完整的(或者至少 Antoine 和 Maria Ines 遵循的证明不完整)。因此我们的工作就是修正它们。

我想强调的是，我和 Antoine 都很清楚，即使中间引理是错误的，主要结果的证明当然可以修正，这是因为从20世纪70年代以来晶体上同调就得到了广泛使用。如果它有问题，早就该暴露出来了。我交流过的每个专家都同意这一点，有几位甚至认为我在小题大做。但也许他们不明白形式化在实践中到底意味着什么:你不能只是说我相信它可以修正，你必须真正地修正它。另外，Roby、Grothendieck 和 Berthelot 都已经去世了，我们无法从这些原来的专家那里直接寻求帮助。

对更多技术细节感兴趣的人可以先看这里:Berthelot 的论文并没有从头开始发展除幂理论，他使用了 Roby 的Les algebres a puissances divisees，1965年在 Bull Sci Math 上发表。该论文的引理8似乎是错误的，而且如何修正证明也没说明白。该引理的证明错误引用了 Roby1963年 Ann Sci ENS 论文中的另一个引理。其正确的表述是Gamma_A （M） tensor_A R = Gamma_R (M tensor_A R)，但其中一个张量积在应用中意外脱离。这就打破了 Roby 关于模(module)的除幂代数具有除幂]的证明，从而阻止我们定义环 A_{cris}。

所以，正如我所言，Antoine 正致力于解决这个问题，而我只是在向专家们八卦闲谈，而且我犯了一个错:在伊斯灵顿的一家咖啡店告诉了時枝正（Tadashi Tokieda）这件事，他回到斯坦福后向 Brian Conrad 提到了这件事，然后 Conrad 就开始在我的收件箱里问我晶体上同调有问题到底是怎么回事。

我解释了这个问题的技术细节，Conrad 同意这好像确实是一个问题，然后他开始思考。几个小时后，他回复了我，并指出，在 Berthelot-Ogus 的关于晶体上同调的著作的附录中，存在对模的一般除幂代数具有除幂这个断言的另一个不同的证明，而且 Conrad 认为这个方法没有问题。证明又回来了!

这差不多就是故事的全部。上个月我访问了伯克利，和 Arthur Ogus 共进午餐，我90年代在那里做博士后的时候就认识他了。我答应过 Arthur，给他讲一个他如何拯救费马大定理的故事，吃饭的时候我告诉他，他的附录如何把我从困境中救了出来。他的回答是哦!那个附录有几个错误!但没关系，我想我知道如何修正它们。

在我看来，这个故事表明，人们在编写现代数学文档方面做得很差。似乎有很多东西是专家们已知的，但却并没有得到正确的文档化。

这些专家们一致认为，重要的想法足够强大，可以经受住这样的打击，但实际发生的细节可能并不像人们期望的那样。对我来说，这只是人类想要正确记录数学的众多原因之一，即在形式系统中，错误的可能性要小几个数量级。

然而，大多数数学家都不是形式主义者，对于这些人，我需要以不同的方式说明我的工作的合理性。对于那些数学家而言，我认为教会机器理解我们的论证是让机器自己做这件事的关键一步。在此之前，我们似乎注定要手动修正人为错误。

不过，这个故事确实有一个圆满的结局 —— 两周前，Maria Ines 在剑桥数学形式化研讨会（Cambridge Formalization of Mathematics seminar）上发表了一个关于除幂的形式化的演讲。根据这个演讲，我的理解是这些问题现在已经得到解决了。所以我们实际上又回到了正轨。直到下一次文献让我们失望……

参考链接:

https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/

https://news.ycombinator.com/item?id=42399397