陶哲軒用AI證明方程理論，19天進(jìn)度99.99%！

作者：新智元 2024-10-14 14:31:36

AI已完全融入數(shù)學(xué)家的工作流中。陶哲軒剛剛宣布，最新方程理論項(xiàng)目已完成99.9963%，眾包之力外加AI輔助取得了重大成績(jī)。他認(rèn)為，剩余大約700個(gè)讓人類頭疼的難題，AI或許更有潛力。

AI，已成為菲爾茲獎(jiǎng)得主最得心應(yīng)手的工具。

大約三周前，陶哲軒提出了一個(gè)協(xié)作項(xiàng)目——

結(jié)合專業(yè)和業(yè)余數(shù)學(xué)家、自動(dòng)定理證明器、AI工具，以及證明輔助語(yǔ)言Lean，來(lái)描述與4694條幺半群（magmas）方程定理定理相關(guān)的蘊(yùn)含圖。

圖片

這些定理最多可以使用，四次幺半群運(yùn)算來(lái)表達(dá)。

也就是說(shuō)，需要確定4694條定理之間可能存在4694 * (4694 - 1) = 22028942蘊(yùn)含的關(guān)系真?zhèn)巍?/span>

圖片

地址：https://github.com/teorth/equational_theories/blob/main/data/equations.txt

這一項(xiàng)目在9月25日發(fā)布當(dāng)天便啟動(dòng)了，如今，已經(jīng)緊鑼密鼓進(jìn)行了19天。

圖片

剛剛，陶哲軒公布了項(xiàng)目的最新進(jìn)展：

從已解決原始蘊(yùn)含關(guān)系角度來(lái)看，截至目前，項(xiàng)目進(jìn)度已完成99.9963%。

在需要解決的22028942個(gè)蘊(yùn)含關(guān)系中，8178279個(gè)被證明為真，13854531個(gè)被證明為假，只有826個(gè)仍未解決。

圖片

而且，項(xiàng)目每一天的進(jìn)展，他都記錄到了個(gè)人日志中。

圖片

一起看看，陶哲軒如何通過(guò)「眾包方式」，探索數(shù)學(xué)新領(lǐng)域。

方程理論項(xiàng)目，進(jìn)度99.99%

在集合中，有249個(gè)蘊(yùn)含關(guān)系推測(cè)為假，并且很快就證明了是假的。

出于編譯效率的考量，他們并沒(méi)有在Lean中記錄每一個(gè)證明，只在其中證明了一個(gè)較小的592790個(gè)蘊(yùn)含關(guān)系集合，然后通過(guò)傳遞性推導(dǎo)出更廣泛的蘊(yùn)含關(guān)系集合。

圖片

例如，利用如果方程X蘊(yùn)含方程Y，方程Y蘊(yùn)含方程Z，那么方程X蘊(yùn)含方程Z的事實(shí)。

他們還很快利用蘊(yùn)含圖對(duì)偶對(duì)稱性，對(duì)其進(jìn)一步簡(jiǎn)化。

經(jīng)過(guò)項(xiàng)目志愿者的不懈努力，陶哲軒稱現(xiàn)在有了很多出色的可視化工具（尚未完成的），來(lái)檢查蘊(yùn)含圖的各個(gè)部分。

比如，如下這張圖描述了方程1491：x = (y ◇ x) ◇ (y ◇ (y ◇ x ))的所有結(jié)果。

圖片

陶哲軒將其稱之為「Obelix law」。它還有一個(gè)伙伴Asterix law，即方程65：x = y ◇ (x ◇ (y ◇ x ))。

如下是，他們正在研究的所有方程定理的表格，以及它們蘊(yùn)含/被蘊(yùn)含定理數(shù)量。

圖片

地址：https://teorth.github.io/equational_theories/implications/

這些界面也在某種程度上與Lean集成。

比如，我們可以點(diǎn)擊查看Obelix law蘊(yùn)含方程359，陶哲軒將其作為題目，讓大家進(jìn)行挑戰(zhàn)。他暗示，在Lean中僅用4行就可以完成證明。

圖片

在過(guò)去的幾周里，他還了解到這些定理中，有許多之前已經(jīng)出現(xiàn)在文獻(xiàn)中。

由此，這里編制了這些方程的「導(dǎo)覽」。

圖片

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

例如，除了眾所周知的交換律（方程43）、結(jié)合律（方程4512）之外，一些方程（方程14、方程29、方程381、方程3722、方程3744）曾出現(xiàn)在一些Putnam數(shù)學(xué)競(jìng)賽中；

方程168定義了一個(gè)引人入勝的結(jié)構(gòu)，被稱為「中心幺半群」（central groupoid）。特別是，由Evans和Knuth研究過(guò)，并且是Knuth-Bendix完成算法的關(guān)鍵靈感來(lái)源；

圖片

而方程1571則對(duì)指數(shù)為二的阿貝爾群（abelian groups）進(jìn)行了分類。

圖片

根據(jù)Birkhoff完備性定理，如果一個(gè)方程定理蘊(yùn)含另一個(gè)，那么它可以通過(guò)有限次重寫操作來(lái)證明。

不過(guò)，所需的重寫次數(shù)可能相當(dāng)長(zhǎng)。

上面提到的1491蘊(yùn)含359的證明已經(jīng)相當(dāng)具有挑戰(zhàn)性，需要四到五次重寫。

另外，方程1689蘊(yùn)含方程2的證明，更是極其冗長(zhǎng)。盡管如此，標(biāo)準(zhǔn)的自動(dòng)定理證明器，如Vampire，完全有能力證明絕大多數(shù)這些蘊(yùn)含關(guān)系。

