數學中，嚴謹至關重要，但數字化證明是否過猶不及？——譯自量子雜志Quanta Magazine

★置頂zzllrr小樂公眾號（主頁右上角）數學科普不迷路！

數學家們正致力于用Lean計算機程序將所有數學內容形式化，而數學追求嚴謹的歷程漫長且曲折，這段歷史值得他們借鑒。

圖源：Kristina Armitage / Quanta Magazine

作者：Leila Sloman（萊拉·斯洛曼，量子雜志特約通訊員）2026-3-25

譯者：zzllrr小樂（數學科普公眾號）2026-3-26

在古希臘，歐幾里得證明了只要認同一小部分基本原理（即公理），人們就能通過演繹推理發現各類全新的數學真理。但數學家們所稱的這些早期證明，即便依據邏輯法則推導而來，有時也暗藏未闡明的假設，或是依賴易產生誤導的直覺。在這類情況下，證明中細微的漏洞可能被忽略，人們無法絕對確信其正確性。

過去幾個世紀里，數學家們一直試圖填補這些漏洞。到20世紀初，他們確定了想要使用的公理，還引入了不同的邏輯體系和標準，力求讓論證進一步“形式化”——確保若將證明中的每一步推導都清晰呈現，無論過程多么冗長復雜，結論都必然成立。

這場形式化的努力不僅建立了信任，更帶來了諸多意外收獲。推動數學形式化的過程，讓數學家們發現了不同數學領域間全新的關聯，將數學研究引向了意想不到的新方向。明尼蘇達州麥卡利斯特學院的戴維·布雷蘇德（David Bressoud）表示，這一過程讓我們明白：“你往往不知道自己還有哪些未知，也因此要保持謙遜。”

但數學領域的重大突破，必然需要大膽的想法。這些想法往往源于實驗與直覺——探索全新的數學領域，驗證新穎的數學理論，即便你無法證明探索過程中的每一步，都能從邏輯上承接上一步。這種研究數學的方式形式性較弱，初期也容易出現謬誤。

在描繪全新數學圖景所需的創造力，與確保這些圖景真實成立所需的嚴謹性之間，找到卓有成效的平衡并非易事。有時，形式化會打破這種平衡。在一些數學家眼中代表著對更高確定性的追求，在另一些人看來，或許只是繁瑣的鉆牛角尖，或是阻礙發展的壁壘。

歐幾里得的《幾何原本》，是西方數學史上首次大規模的形式化嘗試。它確立的命題證明演繹法，至今仍在沿用。上圖為1482年問世的《幾何原本》首個印刷版本內頁。

圖源：福爾杰莎士比亞圖書館/知識共享 署名-相同方式共享4.0協議

如今，數學家們正開展迄今最宏大的形式化項目：試圖用一種名為Lean的計算機語言重寫所有數學內容，再由程序自動驗證這些證明。用Lean撰寫證明需要投入大量的時間和精力，但截至目前，該程序已驗證了超過26萬個定理，有望為數學搭建起人類所能想象的最堅實的基礎。

與以往的數學形式化嘗試一樣，Lean也引發了數學家們復雜的情緒。一些數學家期待將繁瑣的驗證工作交由計算機完成，將Lean視為改變數學研究方式的潛在革命性工具；另一些則認為，時間和資源應用在其他更有價值的研究上，更有甚者擔心，以Lean為核心的研究方式，會扭曲數學的真正價值。一場關于“如何平衡發現數學新關聯所需的創造力，與確保每一步邏輯都無懈可擊所需的嚴謹性”的討論，正在全球各數學系的走廊里展開。

設定邊界

數學追求嚴謹的歷程中，一個重要里程碑的出現，源于一項曠世數學成就背后隱藏的問題。

