陶哲軒發起的「眾包」數學研究項目終于快要迎來勝利時刻！

大約在三周前，陶哲軒提出了一個眾包項目，結合專業和業余數學家、自動定理證明器、AI 工具和證明輔助語言 Lean， 來描述與 4694 條 magma（原群） 方程定律相關的蘊含圖，這些定律可以使用最多四次 magma 操作調用來表達。也即，需要確定這 4694 條定律之間可能蘊含的的真假。

該項目已運行 19 天，從已解決的原始蘊含的角度來看，該項目（截至撰寫本文）已完成 99.9963%：待解決的蘊含中，已被證明為真，已被證明為假，只有懸而未決。盡管在這個集合中，也有蘊含推測為假，但可能很快就正式反駁。

出于編譯效率的原因，他們沒有在 Lean 中記錄這些推測中的每一個證明；只在 Lean 中證明一組較小的蘊含，然后通過傳遞性來暗示一組更廣泛的蘊含（例如，使用以下事實：如果方程 X 蘊含方程 Y，且方程 Y 蘊含方程 Z，則方程 X 蘊含方程 Z）；他們還將很快利用蘊含圖的對偶對稱性實現進一步簡化。

除了感謝眾多志愿者為該項目付出的不懈努力，陶哲軒表示現在擁有許多出色的可視化工具來檢查（尚未完成的）蘊含圖的各個部分。例如，下圖描繪了方程 1491：的所有結果，陶哲軒將其昵稱為「Oberlix 定律」（它有一個「同伴」——Asterix 定律，即方程 65：）。

下面是正在研究的所有方程定律的表格，以及它們蘊含或被蘊含的定律數量。這些界面也與 Lean 有某種程度的集成：例如，你可以單擊來嘗試證明 Oberlix 定律蘊含方程 359，；陶哲軒將此留作一個挑戰（Lean 中可以進行四行證明）。

過去幾周，陶哲軒了解到其中許多定律以前都出現在文獻中，并在下圖項目中對這些方程進行介紹。例如，除了非常著名的交換律（公式 43）和結合律（公式 4512）之外，一些方程（比如公式 4、公式 29、公式 381、公式 3722 和公式 3744）出現在一些 Putnam 數學競賽中；公式 168 定義了一個有趣的結構，被稱為「中心群」，學者 Evans 和 Knuth 對其進行了研究，并成為 Knuth-Bendix 完成算法的主要靈感來源；公式 1571 對指數為 2 的阿貝爾群進行了分類。

方程匯總地址：https://github.com/teorth/equational_theories/wiki/Tour-of-selected-equations

陶哲軒表示 Birkhoff 完備定理起了大作用，如果一個方程定律蘊含另一個，那么可以通過有限次數的重寫操作來證明，但是所需要的重寫次數可能相當長。上面提到的從 方程 1491 推導出 359 的蘊含已經相當有挑戰性，需要重寫四五次；從方程 1681 推導出 2 的蘊含非常長。盡管如此，標準自動定理證明器（例如 Vampire）完全能夠證明這些蘊含中的絕大多數。

更微妙的是反蘊含，他們必須證明一條定律 X 并不蘊含另一條定律 Y。原則上，他們只需展示一個服從 X 但不服從 Y 的 magma。在很大一部分情況下，他們可以簡單地搜索小的有限 magma（例如兩個、三個或四個元素的 magma）來獲得這種反蘊含。但它們并不總是足夠的，事實上，他們知道只有通過構造無限的 magma 才能證明反蘊含。

例如，現在已知「Asterix 定律」并不蘊含「Oberlix 定律」，但所有反例必然是無限的。奇怪的是，已知的構造與集合論中著名的強迫技術有某種相似之處，因為他們不斷地將「通用」元素添加到（部分）magma 中， 以強迫存在具有某些特定屬性的反例，盡管這里的構造肯定比集合論的構造簡單得多。

他們還從交換和非交換環中的「線性」magma 構造中獲得了可觀的收益，比如與「合流」方程定律相關的自由 magma，以及更普遍的具有完整重寫系統的定律。因此，未解決的蘊含數繼續穩步減少，不過還沒有到宣布該項目勝利的時候。

雖然該項目仍在進行中，但陶哲軒對迄今為止取得的進展感到非常滿意，而且對該項目的許多希望已經實現。

在科學方面，他們發現一些新技術和構造，可以證明給定的方程理論并不蘊含另一個方程理論，并且還發現一些奇特的代數結構， 如「Asterix」和「Oberlix」，它們具有有趣的特征。除了此處進行系統搜索之外，其他任何方式都可能無法發現它們。參與者非常多樣化，包括各個職業階段的數學家和計算機科學家、以及感興趣的學生和業余愛好者。Lean 平臺在整合人類生成和機器生成的貢獻方面效果很好，后者在是迄今為止最大的貢獻來源，但許多自動生成的結果首先由人類在特定情況下獲得，然后被泛化和形式化（通常由項目的不同成員完成）。

他們仍在提出許多非正式的數學論證，但它們往往在 Lean 中被迅速形式化，此時關于正確性的爭議就會消失，從而專注如何最好地部署各種經過驗證的技術來解決剩下的問題。

也許陶哲軒目前唯一期待但尚未看到現代 AI 工具的重大貢獻，它們正在以多種次要方式應用于該項目，例如通過 GitHub Copilot 等工具來加速編寫 Lean 證明、LaTeX 藍圖和其他軟件代碼。此外一些可視化工具也主要使用 Claude 等大型語言模型共同編寫。

對于解決蘊含這一核心任務，更「老式」的自動定理證明器迄今為止已被證明更為優越。然而，剩余 700 個左右蘊含中的大多數都不適合這些舊工具，尤其涉及 Asterix 和 Oberlix 的蘊含讓人類合作者困惑了好幾天。所以仍然希望看到現代 AI 在完成剩余蘊含中最難、最頑固的部分發揮更積極的作用。

博客地址：https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/