陶哲軒用AI證明數學猜想實乃誤讀，但數學界仍大受震動

2023年是數學界濃墨重彩的一年。組合學領域的知識爆發式增長。在去年年末，4位重量級數學家更是組隊拿下了加性組合學的圣杯。但對于加性組合學這一年輕、活力四射的研究領域，公眾卻知之甚少。而此事的后續，或許才是影響最為深遠的?！拔覀儗褦祵W數字化，這會讓數學變得更好”。

撰文 | 嘉偉

回顧剛剛過去的2023年，結出累累碩果的組合數學是最令世人矚目的數學分支。在該領域里，全年中幾乎每兩個月便冒出一項令全球數學家嘆為觀止的重大理論突破。剛到10月份，今年在組合學方面的重要論文，竟然給研究和學習者一種“吃撐”的感覺：極值圖論和拉姆齊理論、平面染色理論、平面密鋪、不可傳遞骰子、加性組合以及被菲爾茲獎得主W. T. Gowers譽為組合學（可能的）第一猜想的“有限集合的并集猜想”，組合學中的各個子領域全面開花，統統取得了歷史性的重大進展，甚至為有些課題畫上了完美的句號！

其實在9月中，著名數學家陶哲軒剛剛結束了一項持續了近兩年之久的、重要又艱辛的工作——徹底解答高維空間里的單瓷磚平移周期性覆蓋的問題——一個關聯數理邏輯（圖靈機）和高維離散幾何的難題。同時，陶哲軒公開表示，他打算用一個多月的時間來學習一種名為Lean的、特殊的形式化編程語言。所以，不少人都感到，組合學全年高潮迭起的劇情或許終將歸于平靜，起碼到2024年之前都理應是如此。

誰知在11月13日，組合數學大師Gil Kalai突然宣布，有一支團隊剛剛證明了加性組合學里的圣杯、已故的杰出女性數學家Kati Marton提出的著名猜想——多項式Freiman-Ruzsa猜想。

合著論文的團隊，幾乎是當前人類能拿出來的組合學最強陣容：W. T. Gowers、Ben Green、Freddie Manners、Terence Tao（即陶哲軒）。他們讓過去的一年擁有了一個數學版童話故事般的結局。

四位作者淵源頗深。Gowers和陶哲軒，都是菲爾茲獎得主，是當代組合學界的領軍人物。陶哲軒榮獲菲爾茲獎的重要理由之一便是與Ben Green共同發現了Green-Tao定理。Freddie Manners則是Green的博士生，現為加州大學圣迭戈分校的數學副教授。

圖中人物從上到下，從左至右分別為Gowers，陶哲軒，Manners和Green。|圖源：Gil Kalai的博客Combinatorics and more: Image (wordpress.com)

隨后一個月的時間里，陶哲軒等人又做了一件轟動數學界的大事：使用前文提到的Lean語言，把他們的證明形式化。它在數學史上的重要性或許還要超越證明猜想本身。

編寫Lean語言代碼的時候，陶哲軒借助了當下流行的AI編程助手Copilot。因此，當相關新聞傳回國內時，一些公眾號誤以為陶哲軒借助AI證明了重要的數學猜想，并誕生不少以此為標題的文章。

這種說法當然是錯的。

但是，為什么陶哲軒的團隊用Lean語言形式化了論文就引發了學術界的巨震？為了方便理解，事情還得從“加性組合是什么”說起。

加性組合與多項式Freiman-Ruzsa猜想

加性組合學（Additive Combinatorics）是一門非常年輕的數學分支。正因為年輕，它也是當前數學界最有活力的研究領域之一。

它起源于一個國人非常熟悉的哥德巴赫猜想：

任一大于2的偶數都可寫成兩個質數之和。

從上面的哥德巴赫猜想，我們可以推得所謂的弱哥德巴赫猜想：

任一大于5的奇數都可寫成三個質數之和。

在1742年普魯士的數學家克里斯蒂安·哥德巴赫（Christian Goldbach）與大數學家萊昂哈德·歐拉（Leonhard Euler）通信之前，人們普遍認為，質數就是用于相乘的，而沒人考慮過質數之間的加法會帶來何種性質。

事實證明，哥德巴赫猜想是最難的一類問題。直至今日，數學家對于哥德巴赫猜想的完整證明仍然沒有任何頭緒。實際上，在猜想提出后的很長一段時間內甚至毫無進展，直到20世紀20年代，數學家才從組合學與解析數論兩方面分別提出了解決的思路，并在其后的半個世紀里取得了一系列突破。