17世紀末，艾薩克·牛頓和戈特弗里德·萊布尼茨各自獨立創立了微積分——這一用于研究函數在某一點變化速率的方法。但從非形式化的角度來看，微積分的雛形早在數百年前就已出現。事實上，公元前3世紀，阿基米德的研究就已具備微積分的雛形。為計算圓的面積，他先研究了由直線構成的圖形（即多邊形）的面積，通過不斷增加多邊形的邊數，去逼近一個極限值：圓的面積。牛頓和萊布尼茨采用了類似的思路，借助極限來闡釋變化的概念。

在這本 1897 年譯本的著作《論劈錐曲面體與橢球體》 On Conoids and Spheroids 中，阿基米德（Archimedes）提出的諸多思想，在千年之后的微積分發展進程中發揮了關鍵作用。

內容出自 T?L?希思（T.L. Heath）校訂的《阿基米德著作集》，劍橋大學出版社 1897 年版，公有領域。

微積分一經誕生，便迅速在數學和物理學領域發揮重要作用，但以現代標準來看，它在當時并不具備形式化的特征：牛頓和萊布尼茨的論文回避了一些模糊不清的問題。微積分以無窮和無窮小量（即微元）為核心概念，可兩人僅用模糊的幾何語言對其進行定義；若公式使用不當，便會得出諸如除以零這類毫無意義的計算結果。

在之后的150年里，這一問題并未引發任何麻煩，科學家們早已摸索出微積分的有效適用場景。但到了19世紀初，數學家們開始遇到一些違背直覺的現象——比如無窮級數、形態怪異的鋸齒曲線等。

這一時期，藝術和科學領域也正經歷大范圍的質疑與反思，哲學家、畫家、作家和研究人員紛紛開始探尋認知的邊界。哥倫比亞大學的科學史學家阿爾瑪·施泰因加特（Alma Steingart）表示：“直覺開始受到質疑，人們意識到，直覺可能會引向錯誤的方向。”

戈特弗里德?萊布尼茨（Gottfried Leibniz，上）與艾薩克?牛頓（Isaac Newton，下）于 17 世紀各自獨立創立了微積分。多年來，兩人就微積分核心思想的首創權爭執不休。

肖像作者：克里斯托弗?伯恩哈德?弗蘭克 Christoph Bernhard Francke，上圖；戈弗雷?內勒 Godfrey Kneller，下圖

尼爾斯·阿貝爾（Niels Abel）、奧古斯丁-路易·柯西（Augustin-Louis Cauchy）、卡爾·魏爾斯特拉斯（Karl Weierstrass）等著名數學家意識到，要理解研究中出現的這些奇異級數和曲線，必須回歸最基礎的定義：什么是函數？函數的連續性意味著什么？無窮多個對象相加的本質是什么？

他們為這些問題給出了形式化的定義（例如，魏爾斯特拉斯提出的極限精確定義，至今仍被學生沿用）。這些新定義讓數學家們得以以前所未有的深度和嚴謹性研究函數，最終催生了分析學這一數學分支。

如今，分析學已是數學領域最重要的分支之一，數學家們借助它研究從流體流動、電流傳導，到遙遠恒星的化學成分等各類問題，且它與數論、幾何學等歷史更悠久的數學分支，以及幾乎所有其他數學領域都有著緊密關聯。而微積分的形式化，也推動了集合論的誕生——這一理論確立了現代數學的底層規則，如今集合論本身也成為了一個活躍的研究領域。

19 世紀，奧古斯丁 - 路易?柯西（Augustin-Louis Cauchy，上）與卡爾?魏爾斯特拉斯（Karl Weierstrass，下）重新定義了微積分中的核心概念，由此催生了現代分析學這一數學分支。

圖源：史密森尼學會圖書館 The Smithsonian Libraries，左圖；公有領域 ，右圖

即便如此，當時也有一些研究者對這股形式化浪潮心存顧慮。1899年，物理學家奧利弗·亥維賽（Oliver Heaviside）寫道：“當嚴謹派的冷水澆滅了熱情，便再難讓人提起興致。”

