57天，人類和AI合作搞定了4694個(gè)等式之間22028942個(gè)蘊(yùn)含關(guān)系！

大神陶哲軒激動(dòng)宣布：等式理論計(jì)劃，成功。

“等式理論計(jì)劃”，由陶哲軒本人在2024年9月25日發(fā)起，目的是探索按蘊(yùn)含關(guān)系排序的原群（magma）等式理論空間。

特別的是，在這個(gè)項(xiàng)目里，陶哲軒不僅集合了人類數(shù)學(xué)家的力量，還把AI工具納入了合作者的范圍，包括ChatGPT、Claude和GitHub Copilot。

項(xiàng)目發(fā)起當(dāng)日就正式啟動(dòng)，僅僅9天，項(xiàng)目進(jìn)度就達(dá)到了99.866%。

而現(xiàn)在，在2200萬+個(gè)需要證明的蘊(yùn)含關(guān)系中，8178279個(gè)已被證實(shí)，13855193個(gè)已被證偽，僅有162個(gè)還懸而未決。

按陶哲軒的說法，就是離“宣布完全成功”基本只是“時(shí)間問題”：

因此，我們現(xiàn)在已經(jīng)開始著手撰寫論文了。

什么是“等式理論計(jì)劃”

還是先來扒一扒陶哲軒這回究竟是整了個(gè)什么樣的活兒。

簡單說，“等式理論計(jì)劃”是指：

采用”數(shù)學(xué)家+AI（包括自動(dòng)定理證明系統(tǒng)和大模型）+證明輔助語言Lean”這樣的協(xié)作方式，構(gòu)建一個(gè)展示4694個(gè)magma等式（最多四次使用magma操作）之間所有蘊(yùn)含關(guān)系的 “蘊(yùn)含圖”。

首先，這個(gè)計(jì)劃的最初靈感源于陶哲軒本人對(duì)“去中心化”研究方式的暢想。

傳統(tǒng)上，大部分?jǐn)?shù)學(xué)研究項(xiàng)目都由少數(shù)專業(yè)數(shù)學(xué)家（通常1~5名）進(jìn)行，每個(gè)人都對(duì)自己的部分更專業(yè)，且彼此可以相互驗(yàn)證。

不過也是因?yàn)榇嬖隍?yàn)證環(huán)節(jié)，組織更大規(guī)模的數(shù)學(xué)項(xiàng)目（尤其是需要涉及公眾貢獻(xiàn)），一直具有挑戰(zhàn)性。

而現(xiàn)在，通過AI工具以及Lean這樣的證明輔助語言，數(shù)學(xué)項(xiàng)目的大規(guī)模協(xié)作變得可能。

打前陣的就有開源社區(qū)尋找梅森素?cái)?shù)的成功嘗試，在這個(gè)代號(hào)GIMPS的志愿項(xiàng)目中，任何擁有強(qiáng)大PC或GPU的人都可以加入尋找梅森素?cái)?shù)。

雖然證明助手這樣的AI工具在這個(gè)項(xiàng)目里用得還不多，但表達(dá)的精神是類似的。

因此，在開展等式理論計(jì)劃之前，陶哲軒就打算搞一個(gè)實(shí)驗(yàn)：

在一個(gè)數(shù)學(xué)項(xiàng)目中，聚齊專業(yè)/業(yè)余數(shù)學(xué)家、AI工具、證明輔助語言Lean等，一同干大事！

受去年MathOverflow上一個(gè)等式問題的啟發(fā)，這一次，陶哲軒將目光瞄準(zhǔn)了代數(shù)領(lǐng)域中的magma。

當(dāng)時(shí)的問題是醬嬸兒的：

交換恒等式和常量恒等式之間是否存在等價(jià)關(guān)系？

拋開具體問題不談，這里主要想說明magma涉及等式之間的關(guān)系。

簡單來說，magma是一個(gè)代數(shù)結(jié)構(gòu)，它由一個(gè)集合和一個(gè)在該集合上定義的二元運(yùn)算組成，但不要求滿足任何額外的代數(shù)性質(zhì)，如結(jié)合律、交換律等。

我們常見的有關(guān)magma的等式包括：

而等式理論計(jì)劃，就是要找出magma中不同等式之間的等價(jià)、推出和非推出關(guān)系。

就拿上面這11個(gè)等式來看，最終的關(guān)系圖be like：

可以看出，常量公理等式（1）蘊(yùn)含了其他所有等式，即如果1成立，那么其他等式也自動(dòng)成立；而反身公理等式（11）由于最寬松（x=x），幾乎所有的magma都滿足這個(gè)公理。

回到計(jì)劃本身，陶哲軒等人在初始階段集中研究了那些只包含一個(gè)方程的magma定律，這些方程最多包含四個(gè)magma操作（即二元運(yùn)算）。

舉個(gè)例子，如果我們有一個(gè)magma（M，?），其中M是元素的集合，?是定義在M上的二元運(yùn)算。

則一個(gè)“最多四次使用magma操作”的表達(dá)式如下：

• a?b（一次操作）
• (?????)???(a?b)?c（兩次操作）
• ???(???(?????))a?(b?(c?d))（三次操作）
• ((?????)???)?(?????)((a?b)?c)?(d?e)（四次操作）

其中??,??,??,??,??都是集合M中的元素，每次?的使用都算作一次magma操作。

這樣的等式定律有4694個(gè)，由于每個(gè)定律都可能蘊(yùn)含其他4693個(gè)定律（一個(gè)定律不能蘊(yùn)含自身），因此總共有4694*(4694-1) = 22,028,942個(gè)可能的蘊(yùn)含關(guān)系需要被證明或反駁。

