数学中最大的争议可以由计算机解决

数学界最具争议性的争论之一可以借助计算机得到解决，从而有可能结束一场持续十多年的关于复杂证明的激烈争论。

麻烦始于 2012 年，当时望月新一 (Shinichi Mochizuki) 日本京都大学震惊数学界 ABC 猜想的证明长达 500 页，这是一个重要的未解决问题，触及数字的核心。该证明使用了望月新一发明的技术性高且深奥的框架，称为泛宇宙 Teichmüller (IUT) 理论，即使对于大多数试图理解它的专家数学家来说，该理论也显得难以理解。

ABC 猜想已有 40 多年的历史，它涉及一个看似简单的三个整数方程：a + b = c，并规定了组成这些数字的素数必须如何相互关联。该猜想不仅深入了解加法和乘法如何相互作用的基本性质，还对其他著名的数学猜想（例如费马大定理）具有影响。

这些潜在的后果使数学家最初热衷于验证证明，但早期的努力步履蹒跚，望月新一感叹没有付出更多的努力来消化这项工作。然后在 2018 年，两位著名的德国数学家 Peter Scholze 波恩和雅各布·斯蒂克斯大学 法兰克福歌德大学宣布他们在证明的盔甲上发现了一个可能的裂缝。

但望月新一拒绝了他们的论点，而且由于没有大的裁决机构来裁决谁对谁错，IUT 理论的有效性被冻结为两个阵营：一方面是大多数数学界；另一方面是数学界。另一方面，一小群研究人员松散地隶属于望月新一和他担任教授的京都数学科学研究所。

现在，望月新一提出了一个可能的解决僵局的方案。他建议将证明从目前的形式（为人类设计的数学符号）转换为一种名为 Lean 的编程语言，这种语言可以由计算机自动检查和验证。

这个过程称为形式化，是一个正在进行的研究领域，可以彻底改变数学的完成方式。之前曾有人建议将望月新一的证明形式化，但这是他第一次表示愿意推进该项目。

望月新一没有回应对本文发表评论的请求，但在最近的一份报告中，他认为精益非常适合解决数学家之间的各种分歧，这些分歧阻碍了他的证明被广泛接受：“[Lean] 是最好的，也许是唯一的技术……在将数学真理从社会和政治动态的束缚中解放出来的基本目标方面取得有意义的进展，”望月新一写道。

望月新一表示，在 7 月份参加了最近在东京举行的精益会议后，他对形式化的优点深信不疑，特别是在看到形式化处理数学结构的能力后，他认为形式化对于他的 IUT 理论至关重要。

凯文·巴扎德 (Kevin Buzzard) 表示，这是一个有助于打破僵局的潜在有希望的方向 在伦敦帝国理工学院。 “如果用精益写下来，那就不算疯狂，对吧？论文中的很多东西都是用一种非常奇怪的语言写的，但如果你能用精益写下来，那就意味着至少这种奇怪的语言已经成为一种完全明确定义的东西，”他说。

“我们想了解原因 [of IUT]，我们已经等待这一天十多年了。”Johan Commelin 说道 在荷兰乌得勒支大学。 “精益将能够帮助我们理解这些答案。”

然而，Buzzard 和 Commelin 都表示，形式化 IUT 理论将是一项艰巨的任务，并且需要翻译大量目前仅以人类可读形式存在的数学方程。该项目将与迄今为止完成的一些最大的形式化工作相媲美，这些工作通常涉及专家数学家和精益程序员团队，需要数月或数年的时间。

对于少数有资格承担该项目的数学家来说，这种令人畏惧的前景可能是一个没有吸引力的提议。巴扎德说：“人们必须做出重大判断，决定是否愿意投入大量时间从事一个最终可能会失败的项目。”

但即使数学家们确实成功完成了这个项目，并且精益代码表明望月新一定理没有矛盾，包括望月新一本人在内的数学家们仍然可能会争论其含义，科梅林说。

“精益可以产生很大的影响并结束争议，但前提是望月新一真正坚持他的新决议，将他的工作正式化，”他说。 “如果他在四个月后离开，说，‘好吧，我尝试过这个，但里恩太愚蠢了，无法理解我的证明’，那么这只是一系列很长的章节中的一个新章节，我们仍然陷入社会问题之中。”

而且，尽管望月新一对精益表现出乐观态度，但他也同意批评者的观点，即解释代码的含义可能会导致进一步的分歧，他写道，精益“目前看来并没有构成彻底解决社会和政治问题的任何“灵丹妙药”。”

然而，巴扎德希望，成功的正式化至少可以推动长达十年的传奇故事继续下去，特别是如果望月新一成功的话。 “你无法与软件争论，”他说。