遮天,神墓辰东小说,我欲封天耳根小说零

正是包括兩位菲爾茲獎獲得者在內四位數學家的堅持，才得以證明了一個堪稱「加性組合學圣杯」的猜想，其中 AI 輔助證明起到了不可磨滅的作用。

12 月 5 日，著名數學家、菲爾茲獎獲得者陶哲軒在社交網絡宣布：對多項式 Freiman-Ruzsa 猜想（PFR）的證明進行形式化的 Lean4 項目成功完成，并且耗時僅三周時間，其依賴圖的全部節點都帶上了「可愛的綠色陰影」。

Lean 編譯器也報告該猜想符合標準公理，可以說這是計算機和 AI 輔助證明的一項巨大成功。

但多項式 Freiman-Ruzsa 猜想究竟是什么？為什么對該猜想的證明不僅是一個數學問題，而且對計算機科學也很重要？量子雜志近日報道了這項成就不凡的數學證明及其令人驚嘆的形式化工作，并在文中對多項式 Freiman-Ruzsa 猜想的提出和證明歷程進行了梳理與科普。

總結起來：四位著名數學家（包括兩位菲爾茲獎獲得者）證明了一個堪稱「加性組合學圣杯」的猜想。在一個月的時間內，陶哲軒領導的一個松散的合作團隊通過計算機輔助證明進行了驗證。

下面就進入他們的故事吧。

在一個隨機選取的數值集合中，加法可能會如野火蔓延，勢不可擋。

對于這樣一個集合，如果將其中每兩個數加起來，就會得到一個新的列表并且其中所含的數值將遠遠多于一開始的集合。如果一開始的集合有 10 個隨機數，那么新的列表（稱為和集）會有大約 50 個元素。如果一開始是 100 個隨機數，那么和集中可能會有大約 5000 個元素；而如果初始有 1000 個數，那么和集會有 50 萬個數。

但如果初始集合有結構，則和集中的數會少得多。假設有另一個包含 10 個數的集合：這些數都是 2 到 20 之間的偶數。由于不同的一對數可能會得到相同的求和結果（比如 10+12=8+14=6+16），因此和集只會有 19 個數，而非 50 個。當初始集合變得越來越大時，這一差異也會越來越顯著。一個由 1000 個數構成的結構化列表的和集可能僅會有 2000 個數。

1960 年代，數學家 Gregory Freiman 開始研究和集較小的集合，以探究加法和集合結構之間的聯系 —— 這是定義加性組合學（additive combinatorics）這一數學領域的一個關鍵聯系。Freiman 取得了出色的進展，他證明：一個和集較小的集合必然被包含在一個更大的集合內并且這個更大集合的元素具有高度規則的模式。但自那以后，這一領域就停滯不前了。「Freiman 最初的證明非常難以理解，以至于沒人能真正確定它到底是不是正確的。因此它沒有產生應有的影響。」法蘭西公學院和劍橋大學的數學家 Timothy Gowers 說，他也是一位菲爾茲獎獲得者，「但后來 Imre Ruzsa 突然出現了。」

Ruzsa 在 1990 年代通過兩篇論文用一套優雅的新論證重新證明了 Freiman 定理。幾年之后，一位頗具影響力的匈牙利數學家 Katalin Marton（已于 2019 年去世）探究了一個問題：小的和集能夠揭示出原始集合的結構的哪些方面？她替換了該集合中出現的元素的類型與數學家應當找尋的結構的類型，并認為這能讓數學家提取出更多信息。Marton 的猜想與證明系統、編碼理淪和密碼學存在關聯，并且在加性組合學領域具有崇高的地位。

Katalin Marton

她的猜想「感覺是我們之前無法理解的最基本的東西之一。」牛津大學數學家 Ben Green 說，「它就是我關心的很多事情的基礎。」

Green 與 Gowers、加利福尼亞大學圣迭戈分校的 Freddie Manners 以及加利福尼亞大學洛杉磯分校的一位菲爾茲獎獲得者陶哲軒（Terence Tao）組成了一個團隊。以色列數學家和博主 Gil Kalai 將其稱為 A-team，也即數學家精英團隊。他們在 11 月 9 日發布的論文《On a conjecture of Marton》中證明了該猜想的一個版本。

論文地址：https://arxiv.org/pdf/2311.05762.pdf

未參與該研究的萊斯大學數學家 Nets Katz 描述說這份證明「簡單直接得堪稱美麗」，并且「多少算是完全出乎意料」。

然后陶哲軒開始通過 Lean 來形式化該證明。Lean 是一種可幫助數學家驗證定理的編程語言。不過幾周時間，他就成功完成了。12 月 5 日星期二一早，陶哲軒宣布 Lean 已經完成對該猜想的證明，并且沒有任何 sorry。sorry 是 Lean 中一個標準陳述，表示計算機無法驗證某個特定步驟。這是自 2021 年以來這樣的證明工具最亮眼的成就，并成為了數學家編寫證明的方式的轉折點，也就是開始以計算機能理解的方式編寫證明。Gowers 說：如果這些工具變得很容易，能讓數學家輕松使用，那么它們就可能替代往往耗時漫長且繁重艱巨的同行評審過程。

