数学
教电脑证明费马大定理
教电脑证明费马大定理，揭开分幂理论中的漏洞，人类错误促使数学形式化迈进新一步。
两个月前，我开始尝试教一台电脑证明费马大定理(FLT)。大部分进展都极其琐碎且技术性极强。简单来说，Wiles的证明建立在“R=T”定理上，目前我们主要在教电脑什么是R和T，但到现在连定义都还没完成。不过，我的博士生Andrew Yang已经证明了一个我们需要的抽象交换代数结果——如果抽象环R和T满足许多技术条件，那么它们相等。这是令人兴奋的第一步。我们使用的系统是Lean和其数学库mathlib，由Lean证明社区维护。如果你熟悉Lean和一些数论，可以查看贡献指南、项目面板并认领任务。
我们并不是在形式化上世纪90年代的旧版证明。之后，许多学者(如Diamond、Fujiwara、Kisin、Taylor、Scholze等)将其推广并简化。这次工作不仅为了重新证明FLT，还希望通过形式化推进更广泛、强大的数学成果。这么做的原因在于，如果数学的AI革命真的到来，而Lean成为重要组成部分，电脑将能用理解的形式访问关键现代定义，从而协助人类突破数论的边界。
我们使用晶体上同调这一概念，这是Wiles原始证明中没有用到的。它由Berthelot基于Grothendieck的想法在20世纪六七十年代创立。经典的指数函数和对数函数在微分几何中至关重要，但在特征p等算术背景下不适用。“分幂结构”理论是Roby在20世纪60年代发展起来的，它构造了一种算术情况可用的函数类比。简而言之，我们必须教电脑晶体上同调，而这需要先教分幂结构。
Antoine Chambert-Loir和Maria Ines de Frutos Fernandez正在用Lean教授分幂理论。夏天时，Lean对标准文献中的人类论证提出异议，结果发现人类论证确实有问题。尤其是Roby论文中的一个关键引理似乎不正确。当Antoine用私信告诉我时，他猜我会觉得好笑，结果我给了他一串大笑表情回应。不过，他更专业，决定修复这个问题，而不是像我一样只顾散播“这个证明有麻烦”的消息。
Antoine最终确认Roby的引理存在错误，而Berthelot、Grothendieck和Roby都已去世，无法向他们寻求帮助。我们将问题告诉了一些专家，其中Brian Conrad通过Berthelot-Ogus关于晶体上同调的书中的附录找到了另一个证明。该证明的正确性让我们得以继续下去。
上个月，我在伯克利与Arthur Ogus共进午餐时提到此事，他的附录帮助解决了问题。然而，他表示附录本身也有一些错误，不过他知道如何修复。
这个故事让我感到，人类在记录现代数学上做得有多差。许多“专家知道”的内容并未被正确记录。尽管重要的数学思想足够稳固，但细节却可能埋藏得很深。这也是为什么我们需要将数学形式化，以减少错误。但这项工作需要不断修复人类错误，而这只是第一步。
幸运的是，Maria Ines两周前在剑桥数学形式化研讨会上报告了分幂理论的形式化，问题已经解决。我们又回到了正轨，直到下一次文献再次让我们失望。