科學史學家耶斯佩爾·呂岑（Jesper Lützen）在回顧這一時期時指出 https://www.ams.org/publications/authors/books/postpub/hmath-24 ：“分析學在收獲嚴謹性和一般性的同時，失去了簡潔與優雅，也與直覺漸行漸遠。許多數學家對這一趨勢感到惋惜，卻又無力改變。”

關鍵的是，嚴謹派數學家與反對者最終達成了妥協：數學家們繼續沿用柯西和魏爾斯特拉斯提出的嚴謹定義，同時也構建了新的框架，讓亥維賽等科學家能更自由地對無窮和無窮小量進行計算。

倫敦帝國理工學院的凱文·巴扎德說：“形式化會迫使你用正確的方式思考數學，也會迫使你成為一名‘藝術家’。”

換言之，形式化并非他們的唯一目標。事實上，這段歷史的關鍵，在于形式化背后的初衷：其研究范圍相對狹窄，魏爾斯特拉斯及其同僚當時正研究與函數行為相關的特定問題，形式化只是他們解決這些問題的手段。而分析學、集合論及其他形式化體系的發展，都是在此基礎上自然展開的。

大數學家戴維·希爾伯特在1905年寫道 https://www.leocorry.com/_files/ugd/e6fef7_dbe9131a54ed48c996cd517588422cdd.pdf ：“科學大廈的構建，并非像建造房屋那樣，先牢牢打下地基，再著手建造、擴建房間；相反，科學家應先找到可以自由探索的‘舒適空間’，只有當各處出現松動的地基無法支撐房間擴建的跡象時，再去加固地基。”

他接著說：“這并非缺陷，而是科學發展正確且健康的路徑。”

畢竟，當形式化的目標超出了加固松動地基的范疇，其產生的影響也會截然不同。

刻板的學術體系

對清晰性和嚴謹性的追求，也可能走向極端。

數學界有一個著名（或說聲名狼藉，取決于不同人的看法）的學術流派，由一個名為布爾巴基的數學家秘密團體提出，便是典型的例子。

20世紀30年代中期，法國的數學研究已衰落數十年：第一次世界大戰讓法國失去了一代極具潛力的學生和研究者；各大學的數學教學缺乏協調、體系零散，使用的教材也早已過時。于是，幾位年輕的數學家聯合起來，創立了布爾巴基學派。他們最初的目標很樸素：編寫一套全新、更系統的教材，讓法國的數學課程體系跟上現代步伐。但很快，他們的野心不斷膨脹。如今，成員身份仍處于保密狀態的布爾巴基學派，已出版了40多卷著作，涵蓋了數學領域的所有分支。

1930年代創立的秘密數學團體布爾巴基學派（Bourbaki），將嚴謹、抽象與邏輯奉為至高準則。該學派創始成員包括亨利?嘉當（Henri Cartan，站立者，最左側）、安德烈?韋伊（André Weil，站立者，右數第二位） 以及索萊姆?曼德爾布羅伊（Szolem Mandelbrojt，端坐者，右側）。

布爾巴基學派的真正遺產，并非著作中的內容，而是其研究風格。該學派將抽象性置于首位，摒棄具體的例子和計算，只關注最具一般性的命題。他們呈現的每一個證明，都是一系列邏輯推導的組合，通常不會提及背后的直覺和原理。

特拉維夫大學的科學史學家利奧·科里（Leo Corry）評價道：“這是一種極具形式化的風格，刻板且嚴苛。”

布爾巴基學派的一本教科書

布爾巴基學派的理念迅速傳播，幾乎影響了全球的數學研究。巴黎-薩克雷大學的帕特里克·馬索（Patrick Massot）說：“其影響力巨大，該學派最成功的研究成果，已成為數學通用知識和研究風格的一部分，讓人難以想象在此之前的數學研究是何種模樣。”

