數(shù)學(xué)證明建立在公理之上，追求絕對的邏輯嚴(yán)密。然而，哪怕是最偉大的數(shù)學(xué)家，耗費(fèi)數(shù)年所得的成果也可能因一個細(xì)微的疏漏而崩塌。面對人工校驗(yàn)困難，錯誤難以避免的現(xiàn)實(shí)，“證明助手”應(yīng)運(yùn)而生——以機(jī)器審視每一步推導(dǎo)，確保證明無懈可擊。而今，隨著 AI 的加入，形式化證明正邁向新的階段。也許，希爾伯特那場“讓數(shù)學(xué)徹底形式化”的夢，正悄然接近實(shí)現(xiàn)。

撰文 | Ben Watkins

翻譯 | LogicMoriaty

審校 | 7號機(jī)

人類數(shù)學(xué)家難免出錯。證明助手應(yīng)運(yùn)而生，助其查漏補(bǔ)缺，而在這個過程中，它們也將數(shù)學(xué)轉(zhuǎn)化成了一種高度合作的體驗(yàn)。
什么是證明？

數(shù)學(xué)只是一種依照特定簡單規(guī)則，在紙上操作無意義符號的游戲。

——大衛(wèi)·希爾伯特（David Hilbert）

這話聽起來有些悲觀。

數(shù)學(xué)不同于科學(xué)。盡管二者之間互動密切（有些人認(rèn)為數(shù)學(xué)是科學(xué)的語言），但它們是完全不同的兩種游戲?？茖W(xué)本質(zhì)上是一種基于觀察與經(jīng)驗(yàn)的游戲；在科學(xué)中，只有那些在我們觀察到的世界和宇宙中顯現(xiàn)出來的事物，才被視為真實(shí)。而數(shù)學(xué)則是一種基于公理的游戲。

公理可以看作是數(shù)學(xué)的規(guī)則。它們是無法從其他東西推導(dǎo)或證明出來的基礎(chǔ)，我們在此基礎(chǔ)上構(gòu)建起整個數(shù)學(xué)體系。皮亞諾公理（Peano axioms）便是公理集合的一個范例，它是自然數(shù)的公理體系。其中包括一些像“0是一個自然數(shù)”、“若 x=y，則 y=x”這樣的陳述。在某種意義上，它們是“顯而易見”的陳述，或是用希爾伯特的話來說，它們是“簡單的規(guī)則”。在數(shù)學(xué)中，斷言某個命題為真，例如“存在無窮多個素?cái)?shù)”，就意味著我們可以證明這個命題能夠歸結(jié)于這些公理。數(shù)學(xué)中所有的美妙之處，所有復(fù)雜精妙的結(jié)構(gòu)和簡潔強(qiáng)大的定理（或者說是某些人眼中的“紙上無意義的符號”），在某種意義上，都不過是從公理中幸運(yùn)衍生出的產(chǎn)物。

話雖如此，但這并不是做數(shù)學(xué)的真實(shí)體驗(yàn)。幾乎所有的純數(shù)學(xué)論文都不會提到公理。相反，在實(shí)際的研究體驗(yàn)中，更多是通過將待證明的定理歸結(jié)于先前已經(jīng)被證明的命題來完成證明。不妨在腦海中勾勒這樣一幅圖景：一棵枝繁葉茂的大樹，基礎(chǔ)定理如同主枝一樣從公理的樹干上生長出來，較小的枝條從主枝延伸而出，更細(xì)的嫩枝又從這些小枝上萌發(fā)。最終，每條嫩枝都能追溯回樹干，但是實(shí)際上，將其視作所屬枝條的延伸往往更為實(shí)用。（當(dāng)然，這個比喻的局限性也是顯而易見的。比如某些定理存在多種證明路徑，或者有些命題雖然成立卻暫無證明，此時這樣的比喻就顯得比較牽強(qiáng)。）

然而，至關(guān)重要的是，必須確保論文中的證明是正確和完整的。
一個例子：四色定理
四色定理（Four-colour theorem）說的是，任何有邊界的地圖（例如美國地圖）都只需使用四種顏色來著色，就能使得任何共享邊界的兩個區(qū)域顏色都不相同。