圖片

更微妙的是反蘊(yùn)含關(guān)系，在這種情況下必須證明定理X不蘊(yùn)含定理Y。原則上，只需要展示一個(gè)遵循X但不遵循Y的幺半群即可。

在很大一部分情況下，他們可以簡(jiǎn)單地搜索小型有限幺半群——比如兩個(gè)、三個(gè)或四個(gè)元素的幺半群——來(lái)獲得這種反蘊(yùn)含關(guān)系。

但這些并不足夠，事實(shí)上，他們只知道有些反蘊(yùn)含關(guān)系，只能通過(guò)構(gòu)造無(wú)限幺半群來(lái)證明。

比如，現(xiàn)在已知的Asterix law不蘊(yùn)含Obelix law，但所有反例必然是無(wú)限的。

有趣的是，已知的構(gòu)造方法與集合論中著名的forcing技術(shù)有一些相似之處，即不斷向（部分）幺半群添加「通用」元素，以forcing存在具有某些特定屬性的反例。

不過(guò)，這里的構(gòu)造肯定比集合論構(gòu)造簡(jiǎn)單得多。

他們還從「線性」幺半群x ◇ y = ax + by構(gòu)造中取得了有益的進(jìn)展。這些構(gòu)造存在于交換環(huán)和非交換環(huán)中。

與「匯聚」（confluent）方程定理相關(guān)的自由幺半群，以及更普遍的具有完整重寫系統(tǒng)的定理。

因此，未解決的蘊(yùn)含關(guān)系數(shù)量繼續(xù)穩(wěn)步減少。

遵循標(biāo)準(zhǔn)GitHub實(shí)踐，論文很快上線

經(jīng)過(guò)相當(dāng)繁忙的后端設(shè)置和「滅火」（putting out fires）工作后，項(xiàng)目現(xiàn)在運(yùn)行得相當(dāng)順利。

項(xiàng)目在Lean Zulip頻道上協(xié)調(diào)，所有貢獻(xiàn)都通過(guò)GitHub上的拉取請(qǐng)求（pull request）過(guò)程進(jìn)行，并通過(guò)基于問(wèn)題的GitHub項(xiàng)目進(jìn)行跟蹤。

另外兩位維護(hù)者Pietro Monticone、Shreyas Srinivas為其提供了寶貴的監(jiān)督。

與之前的PFR形式化項(xiàng)目相比，這次項(xiàng)目的工作流程遵循了標(biāo)準(zhǔn)的GitHub實(shí)踐，大致如下：

圖片

如果在Zulip討論過(guò)程中，明確需要完成某些特定任務(wù)以推進(jìn)項(xiàng)目（比如，在Lean中形式化討論線程中已經(jīng)推導(dǎo)出的蘊(yùn)含關(guān)系證明），就會(huì)創(chuàng)建一個(gè)「問(wèn)題」（通常由陶哲軒自己或其他維護(hù)者創(chuàng)建），其他貢獻(xiàn)者可以「認(rèn)領(lǐng)」這個(gè)問(wèn)題，單獨(dú)工作（使用主GitHub倉(cāng)庫(kù)的本地副本）。

然后提交「拉取請(qǐng)求」將他們的貢獻(xiàn)合并回主倉(cāng)庫(kù)。這個(gè)請(qǐng)求隨后可以由維護(hù)者和其他貢獻(xiàn)者審查，如果獲得批準(zhǔn)，就會(huì)關(guān)閉相關(guān)問(wèn)題。

更廣泛地說(shuō)，他們正努力記錄這個(gè)設(shè)置中的所有過(guò)程和經(jīng)驗(yàn)教訓(xùn)。

這將成為即將發(fā)表的關(guān)于這個(gè)項(xiàng)目的論文的一部分，現(xiàn)正處于初步規(guī)劃階段，可能會(huì)包括數(shù)十位作者。

陶哲軒表示，自己對(duì)項(xiàng)目取得的進(jìn)展非常滿意，而且許多最初的期望已經(jīng)實(shí)現(xiàn)。

在科學(xué)方面，他們發(fā)現(xiàn)了一些新的技術(shù)和構(gòu)造，用來(lái)證明一個(gè)給定的方程理論不蘊(yùn)含另一個(gè)；他們還發(fā)現(xiàn)了一些具有有趣特征的奇特代數(shù)結(jié)構(gòu)，如Asterix和Obelix對(duì)，是通過(guò)系統(tǒng)性搜索方式被發(fā)現(xiàn)的。

參與者方面，非常多樣化，從各個(gè)職業(yè)階段的數(shù)學(xué)家、計(jì)算機(jī)科學(xué)家，到感興趣的學(xué)生和業(yè)余愛(ài)好者。

此外，Lean平臺(tái)在整合人工生成和機(jī)器生成的貢獻(xiàn)方面表現(xiàn)良好。

機(jī)器生成在數(shù)量上是迄今為止最大的貢獻(xiàn)來(lái)源，但許多自動(dòng)生成往往是基于人類最初在特殊情況下發(fā)現(xiàn)的，然后由項(xiàng)目的不同成員進(jìn)行推廣和形式化。

在討論線程中，他們還進(jìn)行了許多非正式的數(shù)學(xué)論證，但這些論證往往會(huì)迅速在Lean中形式化，消除了關(guān)于正確性的爭(zhēng)議就。

進(jìn)而，研究人員可以轉(zhuǎn)而專注于如何最好地部署各種經(jīng)過(guò)驗(yàn)證的技術(shù)，來(lái)解決剩余的蘊(yùn)含關(guān)系。