500頁論文引十年爭論，ABC猜想終審IUT理論迎終極裁決

現在，一群數學家決定用計算機來終結這場曠日持久的爭吵。

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

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

人類數學家爭論了十余年沒有結果，現在輪到機器來試試了。

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

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

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

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

這場始于2012年的數學公案，或許正在走向它最終的裁決時刻。