您可以給一百萬張地圖著色，來嘗試驗(yàn)證四色定理，但是這并不能算是一個證明。萬一存在您尚未發(fā)現(xiàn)的反例呢？在1879年，阿爾弗雷德·肯普（Alfred Kempe）似乎認(rèn)為他已經(jīng)證明了反例不存在，并發(fā)表了對該定理的“證明”。然而11年后，珀西·約翰·希伍德（Percy John Heawood）證明了這個“證明”實(shí)際上是錯誤的——肯普的證明中使用了一個錯誤的假設(shè)。
這便引出了一個很自然的問題：當(dāng)一個證明發(fā)表時，我們應(yīng)該如何確定它是正確的？如何確保它是數(shù)學(xué)之樹上的一條新枝，而非一條注定孤獨(dú)墜地的枯枝？肯定存在某種方法可以檢查這些證明是否正確的，對吧？

同行評審?fù)ǔ＞褪墙鉀Q這個問題的方法。也就是說，當(dāng)一篇論文發(fā)表時，一小群其他的數(shù)學(xué)家會檢查你的工作。然而，假如這些同行也沒發(fā)現(xiàn)你的錯誤怎么辦？更何況，如今動輒數(shù)百頁的長篇論文屢見不鮮。所以實(shí)際上，單憑人力根本無力全面檢查。

這便催生了對于“證明助手”（proof assistants）的需求。 證明助手是由計(jì)算機(jī)科學(xué)家開發(fā)的軟件工具，通過要求每一步推導(dǎo)都以形式化語言表述，來驗(yàn)證一個證明是否正確。如若未能滿足要求，程序便會判定該證明不完整。

凱文·巴扎德（Kevin Buzzard）是倫敦帝國理工學(xué)院的純數(shù)學(xué)教授。在巴扎德參加艾薩克·牛頓研究所的“大證明計(jì)劃”（Big Proof programme）完后，筆者曾與他見面（文章稍后會詳細(xì)介紹?。?。他解釋道：“嗯，事情是這樣的，如果你在和一個象棋計(jì)算機(jī)對弈，那你根本無法走出違反游戲規(guī)則的一步，對吧？在象棋中，很容易識別對方是否走了違規(guī)的棋步，但是在數(shù)學(xué)中卻不是這樣，數(shù)學(xué)比象棋要復(fù)雜得多。我們會看到一些發(fā)表的論文有錯誤，雖然很少見，且錯誤往往無關(guān)緊要，但有時候會出現(xiàn)非常大的錯誤。而使用證明助手做數(shù)學(xué)研究，一定程度上消除了出錯的可能性……整個數(shù)學(xué)體系在沒有它們的情況下當(dāng)然也能照常工作，但現(xiàn)在已經(jīng)是2025年了，我們完全可以擁有這點(diǎn)額外的保障。只要我們想要，我們就可以獲得這個額外的優(yōu)勢。”

例如，四色定理的第一個正確證明是由肯尼斯·阿佩爾（Kenneth Appel）和沃爾夫?qū)す希╓olfgang Haken）于1976年給出的。他們通過將需要驗(yàn)證的可能反例的數(shù)量從無窮多（相當(dāng)龐大的一個數(shù)量）減少到1,834個（依然很多，但是已大幅減少）來完成這一證明。隨后，他們借助計(jì)算機(jī)驗(yàn)證了這些情形均不構(gòu)成反例。完整的證明發(fā)表，并附有超過400頁的微縮膠片補(bǔ)充材料。其篇幅之長，對于任何（心智正常的）人來說，根本不可能逐一檢查。

然而到了2005年，本杰明·維爾納（Benjamin Werner）和喬治斯·岡蒂爾（Georges Gonthier）在證明助手 Rocq（前身為 Coq）中給出了一個完全形式化的證明。
證明助手究竟是什么？

凱文·巴扎德將證明助手形容為一個特別學(xué)究式（過分嚴(yán)謹(jǐn)）的學(xué)生。想象一下，你正在講臺上講課，嘗試證明某個結(jié)果。每當(dāng)你在證明中做出任何一步，哪怕是像在方程兩邊加1這樣顯而易見的步驟，坐在教室前排的一個特別讓人惱火的本科生總會舉手發(fā)問：“這個為什么成立？”

當(dāng)你使用證明助手時，你將需要編寫一些代碼，而代碼只有在所有細(xì)節(jié)都得到明確闡明的前提下才能運(yùn)行。假設(shè)你在進(jìn)行某個證明的時候，需要使用某個定理，而這個定理有三個前提條件。也就是說，這個定理表示，如果你已知關(guān)于某個特定對象的三個屬性（例如，它是一個自然數(shù)，它大于3，它是一個質(zhì)數(shù)），然后你就會知道一些關(guān)于它的結(jié)論（例如，它的平方比24的倍數(shù)大1）。那么，當(dāng)你使用這個定理時（例如，對像43這樣的數(shù)字），除非你證明它滿足所有前提條件（即，它是自然數(shù)，它大于3，并且它是質(zhì)數(shù)），否則代碼無法運(yùn)行。

