想?yún)⒓犹照苘幇l(fā)起的「眾包」數(shù)學(xué)研究項(xiàng)目嗎？

機(jī)會(huì)來了！

AI輔助證明數(shù)學(xué)研究，越來越可行了

在傳統(tǒng)上，一個(gè)數(shù)學(xué)研究項(xiàng)目通常是由1到5名數(shù)學(xué)專家來完成的。

他們每個(gè)人都對(duì)項(xiàng)目的各方面都足夠熟悉，可以驗(yàn)證彼此的貢獻(xiàn)。

但如果要組織起更大規(guī)模的數(shù)學(xué)研究項(xiàng)目，特別是涉及公眾貢獻(xiàn)的項(xiàng)目，就麻煩多了。

原因在于，很難驗(yàn)證所有人的貢獻(xiàn)。

2023年底，陶哲軒宣布：將多項(xiàng)式Freiman-Ruzsa猜想的證明形式化的Lean4項(xiàng)目，在三周后取得了成功（圖為最新狀態(tài)）

要知道，在數(shù)學(xué)論證某個(gè)部分中的單個(gè)錯(cuò)誤，可能就會(huì)使整個(gè)項(xiàng)目失敗。

而且，以一個(gè)典型數(shù)學(xué)項(xiàng)目的復(fù)雜程度來說，期待具有本科數(shù)學(xué)教育水平的公眾做出有意義的貢獻(xiàn)，也是不現(xiàn)實(shí)的。

由此我們也可以知道，把AI工具納入到數(shù)學(xué)研究項(xiàng)目中，也是極有挑戰(zhàn)性的。

因?yàn)锳I會(huì)生成看似合理但實(shí)際上毫無意義的論證，因此需要額外驗(yàn)證，才能將AI生成的部分添加到項(xiàng)目中。

好在，證明輔助語言（比如Lean）提供了潛在的方法，能夠克服這些障礙，并且讓專業(yè)數(shù)學(xué)家、廣大公眾和AI工具的合作成為可能。

這種方法的前提是，項(xiàng)目可以以模塊化的方式分解成更小的部分，這些部分可以在不必理解整個(gè)項(xiàng)目的情況下就能完成。

目前的例子主要有將現(xiàn)有數(shù)學(xué)結(jié)果形式化的項(xiàng)目（比如對(duì)Marton最近證明的PFR猜想的形式化）。

這些形式化工作，主要是通過眾包方式由人類貢獻(xiàn)者（包括專業(yè)數(shù)學(xué)家和感興趣的公眾）完成的。

同時(shí)，還有一些新興的嘗試，試圖引入更多的自動(dòng)化工具來完成，后者包括傳統(tǒng)的自動(dòng)定理證明器，以及更現(xiàn)代的基于AI的工具。

探索全新數(shù)學(xué)問題，成為可能

并且，陶哲軒還認(rèn)為，這種全新范式不僅可以用于形式化現(xiàn)有的數(shù)學(xué)，還可以用來探索全新的數(shù)學(xué)！

過去，他曾經(jīng)和繼任組織過一個(gè)在線協(xié)作「Polymath」的項(xiàng)目，就是一個(gè)很好的例子。

不過，這個(gè)項(xiàng)目沒有將證明輔助語言納入工作流，貢獻(xiàn)就必須由人類主持人管理和驗(yàn)證，這項(xiàng)工作非常耗時(shí)，也限制了將這些項(xiàng)目進(jìn)一步擴(kuò)大。

現(xiàn)在，陶哲軒希望，添加證明輔助語言能突破這個(gè)瓶頸。

而他尤其感興趣的，就是是否可能使用這些現(xiàn)代工具同時(shí)探索一類數(shù)學(xué)問題，而不是一次只關(guān)注一兩個(gè)問題。

本質(zhì)上，這種方法是可模塊化的重復(fù)任務(wù)，如果有適當(dāng)?shù)钠脚_(tái)來嚴(yán)格協(xié)調(diào)所有貢獻(xiàn)，眾包和自動(dòng)化工具可能會(huì)尤其有用。

如果用以前的方法，這種數(shù)學(xué)問題類型是無法擴(kuò)大規(guī)模的。除非在多年時(shí)間里，隨著個(gè)別論文慢慢地一次探索一個(gè)數(shù)據(jù)點(diǎn)，直到對(duì)這類問題獲得合理的直覺。

