編輯：桃子 好困
【新智元導讀】 AI已完全融入數學家的工作流中。陶哲軒剛剛宣布，最新方程式理論專案已完成99.9963%，眾包之力外加AI輔助取得了重大成績。他認為，剩余大約700個讓人類頭疼的難題，AI或許更有潛力。
AI，已成為費斯獎得主最得心應手的工具。
大約三周前，陶哲軒提出了一個協作專案——
結合專業和業余數學家、自動定理證明器、AI工具，以及證明輔助語言Lean，來描述與4694條 幺半群 （magmas）方程式定理定理相關的蘊含圖。
這些定理最多可以使用，四次幺半群運算來表達。
也就是說，需要確定4694條定理之間可能存在4694 * (4694 - 1) = 22028942蘊含的關系真偽。
地址：https://github.com/teorth/equational_theories/blob/main/data/equations.txt
這一專案在9月25日釋出當天便啟動了，如今，已經緊鑼密鼓進行了19天。
剛剛，陶哲軒公布了專案的最新進展：
從已解決原始蘊含關系角度來看，截至目前，專案進度已完成99.9963%。
在需要解決的22028942個蘊含關系中，8178279個被證明為真，13854531個被證明為假，只有826個仍未解決。
而且，專案每一天的進展，他都記錄到了個人日誌中。
一起看看，陶哲軒如何透過「眾包方式」，探索數學新領域。
方程式理論專案，進度99.99%
在集合中，有249個蘊含關系推測為假，並且很快就證明了是假的。
出於編譯效率的考量，他們並沒有在Lean中記錄每一個證明，只在其中證明了一個較小的592790個蘊含關系集合，然後透過傳遞性推匯出更廣泛的蘊含關系集合。
例如，利用如果方程式X蘊含方程式Y，方程式Y蘊含方程式Z，那麽方程式X蘊含方程式Z的事實。
他們還很快利用蘊含圖對偶對稱性，對其進一步簡化。
經過專案誌願者的不懈努力，陶哲軒稱現在有了很多出色的 視覺化工具 （尚未完成的），來檢查蘊含圖的各個部份。
比如，如下這張圖描述了方程式1491：x = (y ◇ x) ◇ (y ◇ (y ◇ x ))的所有結果。
陶哲軒將其稱之為「Obelix law」。它還有一個夥伴Asterix law，即方程式65：x = y ◇ (x ◇ (y ◇ x ))。
如下是，他們正在研究的所有方程式定理的表格，以及它們蘊含/被蘊含定理數量。
地址：https://teorth.github.io/equational_theories/implications/
這些界面也在某種程度上與Lean整合。
比如，我們可以點選檢視Obelix law蘊含方程式359，陶哲軒將其作為題目，讓大家進行挑戰。他暗示，在Lean中僅用4行就可以完成證明。
在過去的幾周裏，他還了解到這些定理中，有許多之前已經出現在文獻中。
由此，這裏編制了這些方程式的「導覽」。
地址：https://github.com/teorth/equational_theories/wiki/Tour-of-selected-equations
例如，除了眾所周知的交換律（方程式43）、結合律（方程式4512）之外，一些方程式（方程式14、方程式29、方程式381、方程式3722、方程式3744）曾出現在一些Putnam數學競賽中；
方程式168定義了一個引人入勝的結構，被稱為「中心幺半群」（central groupoid）。特別是，由Evans和Knuth研究過，並且是Knuth-Bendix完成演算法的關鍵靈感來源；
而方程式1571則對指數為二的阿貝爾群（abelian groups）進行了分類。
根據Birkhoff完備性定理，如果一個方程式定理蘊含另一個，那麽它可以透過有限次重寫操作來證明。
不過，所需的重寫次數可能相當長。
上面提到的1491蘊含359的證明已經相當具有挑戰性，需要四到五次重寫。
另外，方程式1689蘊含方程式2的證明，更是極其冗長。盡管如此，標準的自動定理證明器，如Vampire，完全有能力證明絕大多數這些蘊含關系。
更微妙的是反蘊含關系，在這種情況下必須證明定理X不蘊含定理Y。原則上，只需要展示一個遵循X但不遵循Y的幺半群即可。
在很大一部份情況下，他們可以簡單地搜尋小型有限幺半群——比如兩個、三個或四個元素的幺半群——來獲得這種反蘊含關系。
但這些並不足夠，事實上，他們只知道有些反蘊含關系，只能透過構造無限幺半群來證明。
比如，現在已知的Asterix law不蘊含Obelix law，但所有反例必然是無限的。
有趣的是，已知的構造方法與集合論中著名的forcing技術有一些相似之處，即不斷向（部份）幺半群添加「通用」元素，以forcing存在具有某些特定內容的反例。
不過，這裏的構造肯定比集合論構造簡單得多。
他們還從「線性」幺半群x ◇ y = ax + by構造中取得了有益的進展。這些構造存在於 交換環 和非交換環中。
與「匯聚」（confluent）方程式定理相關的自由幺半群，以及更普遍的具有完整重寫系統的定理。
因此，未解決的蘊含關系數量繼續穩步減少。
遵循標準GitHub實踐，論文很快上線
經過相當繁忙的後端設定和「滅火」（putting out fires）工作後，專案現在執行得相當順利。
專案在Lean Zulip頻道上協調，所有貢獻都透過GitHub上的拉取請求（pull request）過程進行，並透過基於問題的GitHub專案進行跟蹤。
另外兩位維護者Pietro Monticone、Shreyas Srinivas為其提供了寶貴的監督。
與之前的 PFR 形式化專案相比，這次專案的工作流程遵循了標準的GitHub實踐，大致如下：
如果在Zulip討論過程中，明確需要完成某些特定任務以推進專案（比如，在Lean中形式化討論執行緒中已經推匯出的蘊含關系證明），就會建立一個「問題」（通常由陶哲軒自己或其他維護者建立），其他貢獻者可以「認領」這個問題，單獨工作（使用主GitHub倉庫的本地副本）。
然後送出「拉取請求」將他們的貢獻合並回主倉庫。這個請求隨後可以由維護者和其他貢獻者審查，如果獲得批準，就會關閉相關問題。
更廣泛地說，他們正努力記錄這個設定中的所有過程和經驗教訓。
這將成為即將發表的關於這個專案的論文的一部份，現正處於初步規劃階段，可能會包括數十位作者。
陶哲軒表示，自己對專案取得的進展非常滿意，而且許多最初的期望已經實作。
在科學方面，他們發現了一些新的技術和構造，用來證明一個給定的方程式理論不蘊含另一個；他們還發現了一些具有有趣特征的奇特代數結構，如Asterix和Obelix對，是透過系統性搜尋方式被發現的。
參與者方面，非常多樣化，從各個職業階段的數學家、電腦科學家，到感興趣的學生和業余愛好者。
此外，Lean平台在整合人工生成和機器生成的貢獻方面表現良好。
機器生成在數量上是迄今為止最大的貢獻來源，但許多自動生成往往是基於人類最初在特殊情況下發現的，然後由專案的不同成員進行推廣和形式化。
在討論執行緒中，他們還進行了許多非正式的數學論證，但這些論證往往會迅速在Lean中形式化，消除了關於正確性的爭議就。
進而，研究人員可以轉而專註於如何最好地部署各種經過驗證的技術，來解決剩余的蘊含關系。
AI並未做出重大貢獻
原本，陶哲軒期待看到現代AI工具，能夠在專案中做出重大貢獻。
但實際上，它們以一種輔助、次要的方式被使用。
比如，透過 GitHub Copilot 等工具來加速編寫Lean證明、LaTeX文件框架、其他軟件程式碼。
此外，他們的幾個視覺化工具，也主要是使用Claude等大模型共同編寫的。
然而，對於解決蘊含關系這一核心任務，更「傳統」的自動定理證明器表現更好。
不過，目前剩余的大約700個蘊含關系，大多數不適合使用傳統工具來處理。
有幾個蘊含關系（特別是涉及Asterix和Obelix那些），已經讓人類專家困惑多日。
陶哲軒認為，在解決剩余的、更困難的蘊含關系時，現代AI可能會發揮更重要的作用。
參考資料：
https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/