這種如同“杠精”一樣的過分嚴(yán)謹(jǐn)在做數(shù)學(xué)時并不常見，但它卻可以使我們放心，當(dāng)代碼能夠運(yùn)行時，證明肯定是正確的。下面的部分將進(jìn)一步介紹如何使用證明助手證明其他的復(fù)雜定理，以及它們?nèi)绾胃淖內(nèi)藗冄芯繑?shù)學(xué)的方式。
證明助手：創(chuàng)作社群

在本文前面的部分中，我們探討了什么是證明助手。當(dāng)然，人們對證明助手的期望，是希望它能夠檢驗(yàn)比上一節(jié)示例更為復(fù)雜的數(shù)學(xué)證明。2023年11月，一項(xiàng)名為多項(xiàng)式Freiman-Ruzsa猜想（Polynomial Freiman-Ruzsa conjecture）的數(shù)學(xué)定理得到了證明。證明這個源自組合數(shù)學(xué)領(lǐng)域的著名猜想是一項(xiàng)非常艱巨的任務(wù)，但最終由一個杰出的團(tuán)隊(duì)完成：蒂莫西·高爾斯（Timothy Gowers）、本·格林（Ben Green）、弗雷迪·曼納斯（Freddie Manners）和陶哲軒（Terence Tao）。

陶哲軒

這個猜想的證明是一篇 33 頁，基本自成一體的論文（也就是說，論文中的證明并沒有過多依賴其他論文的已有成果）。特別是，這篇論文看起來是那種非常適合嘗試通過像 Lean（Lean 是微軟研究院在 2013 年推出的計(jì)算機(jī)定理證明器，同時也是一門通用函數(shù)式編程語言）這樣的證明助手來驗(yàn)證的類型。因此，由陶哲軒牽頭，大約三十名研究者組成的團(tuán)隊(duì)，集思廣益，致力于將這一證明形式化。

值得注意的是，盡管這是組合數(shù)學(xué)領(lǐng)域的一項(xiàng)成果，但并非所有的參與者都是組合數(shù)學(xué)家。他們甚至不全是數(shù)學(xué)家；其中一些是計(jì)算機(jī)科學(xué)家，還有一些僅僅是享受解謎樂趣的人。在證明形式化的初始階段，會先搭建一個證明框架，從而將整個“謎題”分解成許多部分。這種框架被稱為依賴圖（dependency graph）。

形式化證明多項(xiàng)式Freiman-Ruzsa 猜想過程中期的依賴圖示例。圖片來源于陶哲軒的博客

這是多項(xiàng)式Freiman-Ruzsa 猜想在證明形式化過程中期的依賴圖示例。圖中每個氣泡要么代表一個定義（矩形），要么代表一個定理/引理（橢圓形）?？梢钥吹接屑^指向不同的形狀。當(dāng)某個定理/定義被其他定理/定義需要時，箭頭便會從前者指向后者。隨著時間的推移，所有參與者的貢獻(xiàn)會讓圖表逐漸變綠（這意味著特定的定義或引理已經(jīng)完成了編碼和檢查）。當(dāng)定理被完全形式化時，整張圖表將變成令人滿意的深綠色，最終甚至能給人們帶來大量的多巴胺快感。對于多項(xiàng)式 Freiman-Ruzsa 猜想，這一過程耗時約三周。您可以很容易地將其類比為我們之前的大樹比喻。我們想要接上最終的那根枝條（多項(xiàng)式 Freiman-Ruzsa 猜想），但必須從箭頭所指的那幾個分支開始。

數(shù)學(xué)這門學(xué)科，素來享有"孤軍奮戰(zhàn)的學(xué)科"之名，而這一印象在歷史上不無依據(jù)。下圖通過十個數(shù)學(xué)領(lǐng)域的聚類分析，展示了各領(lǐng)域論文的平均作者數(shù)量。

