现在，一群数学家决定用计算机来终结这场旷日持久的争吵。
ABC猜想本身并不难理解。它描述的是方程 a + b = c 中，整数a、b、c所含质因数之间的一种约束关系。尽管表述简洁，这个猜想却牵涉加法与乘法之间深层的相互作用，其解决对费马大定理推广、丢番图方程等众多数论分支都具有深远影响，是数学家梦寐以求的一块拼图。
2018年，德国波恩大学顶尖数学家彼得·朔尔策和雅各布·斯蒂克斯飞赴京都，与望月当面会谈，试图理清证明的核心逻辑。结果却令人失望，两人返回后明确表示，在证明的关键步骤中存在一个他们无法接受的逻辑空洞，而望月坚持认为这两位来访者根本没有理解他的理论。此后双方各执一词，争论陷入僵局。日本数学界官方期刊2021年正式发表了这篇证明，但国际主流数学社区仍普遍持怀疑态度。这种"只在日本成立的证明"的说法，让这场争论更增添了几分戏剧色彩。
人类数学家争论了十余年没有结果，现在轮到机器来试试了。
据《新科学家》报道，两个独立的计算机形式化验证项目已经启动，目标是将ABC猜想相关的数学逻辑翻译成计算机可以逐行检查的语言，从而客观判断证明链条中是否存在错误或跳跃。其中一个项目已秘密运行超过两年，直至近日才浮出水面。参与者均为熟悉形式化证明工具的数学家，他们使用的平台是Lean，这是一款由微软研究院支持开发的定理证明助手，近年来在数学社区中迅速普及。
Lean的工作原理，是强制要求每一个逻辑步骤都必须被明确写出，不允许任何"显然可得"或"留给读者自证"的跳跃。一旦某个步骤无法被系统验证，错误将立即暴露。哥伦比亚大学数学家彼得·沃伊特在其博客中写道，如果一位真正理解IUT理论、同时精通Lean的数学家能够完成形式化，结果将立即终结这场主要争议。
问题在于，这两个条件同时满足的人，目前全球几乎找不到几个。IUT理论的复杂程度意味着，仅仅理解它就需要数年的专门学习，将其翻译成Lean代码则是更大的挑战。参与项目的研究者坦承，最可能的结果是：绝大部分证明可以被验证，但在某个关键节点，隐藏着一个无法被形式化的断言，而那个断言，可能正是朔尔策和斯蒂克斯当年指出的那个争议点。
不过，形式化项目的启动本身，已经是一个重要信号。它意味着越来越多的数学家认为，靠人类的相互说服已经走到了死胡同，必须引入第三方裁判，而计算机是目前最客观的选择。Reddit数学社区对此反应热烈，不少用户指出，无论最终结论是证明成立还是存在漏洞，有了计算机验证的结论，至少争论可以建立在同一套事实基础之上。
这场始于2012年的数学公案，或许正在走向它最终的裁决时刻。
热门跟贴