陶哲軒發(fā)起的「眾包」數(shù)學(xué)研究項(xiàng)目終于快要迎來勝利時(shí)刻！

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

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

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

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

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

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

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

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

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

例如，現(xiàn)在已知「Asterix 定律」并不蘊(yùn)含「Oberlix 定律」，但所有反例必然是無限的。奇怪的是，已知的構(gòu)造與集合論中著名的強(qiáng)迫技術(shù)有某種相似之處，因?yàn)樗麄儾粩嗟貙ⅰ竿ㄓ谩乖靥砑拥剑ú糠郑﹎agma 中， 以強(qiáng)迫存在具有某些特定屬性的反例，盡管這里的構(gòu)造肯定比集合論的構(gòu)造簡單得多。

他們還從交換和非交換環(huán)中的「線性」magma 構(gòu)造中獲得了可觀的收益，比如與「合流」方程定律相關(guān)的自由 magma，以及更普遍的具有完整重寫系統(tǒng)的定律。因此，未解決的蘊(yùn)含數(shù)繼續(xù)穩(wěn)步減少，不過還沒有到宣布該項(xiàng)目勝利的時(shí)候。

雖然該項(xiàng)目仍在進(jìn)行中，但陶哲軒對迄今為止取得的進(jìn)展感到非常滿意，而且對該項(xiàng)目的許多希望已經(jīng)實(shí)現(xiàn)。

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

他們?nèi)栽谔岢鲈S多非正式的數(shù)學(xué)論證，但它們往往在 Lean 中被迅速形式化，此時(shí)關(guān)于正確性的爭議就會消失，從而專注如何最好地部署各種經(jīng)過驗(yàn)證的技術(shù)來解決剩下的問題。

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

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

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