陶哲軒全網懸賞「最強大腦」！AI+人類顛覆數學難題？凡爾賽網友已下場

新智元報道

編輯：Aeneas 好睏

【新智元導讀】最近，陶哲軒向廣大網友和數學愛好者發起了挑戰：大衆數學愛好者、證明助理、自動化助手和AI聯合起來，是否可以證明擴展幾個數量級的數學問題？

想參加陶哲軒發起的「衆包」數學研究項目嗎？

機會來了！

AI輔助證明數學研究，越來越可行了

他們每個人都對項目的各方面都足夠熟悉，可以驗證彼此的貢獻。

但如果要組織起更大規模的數學研究項目，特別是涉及公衆貢獻的項目，就麻煩多了。

原因在於，很難驗證所有人的貢獻。

2023年底，陶哲軒宣佈：將多項式Freiman-Ruzsa猜想的證明形式化的Lean4項目，在三週後取得了成功（圖爲最新狀態）

要知道，在數學論證某個部分中的單個錯誤，可能就會使整個項目失敗。

而且，以一個典型數學項目的複雜程度來說，期待具有本科數學教育水平的公衆做出有意義的貢獻，也是不現實的。

由此我們也可以知道，把AI工具納入到數學研究項目中，也是極有挑戰性的。

因爲AI會生成看似合理但實際上毫無意義的論證，因此需要額外驗證，才能將AI生成的部分添加到項目中。

好在，證明輔助語言（比如Lean）提供了潛在的方法，能夠克服這些障礙，並且讓專業數學家、廣大公衆和AI工具的合作成爲可能。

這種方法的前提是，項目可以以模塊化的方式分解成更小的部分，這些部分可以在不必理解整個項目的情況下就能完成。

目前的例子主要有將現有數學結果形式化的項目（比如對Marton最近證明的PFR猜想的形式化）。

這些形式化工作，主要是通過衆包方式由人類貢獻者（包括專業數學家和感興趣的公衆）完成的。

同時，還有一些新興的嘗試，試圖引入更多的自動化工具來完成，後者包括傳統的自動定理證明器，以及更現代的基於AI的工具。

探索全新數學問題，成爲可能

並且，陶哲軒還認爲，這種全新範式不僅可以用於形式化現有的數學，還可以用來探索全新的數學！

過去，他曾經和繼任組織過一個在線協作「Polymath」的項目，就是一個很好的例子。

不過，這個項目沒有將證明輔助語言納入工作流，貢獻就必須由人類主持人管理和驗證，這項工作非常耗時，也限制了將這些項目進一步擴大。

現在，陶哲軒希望，添加證明輔助語言能突破這個瓶頸。

而他尤其感興趣的，就是是否可能使用這些現代工具同時探索一類數學問題，而不是一次只關注一兩個問題。

本質上，這種方法是可模塊化的重複任務，如果有適當的平臺來嚴格協調所有貢獻，衆包和自動化工具可能會尤其有用。

如果用以前的方法，這種數學問題類型是無法擴大規模的。除非在多年時間裡，隨着個別論文慢慢地一次探索一個數據點，直到對這類問題獲得合理的直覺。

此外，如果有一個大型問題數據集，可能有助於對各種自動化工具進行性能評估，並且比較不同工作流程的效率。

在今年7月，第五個忙碌海狸數被證實爲是47,176,870。

一些更早的衆包計算項目，比如「互聯網梅森素數大搜索」（Great Internet Mersenne Prime Search， GIMPS），在內在精神上跟這些項目也有些類似，儘管它們使用的是更傳統的工作量證明機制，而不是證明輔助語言。

陶哲軒表示，很想知道是否還有其他現存的衆包項目探索數學空間的例子，以及是否有可用的經驗教訓。

陶哲軒提出新項目

爲此，陶哲軒自己也提出了一個項目，來進一步測試這一範式。

這個項目受到去年MathOverflow問題的啓發。

不久後，陶哲軒在自己的Mathstodon上，對它進行了進一步討論。

這個問題屬於泛代數（universal algebra）領域，涉及對原羣（magma）的簡單等式理論的中等規模探索。

原羣是一個配備了二元運算 的集合G。

最初，這個運算o沒有附加任何額外的公理，因此原羣本身是較爲簡單的結構。

當然，通過添加額外的公理，如恆等公理或結合律公理，我們可以得到更熟悉的數學對象，例如羣、半羣或幺半羣。

在這裡，我們感興趣的是（無常數的）等式公理。這些公理涉及由運算o和G中的一個或多個未知變量構建的表達式的相等性。

此類公理的兩個熟悉的例子，是交換律x o y = y o x和結合律(x o y) o z = x o (y o z)。

其中x，y，z是原羣G中的未知變量。