哥德巴赫猜想迫使數學家去考慮質數的加法結構，由此誕生了一門學科：加法數論。數學泰斗華羅庚則稱它為堆壘數論！其中更偏組合學的研究路線如下：考慮全體奇質數構成的集合，令其與自身相加，如果得到的“和集”包含所有大于4的偶數，則猜想獲證。

所謂集合相加，就是一個集合里的每一個元素，與另一集合里的每一個元素相加。其和構成的新集合叫和集。

我們以簡單的有限集加法為例：

{1，2，3}+{1，2}={2，3，3，4，4，5}={2，3，4，5}（因為集合里重復的元素看成是同一個元素。）

從上面可以看出，這一路線更加偏整體和宏觀，是往系統里“塞”結構。另一方面，解析數論里的篩法工具，則是把系統里的“多余”結構過濾掉。當然，這是一種大而化之的漫畫式解讀。實際上，兩種研究風格是互相滲透，互相“利用”的。為了發展組合學方法，需要大量解析數論里的篩法技術。

雖然一開始，加法數論里的組合路線率先為哥德巴赫猜想帶來了突破，蘇聯數學家列夫·根里霍維奇·施尼雷爾曼（Lev Genrikhovich Schnirelmann）借助上面集合相加的組合學思路（同時運用簡單的篩法），證明了任何足夠大的自然數，都可以寫成若干質數之和。雖然這一結論離哥德巴赫猜想還有十萬八千里，但這是第一次在自然數與質數和之間建立起關系，可以看作是從0到1的突破。

蘇聯著名的數學家亞歷山大·雅科夫列維奇·辛欽（Aleksandr Yakovlevich Khinchin）將施尼雷爾曼的結論譽為“數論三大明珠”之一。辛欽就是《數學分析簡明教程》《數學分析八講》等經典教材的作者。學習概率論的朋友，對辛欽大數定律應該也不陌生。

遺憾的是，在數學實踐中，尤其是陳景潤發表了解析數論中著名的陳氏定理（“1+2”）之后，人們意識到，施尼雷爾曼的組合學路線并不是攻克哥德巴赫猜想的正確思路。因此遲至1960年左右，這類研究逐漸冷了下來。

幸好，傳奇數學家保羅·埃爾德什（Paul Erd?s）在這一領域里持續耕耘。后來陶哲軒等人從他手中接過接力棒，扛起加法數論與組合學的大旗。同時，其它幾個數學領域里不斷提出研究加法結構的需求，以及組合學的進步等因素共同作用，使源于加法數論的組合學思想，成長為獨立的數學分支——加性組合學。雖然加性組合學或許不適于攻克哥德巴赫猜想，但它展示了廣袤的研究前景，蘊藏著豐富的數學內容。

多項式Freiman-Ruzsa猜想的證明，就是最新結出的甜美果實。遺憾的是，這個猜想是非常專業的數學內容，幾乎無法用簡單、清晰的方式解釋給讀者。這里僅能提供一種感性的理解思路。

關于集合的加法，有一個符合經驗的直觀洞見：如果集合A本身擁有很好的代數結構，則A+A的和集的規模（就是元素個數）與A相比，不會太“大”。

由這一觀點出發，數學家Kati Marton應用逆向思維，提出如果A+A的和集足夠小，則我們可以推知A所具有的代數結構。

把上面的思想用數學術語嚴格陳述，可以得到多項式Freiman-Ruzsa猜想：

如果A是一個特征為2的有限域F的子集，滿足|A+A|≤K|A|，其中K是一個常數，那么可通過域上一個不大于A的子群的不超過2*K12個陪集而將A覆蓋于其中（原猜想表述里指數為未知常數，12由最新論文所確定）。陪集的數量很可能非常大。但這是K的多項式，不至于隨K的增大而指數級增長。

Kati Marton懸掛在布達佩斯Renyi學院走廊上的照片。|圖源：Gil Kalai的博客Combinatorics and more: Image (wordpress.com)

Marton是出生于匈牙利的數學家，因其在信息論、concentration of measure（隨機變量取值集中的現象）、概率論和遍歷理論方面的研究而聞名于世。在對concentration of measure研究中，Marton巧妙地引入信息論和熵的概念，獲得了一個簡短的精彩證明。在多項式Freiman-Ruzsa猜想的證明中，類似于上面的熵方法似乎扮演了重要的角色，這一點真是再恰當不過了。

另外值得一提的是，雖然多項式Freiman-Ruzsa猜想是限制在特征為2的有限域上的，但陶哲軒等人認為，他們的方法可以推廣到所有的有限域上（具體論文將在未來發布）。也就是說，多項式Freiman-Ruzsa猜想在所有有限域上都是成立的。