數學學科的體系變得愈發嚴密，卻也愈發抽象、難以理解。數學家莫里斯·馬沙爾（Maurice Mashaal）寫道 https://bookstore.ams.org/bourbaki/ ：“從教學的角度來看，這絕非明智的選擇。”但該學派對抽象性的強調，對研究型數學的塑造，其影響則難以評估。

一些數學家推崇布爾巴基學派的研究方法，馬索認為，通過抽象化和追求優雅，“你會被迫去理解事物的核心運作邏輯，分辨何為關鍵、何為無關緊要的干擾信息”。在這種觀點下，形式化帶來了思維的清晰性。

但布爾巴基學派的研究也帶來了意想不到的后果，其使用的術語和研究風格，并非適用于所有數學分支。例如，組合數學（常被描述為研究計數的科學）和圖論（研究網絡的科學）具有高度的具象性和直觀性。因此，數十年來，這兩個領域在美國和歐洲部分地區的頂尖研究機構中一直被邊緣化，僅在匈牙利等布爾巴基學派影響力有限的地區得以蓬勃發展，也就不足為奇了。

孟菲斯大學的貝拉·博洛巴斯（Belá Bollobás）說：“圖論曾是拓撲學的‘貧民窟’，這種狀況直到最近才有所改變，真的是非常近。”

南加州大學的阿拉溫德·阿索克（Aravind Asok）則擔心，過度強調形式化，可能會讓數學研究變得同質化。

即便是在布爾巴基框架下蓬勃發展的代數學、拓撲學、分析學等領域，一些數學家也認為該學派的影響過于深遠。在他們看來，證明的撰寫方式和理論的構建模式，已經變得過于單一。

阿索克說：“能明顯感覺到，數學研究的文化多樣性有所降低。”例如，在布爾巴基學派興起之前，代數幾何有著多種研究范式：法國的研究方法以分析學為基礎，而意大利則盛行幾何化的研究風格。

隨著布爾巴基學派的影響力不斷擴大，缺乏嚴謹性、存在諸多謬誤的意大利代數幾何學派迅速衰落。誠然，代數幾何的研究因此變得更加可靠，但布爾巴基學派在切斷其他潛在發展路徑的同時，也帶來了新的問題。阿索克表示：“我不希望數學研究被一種模式主導，數學有著值得被傳承的文化歷史。”

證明與前景

盡管柯西、魏爾斯特拉斯和布爾巴基學派已竭盡全力，但真正的形式化證明，始終停留在理論層面，從未成為實踐主流。如今，一些數學家希望計算機能改變這一現狀。

自1960年代起，研究人員便開始開發名為“證明助手”的計算機程序。數學家使用證明助手時，需用計算機能理解的語言，撰寫證明的每一行內容（包括所有定義），再由程序檢驗邏輯的正確性。只要有一步推導無法承接上一步——哪怕是未能嚴謹證明1+1=2這類微小的細節，程序也不會認定該證明有效。

目前，數學家們正希望借助Lean這款證明助手，將所有數學內容形式化。他們已在Lean中構建了包含超過12萬個定義的庫，并驗證了25萬個定理。有多位數學家負責維護這一數據庫，及時更新內容并審核新的研究成果（其中部分人全職從事這項工作）。該項目已獲得超過1000萬美元的資金支持，大部分來自億萬富翁金融家阿列克謝·格爾科（Alex Gerko）。

證明助手的工作原理

證明助手Lean通過檢驗數學家的推導過程、自動化證明中的部分步驟，協助其證明定理。

1. 數學家在Lean中搭建證明的基本框架，設定推導步驟的順序

2. Lean的數學庫（mathlib）中包含名為“策略”（tactic）的程序，可執行證明中的具體推導步驟

3. 核心算法依據簡單的規則，檢驗證明的正確性

4. 驗證通過的定理，會被納入mathlib數學庫中

（mathlib：用Lean語言編寫的數學知識庫，數學家會持續為其補充新的知識）