這里的蘊(yùn)含關(guān)系包括“蘊(yùn)含”和“反蘊(yùn)含”，其中“蘊(yùn)含”關(guān)系又涉及到兩種類型：

• 已證明的蘊(yùn)含：在Lean中已經(jīng)過驗(yàn)證
• 推測(cè)的蘊(yùn)含：尚未在Lean中驗(yàn)證，可能由人或計(jì)算機(jī)生成

更多項(xiàng)目細(xì)節(jié)，陶哲軒在項(xiàng)目日志中，留下了非常詳細(xì)的記錄——

9天進(jìn)度99.866%，大模型有用但“表現(xiàn)低于預(yù)期”

簡單總結(jié)“等式理論計(jì)劃”的進(jìn)度，就是一個(gè)字：快。

陶哲軒本人都說：

這個(gè)項(xiàng)目的進(jìn)度遠(yuǎn)超我的預(yù)期。

有多快？

僅僅48小時(shí)，很大一部分蘊(yùn)含關(guān)系就已“解決在望”。

項(xiàng)目啟動(dòng)第5天，項(xiàng)目參與者們已經(jīng)從最初的約2200萬條蘊(yùn)含關(guān)系中解決了大量簡單蘊(yùn)含，只剩下約300萬的數(shù)量尚待解決。

項(xiàng)目啟動(dòng)第9天，隨著首次重大重構(gòu)的完成——合作者們改進(jìn)了magma的運(yùn)算符號(hào)，以使Lean代碼的編譯速度顯著加快，以及一些研究問題的推進(jìn)，項(xiàng)目完成度一舉從87%躍升到了99.866%。

第19天，項(xiàng)目進(jìn)度來到99.9963%。陶哲軒在他的博客文章中提及，寫論文的事已經(jīng)提上日程，并且可能包含數(shù)十名作者。

GitHub顯示該項(xiàng)目有45位貢獻(xiàn)者：

到了11月21日，也就是項(xiàng)目第57天，隨著主項(xiàng)目最后一個(gè)未解決的蘊(yùn)含關(guān)系被搞定（待驗(yàn)證），“等式理論計(jì)劃”目標(biāo)已宣告達(dá)成。

論文可以正式開寫了。

陶哲軒透露，論文的框架早已擬好，但后續(xù)還需要大量工作來對(duì)其進(jìn)行更新，并轉(zhuǎn)換為可以提交的形式。

日志中也詳細(xì)談到了大模型工具發(fā)揮的作用。

在第一天，陶哲軒就對(duì)GitHub Copilot大加贊賞：

GitHub Copilot在處理日常任務(wù)時(shí)非常有用，比如輸入需要證明的新Lean定理，或者更新藍(lán)圖來整合最新的PR結(jié)果。

他具體舉了個(gè)例子：要將Lean轉(zhuǎn)換為LaTeX，把Lean代碼粘貼為注釋，開始敲LaTeX，GitHub Copilot就會(huì)自動(dòng)補(bǔ)全剩下的內(nèi)容。

不過，陶哲軒也坦率表示，大模型們?cè)陧?xiàng)目中的表現(xiàn)“低于預(yù)期”，更多的時(shí)候，數(shù)學(xué)家們用到的還是“經(jīng)典AI”，比如自動(dòng)定理證明器Vampire等。

他還提到：

項(xiàng)目的參與者非常多元化，包括處在職業(yè)生涯各個(gè)階段的數(shù)學(xué)家和計(jì)算機(jī)科學(xué)家，學(xué)生和業(yè)余愛好者。Lean在整合人類和機(jī)器生成的貢獻(xiàn)方面表現(xiàn)出色。機(jī)器生成的部分在數(shù)量上是貢獻(xiàn)的最主要來源，不過，許多自動(dòng)生成的結(jié)果最初是人類在特殊情況下得出的，之后被進(jìn)一步推廣和形式化。

具體到項(xiàng)目中，GitHub Copilot的主要作用還是加快代碼的編寫，而Claude則被用來幫忙創(chuàng)建可視化工具，比如這個(gè)“等式瀏覽器”：

ChatGPT則更多扮演激發(fā)數(shù)學(xué)家們靈感的小助手角色。

對(duì)陶哲軒來說，ChatGPT能幫他快速掌握通用代數(shù)的一些細(xì)節(jié)。

而lyphyser、Daniel Weber、Fan Zheng和Bhavik Mehta這幾位項(xiàng)目參與者，還通過跟ChatGPT的討論，證明1659這個(gè)等式可能具有非平凡的合流性。

主項(xiàng)目里程碑達(dá)成，不過“等式理論計(jì)劃”的其他衍生項(xiàng)目仍在進(jìn)行中，比如研究在有限原群限制下的類似蘊(yùn)含圖、對(duì)蘊(yùn)含圖進(jìn)行數(shù)據(jù)分析等等。

陶哲軒也再次強(qiáng)調(diào)了這一項(xiàng)目和AI的聯(lián)系：

希望項(xiàng)目中的蘊(yùn)含關(guān)系能夠作為未來AI數(shù)學(xué)工具的基準(zhǔn)測(cè)試。

除了陶哲軒之外，項(xiàng)目的主要維護(hù)人還有意大利數(shù)學(xué)家Pietro Monticone和Shreyas Srinivas。

兩位都是Lean重度愛好者。

△Shreyas Srinivas主頁

Pietro Monticone還和他特倫托大學(xué)的同事們一起搞過指數(shù)3的費(fèi)馬大定理的Lean版證明。

GitHub：https://github.com/teorth/equational_theories