現(xiàn)在，一群數(shù)學(xué)家決定用計(jì)算機(jī)來終結(jié)這場曠日持久的爭吵。

ABC猜想本身并不難理解。它描述的是方程 a + b = c 中，整數(shù)a、b、c所含質(zhì)因數(shù)之間的一種約束關(guān)系。盡管表述簡潔，這個(gè)猜想?yún)s牽涉加法與乘法之間深層的相互作用，其解決對費(fèi)馬大定理推廣、丟番圖方程等眾多數(shù)論分支都具有深遠(yuǎn)影響，是數(shù)學(xué)家夢寐以求的一塊拼圖。

2018年，德國波恩大學(xué)頂尖數(shù)學(xué)家彼得·朔爾策和雅各布·斯蒂克斯飛赴京都，與望月當(dāng)面會談，試圖理清證明的核心邏輯。結(jié)果卻令人失望，兩人返回后明確表示，在證明的關(guān)鍵步驟中存在一個(gè)他們無法接受的邏輯空洞，而望月堅(jiān)持認(rèn)為這兩位來訪者根本沒有理解他的理論。此后雙方各執(zhí)一詞，爭論陷入僵局。日本數(shù)學(xué)界官方期刊2021年正式發(fā)表了這篇證明，但國際主流數(shù)學(xué)社區(qū)仍普遍持懷疑態(tài)度。這種"只在日本成立的證明"的說法，讓這場爭論更增添了幾分戲劇色彩。

人類數(shù)學(xué)家爭論了十余年沒有結(jié)果，現(xiàn)在輪到機(jī)器來試試了。

據(jù)《新科學(xué)家》報(bào)道，兩個(gè)獨(dú)立的計(jì)算機(jī)形式化驗(yàn)證項(xiàng)目已經(jīng)啟動，目標(biāo)是將ABC猜想相關(guān)的數(shù)學(xué)邏輯翻譯成計(jì)算機(jī)可以逐行檢查的語言，從而客觀判斷證明鏈條中是否存在錯(cuò)誤或跳躍。其中一個(gè)項(xiàng)目已秘密運(yùn)行超過兩年，直至近日才浮出水面。參與者均為熟悉形式化證明工具的數(shù)學(xué)家，他們使用的平臺是Lean，這是一款由微軟研究院支持開發(fā)的定理證明助手，近年來在數(shù)學(xué)社區(qū)中迅速普及。

Lean的工作原理，是強(qiáng)制要求每一個(gè)邏輯步驟都必須被明確寫出，不允許任何"顯然可得"或"留給讀者自證"的跳躍。一旦某個(gè)步驟無法被系統(tǒng)驗(yàn)證，錯(cuò)誤將立即暴露。哥倫比亞大學(xué)數(shù)學(xué)家彼得·沃伊特在其博客中寫道，如果一位真正理解IUT理論、同時(shí)精通Lean的數(shù)學(xué)家能夠完成形式化，結(jié)果將立即終結(jié)這場主要爭議。

問題在于，這兩個(gè)條件同時(shí)滿足的人，目前全球幾乎找不到幾個(gè)。IUT理論的復(fù)雜程度意味著，僅僅理解它就需要數(shù)年的專門學(xué)習(xí)，將其翻譯成Lean代碼則是更大的挑戰(zhàn)。參與項(xiàng)目的研究者坦承，最可能的結(jié)果是：絕大部分證明可以被驗(yàn)證，但在某個(gè)關(guān)鍵節(jié)點(diǎn)，隱藏著一個(gè)無法被形式化的斷言，而那個(gè)斷言，可能正是朔爾策和斯蒂克斯當(dāng)年指出的那個(gè)爭議點(diǎn)。

不過，形式化項(xiàng)目的啟動本身，已經(jīng)是一個(gè)重要信號。它意味著越來越多的數(shù)學(xué)家認(rèn)為，靠人類的相互說服已經(jīng)走到了死胡同，必須引入第三方裁判，而計(jì)算機(jī)是目前最客觀的選擇。Reddit數(shù)學(xué)社區(qū)對此反應(yīng)熱烈，不少用戶指出，無論最終結(jié)論是證明成立還是存在漏洞，有了計(jì)算機(jī)驗(yàn)證的結(jié)論，至少爭論可以建立在同一套事實(shí)基礎(chǔ)之上。

這場始于2012年的數(shù)學(xué)公案，或許正在走向它最終的裁決時(shí)刻。