圖源：Samuel Velasco / Quanta Magazine 譯制：zzllrr小樂公眾號

羅格斯大學的阿列克謝·康托羅維奇（Alex Kontorovich）稱，Lean具有“革命性”，部分原因在于它能將單個證明拆解為多個部分，各部分可獨立處理、驗證，還能在其他證明中復用。“試想一下，倘若每次建造宇宙飛船，每位工程師都必須了解每一個組件的全部細節——從鐵礦石的開采、冶煉，到組件的設計。而如今，借助這些形式化體系，數學家們首次可以像‘外購零件’一樣開展研究，無需事事親力親為。”

但在Lean中撰寫并審核定義和證明，通常需要數月時間（有些情況下只需幾周，有些則超過一年）。因此，一些數學家擔心，將時間和資源投入其中得不償失。他們認為，盡管證明驗證很重要，但人工檢驗的方式一直運轉良好。阿索克表示，盡管“數學文獻中存在大量謬誤，但我的經驗是，數學體系具有驚人的穩健性”，換言之，數學這座大廈完全崩塌的風險微乎其微。

盡管如此，Lean的使用也催生了新的數學研究成果。2019年，數學家彼得·舒爾茨（Peter Scholze）手工撰寫了一個定理的證明，該定理本將成為其新數學理論的核心。但這個證明極為復雜，舒爾策也難以確定其正確性。于是在2020年末，由約翰·科梅林（Johan Commelin）和亞當·托帕茲（Adam Topaz）領銜的數學家團隊，著手在Lean中對該證明進行形式化驗證。數月后，他們證實了證明的正確性，讓數學家們對舒爾策的新理論更有信心，且在這一過程中，他們找到了更簡潔的證明方式，完善了舒爾策最初的一些想法。

倫敦帝國理工學院的凱文·巴扎德（Kevin Buzzard）是Lean的堅定支持者，他說：“形式化會迫使你用正確的方式思考數學，也會迫使你成為一名‘藝術家’。”過去一年，巴扎德一直致力于用Lean對費馬大定理的證明進行形式化處理 https://imperialcollegelondon.github.io/FLT/ ——這一重要數學成果的證明過程，以冗長復雜著稱。

凱文?巴扎德（Kevin Buzzard）目前正借助 Lean 工具對費馬大定理的證明過程進行形式化處理，這一定理是數學領域最負盛名的成果之一。“我希望這個論證能成為一件精妙的杰作，” 他說，“我希望它能通俗易懂、令人信服。”

此外，當下為開發Lean投入時間和精力，或許是一項極具價值的投資，因為人工智能在未來的數學研究中，必將扮演更重要的角色。當數學家嘗試借助人工智能撰寫非形式化證明時，用Lean這類程序驗證其準確性，會變得愈發重要（況且，人工智能已開始助力更高效地撰寫Lean證明）。

盡管如此，Lean的廣泛應用也伴隨著風險：它是否會像布爾巴基學派一樣，悄然改變數學家們的研究選題傾向？

不斷演變的“生命體”

在Lean的體系中，數學研究的概念、方法和理念多樣性，幾乎沒有生存空間。

一方面，Lean中每一個新證明，都只能使用已驗證并存儲在其庫中的形式化定義和定理，這意味著這些定義和證明必須能無縫銜接；另一方面，更新或修改一個定義，會引發多米諾骨牌效應：基于舊定義撰寫的證明，可能無法適配新定義。

這可能會成為一大問題。西蒙弗雷澤大學的斯蒂芬妮·迪克（Stephanie Dick）表示，數學“并非一個固定、有限、已完成形式化的體系，而是一個不斷演變的生命體，其研究范疇始終在變化”。

斯蒂芬妮?迪克（Stephanie Dick）擔憂，證明助手這類新技術，可能會潛移默化地影響數學家在研究中選擇探索的問題方向。

圖源：埃里克?蘇卡 Eric Sucar / 賓夕法尼亞大學