陶哲軒到底用AI做了什么？

還記得前文提及，陶哲軒在去年9-10月期間宣布去學習名為Lean的語言嗎？在他們把證明多項式Freiman-Ruzsa猜想的論文發布在預印本網站arXiv上幾天后，陶哲軒立即著手進行證明的形式化工作——用他花了一個多月學習的Lean語言。

Lean語言的“商標”是L??N，?是數理邏輯里表示“存在”的符號，?則是表示“任意一個”的符號。Lean語言本身是一種函數式編程語言，同時也是定理證明器。它有一個包含已知定理的數據庫Mathlib（目前尚未竣工）。如果把人類撰寫的、符合人類閱讀習慣的證明語句，轉成形式化的機器語言——相當于得到了一個程序，再在電腦上運行該程序，則可以通過運行結果知道原本的證明是否成立！由包含邏輯漏洞和錯誤的證明轉化的程序，在運行時會報錯。

陶哲軒正是打算形式化自己團隊的證明，把它轉為可運行的程序以校驗其正確與否。他以協作的方式展開了這個項目，利用在線軟件源代碼托管服務平臺GitHub來統籌全球25位志愿者的工作。在此過程中，他們使用了名為Blueprint的管理工具。工具由巴黎薩克雷大學的數學家Patrick Massot開發。功能包括將陶哲軒所表達的“數學式英語”轉換成計算機代碼。Blueprint 還具備多種功能，其中之一就是創建一張圖表，用以呈現證明中涉及的各種邏輯步驟。一旦這個圖表中所有的氣泡變成陶哲軒所形容的“可愛的綠色”，團隊的工作就算完成了。

12 月 4 日時還剩下一個小定理（圖中藍色對象框）未被形式化。|圖源：
teorth.github.io/pfr/blueprint/

12月5日，Gowers宣布，關系對象圖里的氣泡框統統化為了綠色。這意味著，他們的證明經形式化和上機運行后，得以確認無誤。

這件事或許會顛覆現有數學界的研究面貌。Lean技術開源社區最重要的推廣者、倫敦帝國理工學院的Kevin Buzzard 表示：“從根本上來說，顯而易見的是，當你將某些東西數字化時，你就可以以新的方式使用它。我們將把數學數字化，這會讓數學變得更好?！?/p>

要知道，越是重要的論文，審稿時間則會越久。在現代數學史上，目前最重要的兩篇論文分別是證明費馬大定理那一篇和證明龐加萊猜想的那一篇。前者的總審稿時間長達2年，而后者更是經歷了總時長7年的反復審查（因佩雷爾曼的證明過程過于簡略）。

本文開頭曾提及2023年有大量組合學方向上的突破性進展。其中針對拉姆齊問題的杰出論文公布于3月份，然而直到9月份，人工審稿仍未完成！

但是，陶哲軒等人的全新論文，其分量大致與3月份這篇相當。但在公布2周后，我們就已然可以確認，它是正確的。這意味著借助Lean語言形式化證明，可以節省大量的時間與人力成本。

陶哲軒們更大的野心

如果再往深里思考：學術期刊的存在意義是什么？

一家好的期刊，可以提供權威性，而權威性又來自于期刊會審校自己刊發的論文，使論文的正確性有所保障。但人工審校的可靠性并不高。實際上，與機器輔助證明相比，人類犯錯誤的可能性是算法的1000倍。如果以Lean為代表的，可將數學證明形式化的編程語言被大規模使用，那數學期刊的存在意義就會被大幅削弱，甚至不再需要數學期刊。

讓我們暢想一下未來。數學家只需把論文發布在網上（如arXiv等平臺），后面附上論文形式化后得到的代碼，其他人就可以輕易地驗證論文里的證明是否正確無誤，從而迅速接受或拒絕這篇論文。甚至以后用于傳播和保存的正是代碼本身，當我們閱讀論文的時候，可以通過“反編譯”手段，把代碼轉為人類可讀的文字。從此，作為學術交流中樞的數學期刊將不再是必要的，而是成了某種學術收藏品的概念，同時因為審稿成本近乎為0，期刊的價格也應大幅降低。同時，書寫習慣還會反過來作用于我們的思考方式。陶哲軒在形式化的工作結束之后表示：“我最近幾天，每次想要表達的時候，潛意識里都會想著如何以一種更便于形式化的方式闡述和論證?！彼恢肋@會不會成為一種習慣，但樂于長期觀察，看看語言方式對思維的影響。