十個數(shù)學(xué)領(lǐng)域聚類中單篇論文的平均作者數(shù)量。Gen：普通數(shù)學(xué)/歷史/基礎(chǔ)，Disc：離散數(shù)學(xué)/凸幾何，NTAG：數(shù)論/代數(shù)/代數(shù)幾何/群論，Ana：分析與復(fù)分析，OpTh：調(diào)和分析和泛函分析/算子理論，DIEq：分方程和積分方程，OptCS：最優(yōu)化/數(shù)值分析/計(jì)算機(jī)科學(xué)/算法，ProbStat：率論與統(tǒng)計(jì)學(xué)/經(jīng)濟(jì)學(xué)、生物學(xué)應(yīng)用和醫(yī)學(xué)，TopGeom：拓?fù)渑c幾何，MaPh：數(shù)學(xué)物理。

誠然，參與單篇論文研究的數(shù)學(xué)家數(shù)量確實(shí)呈增長趨勢。但是即便如此，能有二十人左右共同參與的數(shù)學(xué)項(xiàng)目，至今依然十分罕見。

除了與其他人共同參與的樂趣外，這種協(xié)作模式的優(yōu)勢在于，對于那些規(guī)模更大、可能也更復(fù)雜的證明，它能讓不同研究者根據(jù)自己的個人興趣與專業(yè)背景，各自投身于證明形式化過程中最契合自身的環(huán)節(jié)。
費(fèi)馬大定理

凱文·巴扎德，由托馬斯·安格斯（Thomas Angus）拍攝

以著名的費(fèi)馬大定理（Fermat’s last theorem）為例，該定理于1994年由安德魯·懷爾斯（Andrew Wiles）在理查德·泰勒（Richard Taylor）的幫助下成功證明，舉世聞名。2024年，英國工程與物理科學(xué)研究委員會（Engineering and Physical Sciences Research Council，EPSRC）撥付了一項(xiàng)五年期資助，支持凱文·巴扎德在 Lean 上完成該定理的形式化證明。

他的最初目標(biāo)是將費(fèi)馬大定理簡化為20世紀(jì)80年代就已知的成果。但是懷爾斯的證明非常復(fù)雜，涉及群論、交換代數(shù)、實(shí)分析、復(fù)分析、代數(shù)幾何、微分幾何等多個數(shù)學(xué)領(lǐng)域的工作。巴扎德坦言自己并非實(shí)分析的擁躉：“如果我傾盡余生去做這個工作，到死我可能都還在做實(shí)分析?！比欢?，隨著項(xiàng)目人數(shù)的增加，這意味著可能更偏愛證明某個領(lǐng)域（比如實(shí)分析）的合作者可以專心做那部分工作，沒有人需要了解整個證明是如何運(yùn)作的。

這是費(fèi)馬大定理立方情形（即兩個立方數(shù)之和不可能等于另一個立方數(shù)）的依賴圖。該圖取自皮特羅·蒙蒂科內(nèi)（Pietro Monticone）關(guān)于費(fèi)馬大定理形式化項(xiàng)目的網(wǎng)站。
機(jī)器學(xué)“形”

如果我們能夠?qū)⑿问交C明助手與大語言模型（large language models，LLMs）如 ChatGPT、DeepSeek、Gemini 或 Llama 結(jié)合使用，這將釋放出巨大潛力。這些人工智能模型在數(shù)學(xué)方面確實(shí)已經(jīng)變得相當(dāng)出色。最近（2025年），更有大語言模型在國際數(shù)學(xué)奧林匹克競賽中達(dá)到了金牌標(biāo)準(zhǔn)。

然而，它們并不完美，目前最大的問題之一無疑就是 “幻覺”，即大語言模型會犯錯誤。凱文·巴扎德解釋道：“關(guān)鍵問題在于，它們該如何改進(jìn)？……目前人們認(rèn)為存在兩種不同的技術(shù)路線，對吧？有些人認(rèn)為我們應(yīng)該繼續(xù)做我們正在做的事，減少模型幻覺，投喂更多數(shù)據(jù)，最終讓它們讀完這間辦公室里所有論文后就能變得更加出色。但我的建議實(shí)際上是，不，我們應(yīng)該教會它們形式化語言，從根本上讓它們不再產(chǎn)生幻覺。所以，誰知道哪條路會勝出……我賭形式化語言這一邊?！?/p>

目前大語言模型還存在一個問題是，當(dāng)遇到瓶頸時，它們的本能不是像人類那樣放棄，而是選擇撒謊或者編造證明。繞開這個問題的一種方法是，要求大語言模型生成符合 Lean 規(guī)范的代碼。也就是說，它們必須先用 Lean 寫出證明，而不是直接生成供人類閱讀的證明文本。然后運(yùn)行 Lean 代碼，它會告訴模型證明哪里不正確，或者是否存在漏洞。這樣，大語言模型就必須檢查自己的錯誤，而不是用那些可能蒙混過關(guān)的含糊表述來逃避檢驗(yàn)。

