[新聞] 數學「A隊」證明了加法和集合之間的關鍵

數學「A隊」證明了加法和集合之間的關鍵聯繫 https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/ Leila Sloman 正是包括兩位菲爾茲獎得主在內四位數學家的堅持，才得以證明了一個堪稱「加性組 合學聖杯」的猜想，其中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 的猜 想與證明系統、編碼理淪和密碼學存在關聯，並且在加性組合學領域具有崇高的地位。 圖片 她的猜想「感覺是我們之前無法理解的最基本的東西之一。」牛津大學數學家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）。 陪集並不具備子群的所有性質，但它又能保留 子群在許多方面的結構。 舉個例子，奇數和偶數一樣是均勻分佈的。 圖片 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 剛給出這個美不勝收的證明。 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 和陶哲軒發 現它很強。 但他們仍然不能證明該猜想。 當這個研究團隊仔細研究他們的新成果時，他們意識到終於建立了一個可讓Gowers 那蟄 伏的想法重獲新生的環境。 如果使用集合的熵來衡量集合的大小，而不是元素數量，則 其技術細節可能會好處理得多。 「某一時刻我們意識到，比起我們當時正在嘗試的思路 ，這些來自Tim 的20 年前的舊想法實際上更可能有效。」陶哲軒說，「於是我們把Tim 帶回了這個項目。然後所有的碎片都出乎意料地很好地拼合在了一起。 儘管如此，在給出完整的證明之前，還有很多細節要處理。 「我們四個人都還各自忙著 其它事，這是有點愚蠢的。」Manners 說，「你希望發表這個偉大的結果並且告訴全世界 ，但你實際上仍然必須去寫期中報告。」最終，這個團隊堅持了下來，並於11 月9 日發 表了論文。 他們證明，如果A+A 不大於A 的大小的k 倍，那麼可透過一個不大於A 的子 群的不超過k1 2 移位而將A 覆蓋其中。 這個移位的數量很可能非常大。 但這是一個多 項式，不會隨著k 的增加而指數級增長；而如果k 在指數中就會這樣。 幾天之後，陶哲軒開始形式化證明。 他以協作的方式運行了這個形式化項目，使用了版 本控制軟體包GitHub 來協調來自全球25 個志工的貢獻。 他們使用了一種名為 Blueprint 的工具。 這個工具是巴黎薩克雷大學數學家Patrick Massot 開發的，可用來 協調組織將陶哲軒所說的「數學式英語」翻譯成電腦程式碼的工作。 Blueprint 的功能 有很多，其中之一是創建一張圖表來描述證明中涉及的各種 邏輯 步驟。 一旦圖中所有 氣泡都變成陶哲軒所說的「可愛的綠色陰影」，這個團隊就算完工了。 對PFR 猜想的證明的依賴圖，其中方框是定義，橢圓是定理和引理，全部背景都是綠色說 明該證明已經完全形式化 他們發現論文中存在一些非常小的拼字錯誤—— 在一條網路訊息中，陶哲軒指出：「這 個計畫中與數學最相關的部分的形式化是相對簡單直接的，但技術上『顯而易見』的步驟 反而耗時最長。 Marton 在她的著名猜想得到證明的幾年前去世了，但這個證明幫助彰顯了她在熵和 資訊 理論 領域的畢生成就。 「當使用這個熵框架進行研究，而不是我之前嘗試的框架時，一 切都好了很多。」Gowers 說，「對我來說，這仍然有些神奇。」 -- ※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 114.38.27.129 (臺灣) ※ 文章網址: https://www.ptt.cc/bbs/Math/M.1714741523.A.DF4.html