這一證明的組分已經醞釀了數十年時間。Gowers 在 2000 年代構想了它的前幾步。但還要另外 20 年，Kalai 所稱的領域「圣杯」才得以證明。

群

為了理解 Marton 猜想，熟悉群（group）的概念會很有幫助。簡單來說，群是由集合和運算構成的數學對象。這里我們假設有整數集（一個包含無限個數的集合）和加法運算。我們每次將兩個整數相加，便會得到另一個整數。加法也服從其它一些群運算規則，比如結合律，也就是可以交換運算的順序：3 + (5 + 2) = (3 + 5) + 2.

在一個群內，你有時候可以找到滿足該群所有性質的較小集合。舉個例子，任意兩個偶數相加會得到另一個偶數。偶數本身就是一個群，這讓其成為了整數的子群（subgroup）。而奇數卻不一樣，它并非一個子群。如果你將兩個奇數加到一起，則會得到一個偶數 —— 這不在原來的集合中。但只需讓每個偶數都加 1，便能得到所有奇數。像這樣的有移位（shift）的子群稱為陪集（coset）。陪集并不具備子群的所有性質，但它又能保留子群在許多方面的的結構。舉個例子，奇數和偶數一樣是均勻分布的。

Timothy Gowers

Marton 猜想如果有一個由群元素組成的集合 A，其和集并不比 A 本身大很多，那么就會存在某個具有一個特殊性質的子群 G。對 G 執行幾次移位可以得到一些陪集，而這些陪集組合起來就會包含原始集合 A。此外，她認為陪集的數量并不會比和集的大小增長更快 —— 她相信這應該是一個多項式關系，而非遠遠更快的指數級增長。

這個研究方向聽起來可能好像就是為了滿足好奇心，似乎沒什么實際用途。但由于它和一個了解子群的總體結構的簡單測試（將集合中的兩個元素加起來會發生什么？）有關，所以對數學家和計算機科學家來說就非常重要了。當計算機科學家想要使得加密消息一次只能被解碼一部分時，也會遇到這個想法的廣義版本。它也會出現在概率可檢驗證明（probabilistically checkable proof）中 —— 這種證明形式讓計算機科學家可以通過檢驗少量孤立的信息來執行驗證。

對于上述的每種情況，你只需要研究一個結構中的一些點，就能得出與一個更大更高層結構有關的結論；比如只需解碼一個長消息中的少量比特或驗證一個復雜證明的一小部分。

牛津大學的 Tom Sanders（他以前是 Gowers 的學生，現在是 Gowers 的同事）說：「你要么可以假設一切都是一個群的一個大子集，要么可以從許多附加巧合的存在中得到你想要的一切。這兩種觀點都很有用。」

Ruzsa 在 1999 年發表了 Marton 猜想，并充分說明了她的貢獻和成就。「她獨立于我和 Freiman 得出了這個猜想，而且可能先于我們。」他說，「也因此，在我和她交談過之后，我決定用她的名字來命名這個猜想。」盡管如此，數學家現在還是將其稱為多項式 Freiman-Ruzsa 猜想，簡稱 PFR。

零和一

和許多數學對象一樣，群也有很多不同的形式。Marton 猜測她的猜想對所有群都成立。這一點還有待證明。這篇新論文證明其對某一特定類型的群成立，這類群的元素是 (0, 1, 1, 1, 0) 這樣的二進制數列表。由于計算機的工作過程就基于二進制，因此這個群對計算機科學至關重要。但它也對加性組合學很有用。「它就像是一個玩具設置，你可以在其中玩耍，嘗試各種東西。」Sanders 說，「這里的代數操作起來比非負整數（whole number）容易太多了。」

陶哲軒

這些列表的長度是固定的，而且每一位都要么為 0，要么為 1。這樣的兩個列表相加就是將一個列表的每一項與另一列表的對應項相加，規則包括 1 + 1 = 0。那么 (0, 1, 1, 1, 0) + (1, 1, 1, 1, 1) = (1, 0, 0, 0, 1)。PFR 試圖搞清楚：如果一個集合算不上是子群，但具有某些類似群的特征，那么這個集合看起來會是什么樣。

為了更清楚地說明 PFR，請想象一下你有一個二元列表構成的集合 A。現在從 A 中取出每一對元素并相加。所得到的和可構成 A 的和集，記為 A+A。如果 A 中的元素是隨機選取的，那么大部分的和都彼此不同。如果 A 有 k 個元素，那就意味著和集有 k2/2 個元素。當 k 很大時（比如 1000），k2/2 就會比 k 大很多。但如果 A 是一個子群，那么 A+A 的每個元素都在 A 中，這就意味著 A+A 的大小和 A 本身是一樣的。

PFR 考慮的集合不是隨機的，但也不是子群。在這些集合中，A+A 的元素數量會有些小，比如 1 萬或 10 萬。加利福尼亞大學圣迭戈分校的計算機科學家 Shachar Lovett 說：「當你的結構概念比僅僅作為精確的代數結構豐富得多時，這真的會很有用。」