此外，如果有一個(gè)大型問題數(shù)據(jù)集，可能有助于對(duì)各種自動(dòng)化工具進(jìn)行性能評(píng)估，并且比較不同工作流程的效率。

這類項(xiàng)目最近的一個(gè)例子，是「忙碌海貍挑戰(zhàn)」。

在今年7月，第五個(gè)忙碌海貍數(shù)被證實(shí)為是47,176,870。

一些更早的眾包計(jì)算項(xiàng)目，比如「互聯(lián)網(wǎng)梅森素?cái)?shù)大搜索」（Great Internet Mersenne Prime Search， GIMPS），在內(nèi)在精神上跟這些項(xiàng)目也有些類似，盡管它們使用的是更傳統(tǒng)的工作量證明機(jī)制，而不是證明輔助語言。

陶哲軒表示，很想知道是否還有其他現(xiàn)存的眾包項(xiàng)目探索數(shù)學(xué)空間的例子，以及是否有可用的經(jīng)驗(yàn)教訓(xùn)。

陶哲軒提出新項(xiàng)目

為此，陶哲軒自己也提出了一個(gè)項(xiàng)目，來進(jìn)一步測(cè)試這一范式。

這個(gè)項(xiàng)目受到去年MathOverflow問題的啟發(fā)。

不久后，陶哲軒在自己的Mathstodon上，對(duì)它進(jìn)行了進(jìn)一步討論。

這個(gè)問題屬于泛代數(shù)（universal algebra）領(lǐng)域，涉及對(duì)原群（magma）的簡(jiǎn)單等式理論的中等規(guī)模探索。

原群是一個(gè)配備了二元運(yùn)算的集合G。

最初，這個(gè)運(yùn)算o沒有附加任何額外的公理，因此原群本身是較為簡(jiǎn)單的結(jié)構(gòu)。

當(dāng)然，通過添加額外的公理，如恒等公理或結(jié)合律公理，我們可以得到更熟悉的數(shù)學(xué)對(duì)象，例如群、半群或幺半群。

在這里，我們感興趣的是（無常數(shù)的）等式公理。這些公理涉及由運(yùn)算o和G中的一個(gè)或多個(gè)未知變量構(gòu)建的表達(dá)式的相等性。

此類公理的兩個(gè)熟悉的例子，是交換律x o y = y o x和結(jié)合律(x o y) o z = x o (y o z)。

其中x，y，z是原群G中的未知變量。

另一方面，（左）恒等公理e o x = x在這里不被視為等式公理（equational axiom），因?yàn)樗婕耙粋€(gè)常數(shù)e ∈ G。這類涉及常數(shù)的公理在本研究中不予討論。

接下來，為了闡明自己發(fā)起的研究項(xiàng)目，陶哲軒介紹了十一個(gè)關(guān)于原群的等式公理例子。

這些等式公理是僅涉及原群運(yùn)算和未知變量的等式——

因此，舉例來說，等式7表示交換律公理，而等式10表示結(jié)合律公理。

常數(shù)公理等式1是最強(qiáng)的，因?yàn)樗拗屏嗽篏最多只能有一個(gè)元素；與之相反，自反公理等式11是最弱的，所有原群都滿足這一公理。

接下來，我們就可以探討這些公理之間的推導(dǎo)關(guān)系：哪些公理能推出哪些公理？

例如，等式1可以推導(dǎo)出這個(gè)列表中的所有其他公理，而這些公理又可以推導(dǎo)出等式11。

等式8作為特殊情況可以推導(dǎo)出等式9，而等式9又作為特殊情況可以推導(dǎo)出等式10。

這些公理之間完整的推導(dǎo)關(guān)系可以用以下哈斯圖（Hasse diagram）來描述：

這一結(jié)果特別回答了數(shù)學(xué)問答網(wǎng)站MathOverflow上的一個(gè)問題：是否存在介于常數(shù)公理（等式1）和結(jié)合律公理（等式10）之間的等式公理（equational axioms）。

值得注意的是，這里大多數(shù)的蘊(yùn)含關(guān)系都很容易證明。然而，其中存在一個(gè)非平凡的蘊(yùn)含關(guān)系。

這個(gè)關(guān)系是在一個(gè)與前述問題密切相關(guān)的MathOverflow帖子回答中得到的：