當(dāng)然，在此之后，它們完全可以將 Lean 代碼轉(zhuǎn)譯回自然語言。若想要讓大語言模型真正能夠開始做研究級數(shù)學(xué)（如果它們能夠做到的話），就必須杜絕其通過糊弄的方式來蒙混過關(guān)的行為。因此，強(qiáng)制其通過 Lean 進(jìn)行運(yùn)作，無疑是實(shí)現(xiàn)這一目標(biāo)的一個好方法。

毫無疑問，要想做到這一點(diǎn)，它們首先需要接受大量 Lean 代碼的訓(xùn)練。幸運(yùn)的是，像費(fèi)馬大定理和多項(xiàng)式 Freiman-Ruzsa 猜想這樣的大型項(xiàng)目，恰好能生成大量這樣的代碼。
艾薩克·牛頓研究所的“大證明”項(xiàng)目

證明形式化是數(shù)學(xué)中一個活躍的研究領(lǐng)域，吸引了數(shù)學(xué)領(lǐng)域最杰出的一些學(xué)者。為這一領(lǐng)域的奠基起到關(guān)鍵作用的是，劍橋大學(xué)艾薩克·牛頓數(shù)學(xué)科學(xué)研究所（Isaac Newton Institute，INI）于2017年開展的一項(xiàng)研究計(jì)劃，名為“大證明”（Big Proof）。在2017年首次"大證明"會議上，大多數(shù)與會者并非數(shù)學(xué)家，而是計(jì)算機(jī)科學(xué)家。艾薩克·牛頓數(shù)學(xué)科學(xué)研究所率先意識到了證明助手對數(shù)學(xué)未來發(fā)展的重要性，在這方面走在了時代前列。

然而，盡管與會數(shù)學(xué)家人數(shù)或許較少，但是這次會議仍然產(chǎn)生了深遠(yuǎn)影響。凱文·巴扎德坦言，正是湯姆·哈爾斯（Tom Hales）在會議上的演講激勵他投身當(dāng)前的研究：“我聽了湯姆·哈爾斯的首場講座，他使用的工具與我相同，但他談?wù)摰南敕ㄊ侨绾问褂眠@些工具開展現(xiàn)代數(shù)學(xué)研究……當(dāng)時我剛剛花了兩周時間證明完根號2是無理數(shù)，我看著這些幻燈片，心想，‘如果能在這個系統(tǒng)中做高等代數(shù)幾何，豈不是很棒嗎？’”

時光流轉(zhuǎn)來到 2025 年，最新一屆“大證明”會議最近如期舉行。這一次，許多數(shù)學(xué)家處于各自領(lǐng)域的最前沿（盡管只有三位菲爾茲獎得主）。形式化數(shù)學(xué)的夢想正煥發(fā)著蓬勃生機(jī)。根據(jù)巴扎德所說，其本科階段的知識體系中，目前僅剩兩個小部分尚未用Lean編碼，而這一領(lǐng)域只會不斷擴(kuò)展！
展望未來

在展望證明助手將如何塑造數(shù)學(xué)的未來時，我們不宜一概而論。然而，如果允許我們持樂觀態(tài)度的話……在未來大語言模型的輔助下，形式化證明助手或許真的有機(jī)會趕上現(xiàn)代數(shù)學(xué)。大衛(wèi)·希爾伯特曾夢想將所有數(shù)學(xué)形式化，而借助證明助手，這一夢想很有可能真的會成為現(xiàn)實(shí)。此外，又有誰知道，我們的數(shù)學(xué)樹上是否還有我們尚未發(fā)現(xiàn)的遺漏分支？而當(dāng)人工智能完全掌握 Lean 的所有能力時，誰又能預(yù)料它可能會創(chuàng)造出怎樣的奇跡呢？

本文經(jīng)授權(quán)轉(zhuǎn)載自微信公眾號“中科院物理所”，原題目為《數(shù)學(xué)界來了個“頂級杠精”，專治各種證明不服！》，
https://plus.maths.org/content/proof-assistants-part-1。

特 別 提 示

1. 進(jìn)入『返樸』微信公眾號底部菜單“精品專欄“，可查閱不同主題系列科普文章。

2. 『返樸』提供按月檢索文章功能。關(guān)注公眾號，回復(fù)四位數(shù)組成的年份+月份，如“1903”，可獲取2019年3月的文章索引，以此類推。