正因如此，此前嘗試將數學成果數字化的項目（例如1994年提出的QED聲明 https://www.cs.ru.nl/~freek/qed/qed.html ），很快就陷入了關于“使用何種定義和框架”的爭論。迪克說：“從原則上講，所有人都認同這一想法，但實際操作起來卻困難重重。人們會在編程語言的選擇上產生分歧，甚至對這類項目是否具備可行性，也存在根本性的爭議。”

為避免此類分歧，一群專注的Lean使用者負責確定哪些定義應納入Lean的庫，以及如何對這些定義進行編碼——卡內基梅隆大學的西蒙·德迪奧（Simon DeDeo）表示，這一模式與維基百科的運營方式類似。

約翰斯·霍普金斯大學的數學家埃米莉·里爾（Emily Riehl）說：“這確實是一個社群，成員都在為社群的整體利益努力。”截至目前，這一模式運轉良好，決策過程也基本保持民主。但她也表示：“其弊端在于，最終只會得出一個決策，而很多情況下，并不存在唯一正確的答案，有人會滿意，就必然有人失望。”

正如布爾巴基學派的方法僅適用于特定數學領域，Lean的語言體系及其庫中的定義選擇，也并非對所有數學分支都同樣適用：例如，它對數論和代數幾何的適配性較好，對圖論和范疇論則不然。

這只是Lean可能讓數學研究變得同質化的一個方面。迪克指出，過往的技術——即便是數學符號的選擇，也悄然改變了數學家的研究方式。Lean可能會在數學家未察覺的情況下，促使他們專注于研究那些更易形式化的概念。她說：“我已經發現了許多類似的案例，研究重心、直覺和理解方式，會從數學問題本身，轉向這個系統的運行規則。”

Lean無疑帶來了諸多值得期待的可能，但里爾認為，數學家們應嘗試使用多種證明助手，而非單純依賴Lean。不過，考慮到形式化研究需要投入大量精力，她也不確定這一想法的可行性。

過度修正

數個世紀以來，數學家們一直將“能否驗證證明的每一步”作為追求嚴謹性的核心標準，但并非向來如此。對17世紀的笛卡爾而言，嚴謹意味著能在頭腦中構建一個概念，并直觀理解其成立的原因。普林斯頓高等研究院的阿克沙伊·文卡特什（Akshay Venkatesh）表示，正因如此，早期的數學證明“帶有一種質樸的厚重感”。

他說：“這類證明并非形式上優雅的論證，卻能讓普通人輕松理解。”誠然，現代的數學證明更加優雅，卻也愈發晦澀，難以讓人理解其核心。（有趣的是，巴扎德在談及對Lean影響證明撰寫方式的期待時，也用到了類似的表述：“我希望這個論證成為一件美的作品，能讓人輕松理解、心悅誠服。”）

這一趨勢，反映出一個如今被視為理所當然的觀點：證明應是數學的核心。文卡特什說：“毫無疑問，證明的概念是數學的基礎組成部分，但值得質疑的是，它是否應成為定義數學的唯一特征。”

借助Lean進行形式化，將延續這種以證明為核心的趨勢，但這并非數學家們設想的數學發展唯一未來。阿索克表示，研究者們被灌輸了一種觀念——“數學研究的唯一發展方向，是讓論文都通過Lean完成形式化驗證”。“而我認為，另一種可行的方向是，我們稍作停頓，減少研究成果的產出。但這與當下的學術激勵機制相悖。”

我們無法預測Lean形式化會以何種方式影響數學發展，但從歷史中可以明確的是，數學具有自我修正的能力，而這一輪形式化浪潮的未來，終將超出我們的想象。

參考資料

https://www.quantamagazine.org/in-math-rigor-is-vital-but-are-digitized-proofs-taking-it-too-far-20260325/

小樂數學科普近期文章

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

收藏、分享、轉載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數學科普不迷路！