（視覺中國/圖）
随着GPT熱潮的不斷發展，包括ChatGPT在内的大型語言模型（Large Language Model；LLM）開始逐漸進入各種原來被認為是人類智力活動專屬的領域當中。例如，菲爾茲獎得主、華裔數學家陶哲軒就在一篇部落格中宣稱，他已經開始使用GPT-4來協助自己的工作。而2023年7月27日釋出在預印本網站（arXiv）上的一篇由加州理工、英偉達、MIT等機構的學者共同撰寫的論文聲稱，他們建構了一個基于開源LLM的定理證明器。似乎一夜之間，AI就攻陷了數學，這個人類智慧最純粹的領域之一。
實際上，追本溯源起來，數學家尋找自動化證明的過程，已經有一百多年的曆史了。甚至計算機的誕生與發展，也與這一探尋過程有着密不可分的關系。
數學基礎與哥德爾不完備定理
在1900年4月27日英國皇家學會的一次演講上，實體學家開爾文男爵發表了著名的實體學“兩朵烏雲”的演講。後來的事情大家都知道了，兩朵烏雲掀起了狂風暴雨，從中誕生了二十世紀現代實體學的兩大支柱——相對論和量子力學。
就在開爾文男爵發表演講的同一年，數學家大衛·希爾伯特在巴黎舉行的第二屆國際數學家大會上，作了題為《數學問題》的演講，提出了二十三道他認為最重要的數學問題。這些問題随後被稱作“希爾伯特問題”或者“希爾伯特的23個問題”。針對這些問題的研究，在很大程度上促進了二十世紀數學的發展。
在希爾伯特提出的這23個問題當中，就有諸如“連續統假設”“算術公理之相容性”“公理化實體”這樣涉及數學以及科學基礎的問題。這些問題的提出，來源于希爾伯特的雄心壯志：他希望能夠建立起一套統一的數學公理化體系。不止于此，在公理化體系之上，他還有一個更加宏大的設想，那就是所謂的“希爾伯特形式主義綱領”。
按照希爾伯特的設想，他想要建立的形式化的數學公理體系應該滿足三個條件。即：完備性：可以發現所有數學真命題；自洽性：數學内部不存在沖突；可決定性：能夠判斷每一個數學命題的真僞。
作為數學家的希爾伯特，他所關心的是“數學大廈”本身如何建造。至于這座大廈的地基建在哪裡，在希爾伯特看來是一件無需考慮的事情。但是，就是這件“無需考慮”的事情，卻出現了意想不到的問題。
1901年，年僅29歲的英國哲學家羅素發現了著名的羅素悖論。這一悖論，最簡單的表述形式就是所謂的“理發師悖論”。即：小城裡的理發師放出豪言：他要為城裡人刮胡子，而且一定隻要為城裡所有“不為自己刮胡子的人”刮胡子。那麼，理發師該為自己刮胡子嗎？
這一悖論說明了，當時作為“數學大廈”的基礎的樸素集合論，在邏輯上是不嚴謹的。這就是所謂的“第三次數學危機”。為此，數學家們最終将樸素集合論發展成了公理化集合論。更為重要的是，數學家們認識到，不僅數學本身需要公理化，數學基礎更需要公理化。
為此，羅素和他在劍橋大學三一學院時的老師、著名哲學家懷特海德，花費了十年時間，完成了三卷本的巨著《數學原理》。
羅素的做法，屬于對數學基礎進行探究的另外一個學派：“邏輯主義”。這部三卷本的《數學原理》，正是邏輯主義發展的高峰。在《數學原理》中， 數學大廈的一部分被從邏輯出發直接構築了出來。
這一宏大的目标的代價之一就是推理的極度曲折和冗長。比方說，“1”這個最簡單的數字在《數學原理》中直到第363頁才被定義；1+1=2這個最簡單的國小算術題直到第379頁才有結果。
《數學原理》滿滿兩大箱的手稿，被羅素用馬車運到了劍橋大學出版社。而出版社對這部巨著的利潤估計為：出版這部書會讓出版社虧損600英鎊。1910年的600英鎊，約等于現在的60萬元人民币。幸好，劍橋大學出版社并不是純粹的盈利性出版社，他們願意為這部學術著作承擔300英鎊的虧損。剩下的300英鎊中，英國皇家學會資助了200英鎊。最後這100英鎊隻得由羅素和懷特海德個人承擔。
但是，就在《數學原理》出版之後不久的1931年，年僅25歲的數學家哥德爾證明并發表了兩條日後被稱作“哥德爾不完備定理”的數學定理。這兩條定理表明，包含算術公理的數學體系是不完備的，同時也是不自洽的。
就像開爾文男爵口中的“兩朵烏雲”徹底改變了實體學大廈的形态一樣。哥德爾不完備定理也宣告了，希爾伯特和羅素所希望建立的數學大廈是永遠不可能竣工的。
前AI時代的機器證明
雖然希爾伯特和羅素的宏偉計劃被哥德爾證明是無法實作的。但是他們的工作，對于數學和計算機的發展，卻起到了難以估量的作用。
一方面，這些工作，使得現代數學有了一個相對堅實的基礎。另外一方面，這些工作中對公理化和形式化數學的探究，也徹底改變了自古以來數學家們描述數學的語言和研究數學的方式。這一變化最顯著的例子就是，現在幾乎所有的數學專著，都會選擇幾乎一模一樣的開篇方式。即在開頭部分，用集合論之類的語言，給出書中讨論的數學對象的嚴格定義。
而對希爾伯特公理化三條準則的研究，也催生出現代計算機的理論基礎。
哥德爾不完備定理宣告了希爾伯特公理體系中的完備性和自洽性是不成立的。而在同一時期，對于希爾伯特公理體系可決定性的研究也在進行。就在哥德爾發表不完備定理幾年後，波蘭裔數學家阿爾弗雷德·塔斯基和英國數學家阿蘭·圖靈各自獨立地證明了，希爾伯特公理體系中的可決定性，也是不成立的。
在證明的過程中，圖靈提出了“圖靈機”的概念。這一概念，就是現代計算機的理論模型。從本質上講，包括算盤、機械計算機、電子計算機在内的所有計算“機”，都可以看做是一種具體的圖靈機。另外，圖靈還證明了，希爾伯特公理體系中的可決定性，和圖靈機的停機問題是等價的。
圖靈的這些研究，成為日後計算機發展的理論基礎。因為在人工智能領域開創性的奠基作用，圖靈被稱為“人工智能之父”。
二戰之後，随着第一代真空管計算機在美國的發展，數學家們也開始嘗試在真正的“機器”上去實作那些已有的形式化的數學結論。為了做到這一點，首先需要創造出“機器”能夠“聽懂”，而且能夠用來進行邏輯推理的語言。這時，希爾伯特和羅素所使用的那一套形式化的邏輯符号，也就成為之後發展出的“機器”所使用的各種“數學語言”的基礎。
這一時期的主要結果，都是在普林斯頓高等研究院重達2.3噸的真空管計算機“JOHNNIAC”上完成的。1954年，馬丁·戴維斯開始嘗試為JOHNNIAC編寫包含自然數和加法的算法程式。他所取得的最大成果就是，讓JOHNNIAC證明了“兩個偶數的和還是偶數”。
在1956年，同樣是在JOHNNIAC上，艾倫·紐維爾、赫伯特·西蒙和J·C·肖，用他們開發的程式“邏輯證明機”，證明了羅素的《數學基礎》中前52條定理中的38條。對于某些定理，“邏輯證明機”甚至找到了新的、更優雅的證明。
自此，自動化證明（Automated Theorem Proving，ATP）開始逐漸成為一個正式的研究方向。而“邏輯證明機”也被很多人認為是“第一個人工智能程式”。盡管在當時，人工智能這一研究領域還不存在。
在随後的幾十年間，自動化證明有了長足的發展。但是，想要真正地讓自動化證明産出數學上有價值的結果，還是一件遙遙無期的事情。因為自動化證明，面臨一個魚和熊掌不可兼得的兩難局面。能夠用來生成有價值的數學結論的證明器通常基于比較強的邏輯系統，而在這類邏輯系統上實作全自動推理還是相當困難的。與之相對的，能夠實作強自動化的邏輯系統，如一階邏輯甚至布爾邏輯，卻無法産出真正有價值的數學結論。
面對這一局面，有人工引導的、強邏輯系統下的證明機器成為了發展的主流方向。這也就是所謂的互動式證明（Interactive Theorem Proving，ITP）。
利用互動式證明得出的最早也是最為知名的結果，就是四色定理的證明。
所謂四色定理，用通俗的話來說就是：“每個無外飛地的地圖都可以用不多于四種顔色來染色，而且不會有兩個鄰接的區域顔色相同。”這一問題最早是由南非數學家法蘭西斯·古德裡在1852年提出的，被稱為“四色問題”或“四色猜想”。在此後的一百多年時間裡，包括闵可夫斯基在内的知名大數學家都研究過這個問題，但是一直沒有得到完整的證明。
關于四色定理的證明思路，其實很早就已經明确了。這是因為，地圖上相鄰國家的接壤方式，可以分為有限多種情況。這些互不相同的情況，被稱為構型。是以，隻需要逐一驗證所有的構型都符合四色定理的情況，就證明了四色定理。但是這一目标的工作量，遠遠超過了人類能夠完成的極限。直到1976年，數學家凱尼斯·阿佩爾和沃夫岡·哈肯，在美國伊利諾伊大學的IBM 360電腦上，花費了1200小時的時間，驗證了所有的1936種構型，進而證明了四色定理。
自那之後，包括雙泡猜想、羅賓斯猜想在内的數十個數學問題，以與四色定理類似的方式得到了解決或者取得了重要的進展。
數學家們想要什麼？
雖然取得了這些成果，但是互動式的機器證明仍然沒有被數學界廣泛采用。甚至時至今日，還有數學家在嘗試不使用計算機，純靠人力去證明包括四色定理在内的，這些已經通過機器證明得到解決的數學問題。
這一方面是因為，互動式證明能夠解決的問題是有局限性的。而且，互動式證明作為一門獨立的研究方向，是有着不低門檻的。它需要掌握相應的人機互動語言。另外，互動式證明主流使用的，以類型論為基礎的邏輯體系，也和數學家們習慣的，以集合論為基礎的數學體系并不相同。這就導緻了如果數學家們想要親自使用互動式證明，就先要花費不小的學習成本來學習。
更為重要的原因，則是因為數學這門學科本身的價值觀。
提起數學，我們的第一反應大機率會是“嚴格”。在數學裡，對就是對，錯就是錯。在自然數當中1+1永遠都隻會等于2。數學考試的時候，哪怕最後結果算對了，隻要中間步驟有錯，也會被老師毫不留情地扣分。
不可否認的是，嚴格性的确是數學，特别是數學證明中極為重要的價值。但是，隻要稍微了解一點兒數學史，以及數學家們的具體工作，我們就難免會産生這樣的疑問：嚴格性是不是數學最重要的價值？
微積分的嚴格化是由魏爾斯特拉斯完成的。那時距離牛頓和萊布尼茨提出微積分已經過去了快200年。但是這并不影響牛頓和萊布尼茲作為微積分的提出者，被認為是曆史上最偉大的數學家之一。也不影響這200年間，數學家們用着不嚴格的微積分工具，發展出了極為精彩的數學理論和定理。
歐拉的很多極為精彩的工作，以現在的标準來看都是完全不嚴格的。時至今日，歐拉得出的那個全體自然數的和等于-1/12的結論，還在被各種營銷号拿來傳播。但是這也絲毫不影響歐拉在數學上的貢獻。
黎曼的很多工作是用到的數學理論，例如黎曼映照定理的證明中用到的，橢圓方程的正則性，直到20世紀很晚的時候才逐漸建立起來。
直到現在，數學中仍然有很多這樣的例子。
對現代幾何學的多個領域做出了革命性貢獻的俄裔法國數學家格羅莫夫，他的很多論文，按照一般數學工作者的标準來看，已經遠遠超出了“不嚴格”的程度。為了了解格羅莫夫的一篇短短十數頁的文章中的内容，往往就需要很多數學家去寫一系列的文章。
類似的情況還有實體學家出身，卻拿下來數學界最高獎菲爾茲獎的愛德華·威騰。他的很多工作，都來自于實體學的直覺，而不是數學的嚴格。
一個數學結果無法被嚴格寫下來，原因可能是多種多樣的。一個是數學還沒發展到可以用精煉的語言寫下嚴格的論斷的時候。牛頓和萊布尼茨、歐拉都是這種情況。在他們的時代，“無窮”還是一個相當模糊的概念，無論是數學上還是哲學上都沒有辦法準确描述什麼是“無窮”。在十九世紀後期這個問題開始被解決之後，人們就能很好地嚴格化他們的論述。
另一個原因則是出于效率的考慮。即使不談這些大數學家，作為普通的數學工作者，以及數學專業的學生，在寫論文的時候，也不會事無巨細地像機器證明那樣寫出所有的細節。很多繁瑣的内容，都被簡簡單單的“顯然”兩個字概括了。
更為主要的原因，則是對于數學了解的考慮。很多數學上的想法，未必是嚴格的，但很可能是很精彩的。無論是黎曼還是格羅莫夫和威騰，他們寫下的“證明”都是充滿内涵和啟發性的。相較于一個嚴格的、沒有錯誤的證明，這些“不嚴格”工作能夠讓我們對數學的了解更加深入，進而發現更多未知的數學。就像陳省身所說的：“有數學經驗和遠見的人，能在大海航行下，達到重要的新的領域。”
是以，雖然所有的數學結果，在最後都必須要徹底地嚴格化。但是在具體的過程中，嚴格性很多時候其實并不是處在最重要的位置上的。比起一萬個嚴格寫下來的形式化的證明，現在數學界主流還是更欣賞一個不嚴格的但是有深刻内涵的“證明”。
AI是解決之道嗎？
那麼，現在風頭正勁的，以GPT為代表的大型語言模型，能否改變這種局面，讓機器證明能夠滿足數學家們的需求，進而真的變得可用起來呢？
首先，要做到這一點，直接使用諸如GPT這樣的通用型的大型語言模型是不行的。
實際上，根據微軟研究院對GPT-4的測試報告，數學能力，在GPT-4的各項能力當中，本身就是一個相對的弱項。這很大程度上是因為，GPT的訓練和養成，主要是靠網際網路上的資訊。想要通過這樣的方式，獲得相當程度的專業數學能力，本身就是不現實的。而且，專業數學能力的培養，本身也不是GPT所要實作的目标。
那麼，如果我們換一個思路，将大型語言模型，與已有的互動式證明程式相結合，能不能制造出能夠滿足數學家們的需求的定理證明機呢？
這種想法是有着很強的合理性的。首先，大型語言模型這一工具，可以讓數學家們免去學習使用互動式證明的過程。他們隻需要用自己熟悉的語言将問題“告訴”給大型語言模型，然後讓模型将其“翻譯”給互動式證明程式，完成之後，再将程式給出的形式化的符号結果“翻譯”成數學家們習慣的數學語言。
另外，更為重要的是，現在的大型語言模型，已經展現出了一定的邏輯推理能力。按照AI的學習成長速度，再繼續發展下去，将來很有可能會出現，能夠給出在數學上做出有深刻内涵的啟發性工作的人工智能。
本文開頭所提到的，由加州理工、英偉達、MIT等機構的學者共同撰寫的論文中的工作，就是朝着這個方向邁出的第一步。
他們以Lean，這個由微軟研究院的萊昂納多·德·莫拉最初于2013年釋出的開源互動式證明機為基礎，推出了首個基于大型語言模型的開源定理證明機：LeanDojo。
不同于GPT這樣“大”型語言模型，LeanDojo要小很多。它的核心資料集，隻有96962個定理和證明過程。而且，不同于GPT需要在海量的硬體上進行長時間的訓練，LeanDojo的訓練過程，隻需要單張顯示卡一周的時間，就可以訓練完成。而根據論文中的說法，LeanDojo的數學能力，相較于GPT-4有着顯著的提升。
這是因為，相較于泛用型的GPT，專注于數學的LeanDojo，所需要處理的問題要單一得多。而且，形式化數學和機器證明幾十年的發展積累，也為LeanDojo的訓練提供了一個堅實的基礎。
盡管LeanDojo的表現看上去足夠讓人印象深刻，但是這篇論文的作者們卻十分地清醒。他們在論文中寫道：這項工作，旨在降低這一領域的進入門檻，并且為今後的工作提供一個可以繼續前進的起點。
雖然在現在這個時刻，想要讓AI做出數學家級别的工作還遠遠不可能。但是，大型語言模型和機器證明的結合，至少代表着一種可能性。就像一個小孩在紙上歪歪扭扭地寫出了“1+1=2”，所有人的反應，都是會微笑着期待這個小孩将來長大之後會做出什麼。
左力