就數學家所知，所有服從這一性質的集合「都相當接近于真正的子群。」陶哲軒說，「這是一個直覺認識，也就是沒有其它類型的假群存在。」Freiman 在其原研究成果中證明了這一命題的一個版本。1999 年時，Ruzsa 將 Freiman 定理從整數擴展到了二元列表設置。他證明，當 A+A 的元素數量是 A 的大小的常數倍時，A 必定被包含在一個子群內。

但 Ruzsa 定理需要子群非常巨大才行。Marton 的見解是假定 A 不是包含在一個巨大的子群中，而是可以包含在一個子群的多項式數量的陪集中并且這個子集不大于原始集合 A。

好想法看一眼就知道

千年之交那段時間，Gowers 在研究與包含均勻相間的字符串的集合相關的另一問題時看到了 Ruzsa 對 Freiman 定理的證明。「我就需要這樣的東西，差不多就是從有關一個特定集合的松散得多的信息中獲取結構化信息。」Gowers 說，「我非常幸運，就在那不久前，Ruzsa 剛給出這個美不勝收的證明。」

Freddie Manners

Gowers 開始著手嘗試證明該猜想的多項式版本。他的想法是先從和集相對較小的集合 A 開始，然后逐漸操作 A，將其變成一個子群。如果他能證明所得子群與原始集合 A 相似，他就可以輕松斷定這個猜想是正確的。Gowers 將這個想法分享給了自己的同事，但沒人能將其轉化成完整的證明。盡管 Gowers 的策略能成功處理一些情況，但在其它情況中，這種操作卻會讓 A 更加遠離多項式 Freiman-Ruzsa 猜想的預期結論。

最終，該領域放棄了這一思路。2012 年，Sanders 幾乎證明了 PFR。但他需要的移位子群的數量高于多項式水平，盡管只高一點點。Gowers 說，「一旦他做到了，就意味著這事件變得不那么緊迫了，但這仍然是一個我非常喜歡的好問題。」

但 Gowers 的想法依然留存在他同事的記憶和硬盤中。「那是一個真正的好想法。」Green 說，他也曾是 Gowers 的學生，「好想法看一眼就知道。」今年夏季，Green、Manners 和陶哲軒終于將 Gowers 的想法從煉獄中解放了出來。

在決定研究已有 20 年歷史的 Gowers 想法之前，Green、陶哲軒和 Manners 的合作成果已經可以羅列 37 頁之長。在 6 月 23 日的論文《Sumsets and entropy revisited》中，他們成功使用了概率論中的「隨機變量」概念來探測具有小和集的集合的結構。通過這種切換，該團隊可以更巧妙地操作集合。「處理隨機變量在某種程度上比處理集合要簡單得多。」Manners 說，「對于隨機變量，我可以稍微調整其中一個概率，而這就可能會給我一個更好的隨機變量。」

從這個概率角度入手，Green、Manners 和陶哲軒可以不用再面對一個集合的元素數量，而是可以去衡量一個隨機變量中所包含的信息，這個量被稱為熵（entropy）。對加性組合學來說，熵并不是新東西。事實上，陶哲軒在 2000 年代末就嘗試過推廣這一概念。但還沒有人試過將其用于多項式 Freiman-Ruzsa 猜想。Green、Manners 和陶哲軒發現它很強。但他們仍然不能證明該猜想。

Ben Green

當這個研究團隊仔細研究他們的新成果時，他們意識到終于建立了一個可讓 Gowers 那蟄伏的想法重獲新生的環境。如果使用集合的熵來衡量集合的大小，而不是元素數量，則其技術細節可能會好處理得多。「某一時刻我們意識到，比起我們當時正在嘗試的思路，這些來自 Tim 的 20 年前的舊想法實際上更可能有效。」陶哲軒說，「于是我們把 Tim 帶回了這個項目。然后所有的碎片都出人意料地很好地拼合在了一起。」

盡管如此，在給出完整的證明前，還有很多細節要處理。「我們四個人都還各自忙著其它事，這是有點愚蠢的。」Manners 說，「你希望發表這個偉大的結果并且告訴全世界，但你實際上還依然必須要去寫期中報告。」最終，這個團隊堅持了下來，并于 11 月 9 日發表了論文。他們證明，如果 A+A 不大于 A 的大小的 k 倍，那么可通過一個不大于 A 的子群的不超過 k12 移位而將 A 覆蓋其中。這個移位的數量很可能非常大。但這是一個多項式，不會隨 k 的增大而指數級增長；而如果 k 在指數中就會這樣。

幾天之后，陶哲軒開始形式化該證明。他以協作的方式運行了這個形式化項目，使用了版本控制軟件包 GitHub 來協調來自全球 25 個志愿者的貢獻。他們使用了一種名為 Blueprint 的工具。這個工具是巴黎薩克雷大學數學家 Patrick Massot 開發的，可用于協調組織將陶哲軒所說的「數學式英語」翻譯成計算機代碼的工作。Blueprint 的功能有很多，其中之一是創建一張圖表來描述證明中涉及的各種邏輯步驟。一旦圖中所有氣泡都變成陶哲軒所說的「可愛的綠色陰影」，這個團隊就算完工了。