为什么费马大定理的证明不需要改进

自Fermat伟大的定理得到具有里程碑意义的证明以来，数十年来，关于如何使其更加可靠的想法浮出水面。 但是，这些尝试反映了对使证据变得重要的深刻误解。

6月23日是安德鲁·威尔斯 （ Andrew Wiles）宣布成立25周年，这引起了所有人的兴奋，他宣布收到费马大定理的证明，该定理是350年来数学上最著名的问题。 关于威尔斯证据的故事-他秘密从事此项目长达七年之久，6月宣布后出现了证据差距，一年后，威尔斯与他的前学生理查德·泰勒 （ Richard Taylor）联合撰写了一篇优雅的解决方案，并于2000年获得了骑士勋章-进入了数学传奇史册。

威尔斯（Wiles）突破之后，人们经常会听到关于数学特别是数论（费马定理所属的领域）出现新的“黄金时代”的猜测。 威尔斯（Wiles）和泰勒（Taylor）提出的方法如今已成为考虑了大定理历史的数论专家工具包的一部分。 但是这个故事不仅感动了数论专家。

2017年的事件让我突然想起了这一点，当时在几天之内，在两个不同大陆进行报告的两位逻辑学家指出了改进定理证明的方法-并谈到了当数论专家没有表现出对同事的惊讶他们的想法毫无意义。

逻辑学家用各自专业的语言表达了这些思想，即集合论和理论计算机科学。 他们提出的建议本质上是真实的，也许有朝一日他们会提出新的问题，与Fermat的建议一样有趣。 但是，对我而言，立即清楚的是，这些问题与数论专家无关，并且任何其他假设都反映了对维尔斯证明的本质和数论目标的深刻误解。

这种误解的根源可以从定理的简单陈述中找到，该定理是其吸引人的主要原因：如果n是大于2的任何正整数，则不可能找到三个这样的正数a，b和c，从而：

$$

$$a ^ n + b ^ n = c ^ n$$

这与n为2的情况形成鲜明对比：研究欧几里得几何的任何人都将记住3 ² + 4 ² = 5 2，5 ² + 12 ² = 13 ² ，依此类推（以此类推）。 在过去的几个世纪中，数学家一直试图解释这种对比的存在，但是每次失败时，它们就会留下全新的数学分支。 在这些分支中，有威尔斯因其成功的解决方法而吸引着的现代数字理论的大领域，以及数学家触及的科学每一部分的许多基本思想。 但在威尔斯之前，没有人能证明费马的主张。

最近，计算机科学家对了解自动确认证据的进展感到兴奋，这是将形式主义数学方法付诸实践的雄心勃勃的尝试。 对于形式主义者，数学证明是满足严格限制的一系列语句：

1. 列表顶部的声明应包含公认的想法。 在严格的解释中，这仅包括形式集理论的公理，通常来自称为ZFC （具有选择公理的Zermelo-Frenkel系统）的形式系统。 这是完全不切实际的，因此我们也允许包含已经证明的定理-例如，n = 4情况下的大定理，这是费马特本人在17世纪证明的。
2. 必须通过将逻辑推导规则应用于先前的语句来获取每个后续​​语句。
3. 最后，证明定理应该在列表的最后。

开发数学逻辑是为了希望将数学建立在坚实的基础上-作为没有矛盾的公理系统，该系统能够推理而不会陷入矛盾。 尽管库尔特·哥德尔（KurtGödel）的工作证明了这一梦想是无法实现的，但许多数学哲学家以及一些逻辑学家（根据集合论的专家认为，这是少数但活跃的少数派）仍然将ZFC和上述要求视为数学的一种构成。

但是，数学家永远不会以这种方式写证据。 对Wiles证据的逻辑分析指出，许多步骤没有考虑ZFC，并且有可能引起丑闻：如果数学家在不检查合宪性的情况下提出规则，他们怎么知道它们都是同一件事？

自动验证证据似乎可以解决此问题。 它涉及通过一组单独的语句来重新构造证据，每个语句都以计算机可以阅读的一致语言编写，然后确认每个步骤的结构保真度。 这种费时的方法已成功地应用于许多冗长而复杂的证明，其中最著名的是开普勒关于托马斯·海尔斯（Thomas Hales）制造的最密堆积球的假设的证明。 长期以来，检验威尔斯的证据一直被认为是主要目标之一。 因此，我的朋友，一位计算机科学专家，对他提出的“纯粹支持数学家在论证中使用自动工具的纯粹数学家”的搜索感到非常失望。


1670年丢番图版《 算术 》，其中臭名昭著的费马笔记也包括在正文中。 在翻译中，其含义如下：``一个立方体不可能是两个立方体的总和，对于第四度来说，不可能是两个第四度的总和，或者通常，对于任何代表大于第二度的度的数，都不可能是两个相同度的总和。 我已经发现了这一假设的确凿证据，这些领域太狭窄而无法容纳。