上面關于期刊的部分，絕非筆者個人一廂情愿的幻想。仔細考察當前數學界兩位最活躍的領導者——陶哲軒與Gowers——對數學期刊的一貫態度，就能窺探到他們所樂見并親力推動的未來。

他們一貫支持開源和公平的學術出版模式，反對商業出版社的壟斷和高昂的訂閱費用。他們倡導論文開源的理念，認為學術成果應該免費地分享給所有的讀者。

陶哲軒和Gowers在2012年還曾發起針對商業出版社Elsevier的抵制運動，號召數學家不要向Elsevier旗下的期刊投稿、審稿或編輯，也不要購買或閱讀Elsevier的期刊。他們支持開源期刊的發展。開源期刊通常采用開放獲取的許可協議，允許讀者自由地下載、復制、分發、引用、修改和使用期刊上的文章。陶哲軒和Gowers還是一些開源期刊的創始人。

讀到這里，大家應該也猜到了，陶哲軒與Gowers這一次把自己的證明形式化，絕非一時心血來潮，而是一次有預謀的無聲呼吁：他們認為這是一個時代的契機——去商業學術期刊化的契機。AI浪潮席卷而過，為他們沖刷出另一條學術交流之路。

總而言之，在未來，數學界內部的交流方式，新定理的認可速度，論文的寫作和獲取方式，數學證明的表達規范，都將與現在不同。

當然這也和數學自身和數學證明的特性有關。諸如歷史這樣的學科，或者實驗性的學科，是無法把論文形式化的。

或許，抗拒這一潮流的唯一內源性力量是，形式化論文本質上是把部分審稿成本轉移到論文作者的身上——我們為了向學界“自證”，就需要再掌握一門編程語言Lean（或未來取代它的語言），并且要花時間形式化自己的數學論文。但是，在2022年以后，似乎學習使用新的編程語言不再是什么沉重的負擔。因為大語言模型的出現，現有AI在其它方面或許幫助有限，但是在輔助編程方面，則可以帶來極高的增益。而隨著相關技術的進步。這種AI助手只會越來越強。同時，相關語言，如Lean也會迭代得更加靈活，方便。

未來的發展，無論是計算機輔助證明工具，還是各類型的AI，最終目標都是對數學定理的自動化證明?，F在的Lean本質上還是一種傳統的計算機輔助證明工具，其核心是形式化證明。它不是當前主流的生成式AI和CoT（思維鏈）可自動推理的大語言模型。形式化證明的概念已經存在很久了，與基于大模型和生成式方法的當前人工智能是完全不同的概念。當然，即便是后者，目前也無法獨立完成真正意義上的數學證明。在將Lean語言與AI結合的過程中，除非有一天AI能夠創造性地自動完成Blueprint和Lean中的關鍵創造性步驟，否則我們也無法將這種工具稱為具備數學能力的人工智能。

未來有太多的可能性，而現在局勢已然明了的部分則是，Lean或某個取代它的后繼語言，代表著數學研究與論文寫作的未來。

Lean的最新版本是Lean 4。它的目標是提供一個高效、可擴展、可靠的平臺，用于形式化數學、驗證軟件和硬件，以及開發通用的函數式程序。我在這里分享一本開源教程Mathematics in Lean（鏈接見參考資料6）。

參考資料

1. [2311.05762] On a conjecture of Marton (arxiv.org)

2. Marton’s “Polynomial Freiman-Ruzsa” Conjecture was Settled by Tim Gowers, Ben Green, Freddie Manners and Terry Tao ? Combinatorics and more ? Reader — WordPress.com

3. Additive Combinatorics | Van Vu (yale.edu)

4. On a conjecture of Marton | What's new (wordpress.com)

5. ‘A-Team’ of Math Proves a Critical Link Between Addition and Sets | Quanta Magazine

6. Mathematics in Lean (leanprover-community.github.io)：https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf

本文受科普中國·星空計劃項目扶持

出品：中國科協科普部

監制：中國科學技術出版社有限公司、北京中科星河文化傳媒有限公司

特 別 提 示

1. 進入『返樸』微信公眾號底部菜單“精品專欄“，可查閱不同主題系列科普文章。

2. 『返樸』提供按月檢索文章功能。關注公眾號，回復四位數組成的年份+月份，如“1903”，可獲取2019年3月的文章索引，以此類推。

版權說明：歡迎個人轉發，任何形式的媒體或機構未經授權，不得轉載和摘編。轉載授權請在「返樸」微信公眾號內聯系后臺。