一個“吹毛求疵”的學生，正在改變數學證明

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

撰文 | Ben Watkins

翻譯 | LogicMoriaty

審校 | 7號機

人類數學家難免出錯。證明助手應運而生，助其查漏補缺，而在這個過程中，它們也將數學轉化成了一種高度合作的體驗。
什么是證明？

數學只是一種依照特定簡單規則，在紙上操作無意義符號的游戲。

——大衛·希爾伯特（David Hilbert）

這話聽起來有些悲觀。

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

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

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

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

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

同行評審通常就是解決這個問題的方法。也就是說，當一篇論文發表時，一小群其他的數學家會檢查你的工作。然而，假如這些同行也沒發現你的錯誤怎么辦？更何況，如今動輒數百頁的長篇論文屢見不鮮。所以實際上，單憑人力根本無力全面檢查。

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

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

例如，四色定理的第一個正確證明是由肯尼斯·阿佩爾（Kenneth Appel）和沃爾夫岡·哈肯（Wolfgang Haken）于1976年給出的。他們通過將需要驗證的可能反例的數量從無窮多（相當龐大的一個數量）減少到1,834個（依然很多，但是已大幅減少）來完成這一證明。隨后，他們借助計算機驗證了這些情形均不構成反例。完整的證明發表，并附有超過400頁的微縮膠片補充材料。其篇幅之長，對于任何（心智正常的）人來說，根本不可能逐一檢查。

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

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

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

這種如同“杠精”一樣的過分嚴謹在做數學時并不常見，但它卻可以使我們放心，當代碼能夠運行時，證明肯定是正確的。下面的部分將進一步介紹如何使用證明助手證明其他的復雜定理，以及它們如何改變人們研究數學的方式。
證明助手：創作社群

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

陶哲軒

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

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

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

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

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

十個數學領域聚類中單篇論文的平均作者數量。Gen：普通數學/歷史/基礎，Disc：離散數學/凸幾何，NTAG：數論/代數/代數幾何/群論，Ana：分析與復分析，OpTh：調和分析和泛函分析/算子理論，DIEq：分方程和積分方程，OptCS：最優化/數值分析/計算機科學/算法，ProbStat：率論與統計學/經濟學、生物學應用和醫學，TopGeom：拓撲與幾何，MaPh：數學物理。

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

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

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

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

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

這是費馬大定理立方情形（即兩個立方數之和不可能等于另一個立方數）的依賴圖。該圖取自皮特羅·蒙蒂科內（Pietro Monticone）關于費馬大定理形式化項目的網站。
機器學“形”

如果我們能夠將形式化證明助手與大語言模型（large language models，LLMs）如 ChatGPT、DeepSeek、Gemini 或 Llama 結合使用，這將釋放出巨大潛力。這些人工智能模型在數學方面確實已經變得相當出色。最近（2025年），更有大語言模型在國際數學奧林匹克競賽中達到了金牌標準。

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

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

當然，在此之后，它們完全可以將 Lean 代碼轉譯回自然語言。若想要讓大語言模型真正能夠開始做研究級數學（如果它們能夠做到的話），就必須杜絕其通過糊弄的方式來蒙混過關的行為。因此，強制其通過 Lean 進行運作，無疑是實現這一目標的一個好方法。

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

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

然而，盡管與會數學家人數或許較少，但是這次會議仍然產生了深遠影響。凱文·巴扎德坦言，正是湯姆·哈爾斯（Tom Hales）在會議上的演講激勵他投身當前的研究：“我聽了湯姆·哈爾斯的首場講座，他使用的工具與我相同，但他談論的想法是如何使用這些工具開展現代數學研究……當時我剛剛花了兩周時間證明完根號2是無理數，我看著這些幻燈片，心想，‘如果能在這個系統中做高等代數幾何，豈不是很棒嗎？’”

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

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

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

特 別 提 示

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

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