另一方面，（左）恆等公理e o x = x在這裡不被視爲等式公理（equational axiom），因爲它涉及一個常數e ∈ G。這類涉及常數的公理在本研究中不予討論。

接下來，爲了闡明自己發起的研究項目，陶哲軒介紹了十一個關於原羣的等式公理例子。

這些等式公理是僅涉及原羣運算和未知變量的等式——

因此，舉例來說，等式7表示交換律公理，而等式10表示結合律公理。

常數公理等式1是最強的，因爲它限制了原羣G最多隻能有一個元素；與之相反，自反公理等式11是最弱的，所有原羣都滿足這一公理。

接下來，我們就可以探討這些公理之間的推導關係：哪些公理能推出哪些公理？

例如，等式1可以推導出這個列表中的所有其他公理，而這些公理又可以推導出等式11。

等式8作爲特殊情況可以推導出等式9，而等式9又作爲特殊情況可以推導出等式10。

這些公理之間完整的推導關係可以用以下哈斯圖（Hasse diagram）來描述：

這一結果特別回答了數學問答網站MathOverflow上的一個問題：是否存在介於常數公理（等式1）和結合律公理（等式10）之間的等式公理（equational axioms）。

值得注意的是，這裡大多數的蘊含關係都很容易證明。然而，其中存在一個非平凡的蘊含關係。

這個關係是在一個與前述問題密切相關的MathOverflow帖子回答中得到的：

命題1：等式4蘊含等式7

證明：假設G滿足等式4，因此

對所有x,y ∈ G成立。

特別是，當y = x o x時，可以得出(x o x) o (x o x) = (x o x) o x。

再次應用（1），可以得出x o x是冪等的：

現在，在（1）中將x替換爲x o x，然後使用（2），可以得出(x o x) o y = y o (x o x)。

尤其，x o x與y o y是可交換的：

此外，通過兩次應用（1），可以得到(x o x) o (y o y) = (y o y) o x = x o y。

因此，（3）就可以簡化爲x o y = y o x，這就是等式7。

上述論證過程的形式化，可以在Lean中找到。

然而值得注意的是，確定一組等式公理是否決定另一組等式公理的一般問題，是不可判定的。

因此，這裡的情況有點類似於「忙碌海狸」挑戰，即在某個複雜點之後，我們必然會遇到不可判定的問題；但在達到這個閾值之前，我們仍有希望發現有趣的問題和現象。

上面的哈斯圖不僅斷言了列出的等式公理之間的蘊含關係，還斷言了公理之間的非蘊含關係。

例如，如圖所示，交換公理等式7並不蘊含等式4公理(x + x) + y = y + x。

要證明這一點，只需找出一個滿足交換公理等式7但不滿足等式4公理的原羣的例子。

比如，在這種情況下，我們可以選擇自然數集N，其運算爲x o y := x+y。

更一般地，該圖斷言以下非蘊含關係，這些關係（連同已指出的蘊含關係）完整描述了這十一個公理之間蘊含關係的偏序集：

在此，陶哲軒邀請讀者提出反例，來完成其中的部分證明。

最難找到的反例，就是等式9無法推出等式8了。

用Lean可以給出解決方案。

另外，陶哲軒還提供了一個GitHub存儲庫，包含了所有上述包含和反包含關係的Lean證明。

可以看出，僅僅計算11個等式的哈斯圖就已經有些繁瑣了。

而陶哲軒提出的項目，是嘗試將這個哈斯圖擴展幾個數量級，覆蓋更大範圍的等式集。

他提議的集合是ε，即最多使用原羣運算o四次的等式集，直到重新標記和等式的自反性和對稱性公理。

這包括了上述十一個等式，但還有更多。

還有多少呢？

回想一下，卡特蘭數C_n是用二元運算o（應用於n+1個佔位符變量）形成表達式的方法數；而給定m個佔位符變量的字符串，貝爾數B_m是爲這些變量分配名稱的方法數（可以重新標記），其中允許某些佔位符被分配相同的名稱。

因此，忽略對稱性，最多涉及四次運算的等式數量是

左側和右側相同的等式數量是

這些都等同於自反公理（等式11）。

剩下的9118個等式由於等式的對稱性成對出現，所以ε的總大小是

陶哲軒表示，自己還沒有生成這樣恆等式的完整列表，但他猜想，使用Python就可以輕鬆完成。

使用AI工具，應該能生成大部分所需的代碼。

他表示，自己完全不清楚ε的幾何結構會是什麼樣子。

大多數等式會彼此不可比較嗎？它會分爲「強」公理和「弱」公理嗎？

現在，陶哲軒的留言區，已經有了幾十條評論。

感興趣的讀者，陶哲軒也向你發出了邀請。

參考資料：

https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/