没有考虑到这种失望的第一件事是，威尔斯的证据尽管很复杂，但有一个简单的基础，很容易向普通观众解释。 假设与费马的说法相反，存在三个正整数a，b，c，使得

（a）a ^p + b ^p = c ^p

对于一些奇数质数p（仅考虑质数就足够了）。 1985年，格哈德·弗雷（Gerhard Frey）证明a，b和c可以重新排列为

（二）一个新的方程称为“椭圆曲线”

具有每个人都认为不可能的特性。 更确切地说，人们早就知道如何用

（C）伽罗瓦代表

这是一组与椭圆曲线相关并通过明确规则彼此相关的无限等式。

这些步骤之间的联系在1985年是众所周知的。 到那时，尽管到目前为止还没有证据表明，大多数数论专家都确信，可以根据明确的规则再次分配每个Galois代表，

（四）模块化功能，

类似三角函数中熟悉的正弦和余弦函数的二维概括。

当肯·里贝特（Ken Ribet）确认让·皮埃尔·瑟尔（Jean-Pierre Seur）的假设时，就获得了最终联系。

（E）权重2和等级2的另一个模块化功能。

但是，这些功能不存在。 因此，既不存在模函数（D），也不存在伽罗瓦表示（C），也不存在方程（B），也不存在解（A）。

剩下的只是找到（C）和（D）之间缺失的联系，数学家将其称为模块化假设。

该链接一直是Wiles搜寻了7年的主题。 从我们当前的角度来看，很难完全理解这个冒险企业的勇气。 谷山丰（Yutaka Taniyama）和志村吾郎（Goro Shimura）在1950年代首次报道 （B）与（D）到（C）之间的关系20年之后，数学家逐渐得出结论，事实应该是这样。 这种希望在安德烈·威尔（Andre Weil）的一项非常受欢迎的作品中得到了表达，该作品完全符合以加拿大数学家罗伯特·兰兰兹（Robert Langlands）命名的极具影响力的Langlands计划 。 这种联系太好了，不能真实。 但是，模块化的假设似乎完全无法实现。 （C）和（D）类型的对象太不同了。

这位计算机科学家没有解释他的失望是否是由于以下事实：对数论并不重要的是，证据仅限于寻找（C）与（D）之间的关键链接，或者从（A）到（D） （E）。 我不会尝试解决。 但是，如果逻辑学家只需要正式确认（C）和（D）之间联系的公开证明，那么他们的期望就太高了。 首先，Wiles证明了模块化假设足以完成“从（A）到（E）”的推论。 几年后，克里斯托夫·布罗意（Christoph Broglie），布莱恩·康拉德（Brian Conrad），弗雷德·戴蒙德（Fred Diamond）和理查德·泰勒（Richard Taylor）建立了模块化的完整假设。 但这并没有给威尔斯的作品蒙上阴影！ 相反，这么多世界领先的数论专家在维尔斯出现仅仅几个月后便跟随了威尔斯的足迹，这说明了它的财富。

例如，不久之后，在2016年秋天，十名数学家在新泽西州普林斯顿的高级研究所开会，并能够证明在新条件下椭圆曲线和模函数之间存在联系。 他们都使用不同的途径来理解威尔斯证据的结构，这些证据是在他们中有些还小的时候出现的。 如果要求他们以一系列逻辑结论的形式描述这一证明，那么他们无疑会发行10种不同版本的证明。 它们中的每一个都类似于上述从（A）到（E）的路径，但是会更加详细。

然而，这-从证据的哲学观点上总是被忽视-这十个证据中的每一个都将其证据的作者归于威尔斯。 他们将以与他们在解释性文章或他们参加或教授的培训课程中研究的其他证据相同的方式提及他们。 尽管十个人中的每一个都会省略一些细节，但总的来说，它们都是正确的。

如果威尔斯可以有这么多不同的选择，那么威尔斯的证据是什么？ 在数学哲学中，习惯上将已发布的证明作为理想形式证明的近似，原则上可以在应用形式系统规则的计算机上对其进行检查。 理想证据不受形式体系之外的任何事物的污染-好像每部法律都带有确认其宪法合理性的标记。

但是这种方法与数学家们自己关于他们的证据的说法相矛盾。 数学家不使用意识形态或哲学试题，但我坚信大多数同事会同意迈克尔·弗朗西斯·阿提亚（Michael Francis Atiyah）的观点，他说证明“是最终的测试，而不是任何依据”。 公开的证据显然不是任何依据。

威尔斯和数论专家，完善和扩展他的思想，当然没想到会收到两位逻辑学家的邀请。 但是-与许多人从远处观察数论不同-他们明确地理解，Wiles所发表的证明本身不应被视为一种人工产物。 相反，Wiles的证明是公开对话的起点，这种对话太含糊而生动，以致不能局限于与该主题无关的严格限制。