命題1：等式4蘊(yùn)含等式7

證明：假設(shè)G滿足等式4，因此

對(duì)所有x,y ∈ G成立。

特別是，當(dāng)y = x o x時(shí)，可以得出(x o x) o (x o x) = (x o x) o x。

再次應(yīng)用（1），可以得出x o x是冪等的：

現(xiàn)在，在（1）中將x替換為x o x，然后使用（2），可以得出(x o x) o y = y o (x o x)。

尤其，x o x與y o y是可交換的：

此外，通過兩次應(yīng)用（1），可以得到(x o x) o (y o y) = (y o y) o x = x o y。

因此，（3）就可以簡(jiǎn)化為x o y = y o x，這就是等式7。

上述論證過程的形式化，可以在Lean中找到。

然而值得注意的是，確定一組等式公理是否決定另一組等式公理的一般問題，是不可判定的。

因此，這里的情況有點(diǎn)類似于「忙碌海貍」挑戰(zhàn)，即在某個(gè)復(fù)雜點(diǎn)之后，我們必然會(huì)遇到不可判定的問題；但在達(dá)到這個(gè)閾值之前，我們?nèi)杂邢Ｍl(fā)現(xiàn)有趣的問題和現(xiàn)象。

上面的哈斯圖不僅斷言了列出的等式公理之間的蘊(yùn)含關(guān)系，還斷言了公理之間的非蘊(yùn)含關(guān)系。

例如，如圖所示，交換公理等式7并不蘊(yùn)含等式4公理(x + x) + y = y + x。

要證明這一點(diǎn)，只需找出一個(gè)滿足交換公理等式7但不滿足等式4公理的原群的例子。

比如，在這種情況下，我們可以選擇自然數(shù)集N，其運(yùn)算為x o y := x+y。

更一般地，該圖斷言以下非蘊(yùn)含關(guān)系，這些關(guān)系（連同已指出的蘊(yùn)含關(guān)系）完整描述了這十一個(gè)公理之間蘊(yùn)含關(guān)系的偏序集：

在此，陶哲軒邀請(qǐng)讀者提出反例，來完成其中的部分證明。

最難找到的反例，就是等式9無法推出等式8了。

用Lean可以給出解決方案。

另外，陶哲軒還提供了一個(gè)GitHub存儲(chǔ)庫(kù)，包含了所有上述包含和反包含關(guān)系的Lean證明。

可以看出，僅僅計(jì)算11個(gè)等式的哈斯圖就已經(jīng)有些繁瑣了。

而陶哲軒提出的項(xiàng)目，是嘗試將這個(gè)哈斯圖擴(kuò)展幾個(gè)數(shù)量級(jí)，覆蓋更大范圍的等式集。

他提議的集合是ε，即最多使用原群運(yùn)算o四次的等式集，直到重新標(biāo)記和等式的自反性和對(duì)稱性公理。

這包括了上述十一個(gè)等式，但還有更多。

還有多少呢？

回想一下，卡特蘭數(shù)C_n是用二元運(yùn)算o（應(yīng)用于n+1個(gè)占位符變量）形成表達(dá)式的方法數(shù)；而給定m個(gè)占位符變量的字符串，貝爾數(shù)B_m是為這些變量分配名稱的方法數(shù)（可以重新標(biāo)記），其中允許某些占位符被分配相同的名稱。

因此，忽略對(duì)稱性，最多涉及四次運(yùn)算的等式數(shù)量是

左側(cè)和右側(cè)相同的等式數(shù)量是

這些都等同于自反公理（等式11）。

剩下的9118個(gè)等式由于等式的對(duì)稱性成對(duì)出現(xiàn)，所以ε的總大小是

陶哲軒表示，自己還沒有生成這樣恒等式的完整列表，但他猜想，使用Python就可以輕松完成。

使用AI工具，應(yīng)該能生成大部分所需的代碼。

他表示，自己完全不清楚ε的幾何結(jié)構(gòu)會(huì)是什么樣子。

大多數(shù)等式會(huì)彼此不可比較嗎？它會(huì)分為「強(qiáng)」公理和「弱」公理嗎？

現(xiàn)在，陶哲軒的留言區(qū)，已經(jīng)有了幾十條評(píng)論。

感興趣的讀者，陶哲軒也向你發(fā)出了邀請(qǐng)。