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

數(shù)學(xué)家們正致力于用Lean計算機(jī)程序?qū)⑺袛?shù)學(xué)內(nèi)容形式化，而數(shù)學(xué)追求嚴(yán)謹(jǐn)?shù)臍v程漫長且曲折，這段歷史值得他們借鑒。

圖源：Kristina Armitage / Quanta Magazine

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

譯者：zzllrr小樂（數(shù)學(xué)科普公眾號）2026-3-26

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

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

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

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

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

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

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

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

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

設(shè)定邊界

數(shù)學(xué)追求嚴(yán)謹(jǐn)?shù)臍v程中，一個重要里程碑的出現(xiàn)，源于一項曠世數(shù)學(xué)成就背后隱藏的問題。

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

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

內(nèi)容出自 T?L?希思（T.L. Heath）校訂的《阿基米德著作集》，劍橋大學(xué)出版社 1897 年版，公有領(lǐng)域。

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

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

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

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

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

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

他們?yōu)檫@些問題給出了形式化的定義（例如，魏爾斯特拉斯提出的極限精確定義，至今仍被學(xué)生沿用）。這些新定義讓數(shù)學(xué)家們得以以前所未有的深度和嚴(yán)謹(jǐn)性研究函數(shù)，最終催生了分析學(xué)這一數(shù)學(xué)分支。

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

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

圖源：史密森尼學(xué)會圖書館 The Smithsonian Libraries，左圖；公有領(lǐng)域 ，右圖

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

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

關(guān)鍵的是，嚴(yán)謹(jǐn)派數(shù)學(xué)家與反對者最終達(dá)成了妥協(xié)：數(shù)學(xué)家們繼續(xù)沿用柯西和魏爾斯特拉斯提出的嚴(yán)謹(jǐn)定義，同時也構(gòu)建了新的框架，讓亥維賽等科學(xué)家能更自由地對無窮和無窮小量進(jìn)行計算。

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

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

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

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

畢竟，當(dāng)形式化的目標(biāo)超出了加固松動地基的范疇，其產(chǎn)生的影響也會截然不同。

刻板的學(xué)術(shù)體系

對清晰性和嚴(yán)謹(jǐn)性的追求，也可能走向極端。

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

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

1930年代創(chuàng)立的秘密數(shù)學(xué)團(tuán)體布爾巴基學(xué)派（Bourbaki），將嚴(yán)謹(jǐn)、抽象與邏輯奉為至高準(zhǔn)則。該學(xué)派創(chuàng)始成員包括亨利?嘉當(dāng)（Henri Cartan，站立者，最左側(cè)）、安德烈?韋伊（André Weil，站立者，右數(shù)第二位） 以及索萊姆?曼德爾布羅伊（Szolem Mandelbrojt，端坐者，右側(cè)）。

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

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

布爾巴基學(xué)派的一本教科書

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

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

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

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

孟菲斯大學(xué)的貝拉·博洛巴斯（Belá Bollobás）說：“圖論曾是拓?fù)鋵W(xué)的‘貧民窟’，這種狀況直到最近才有所改變，真的是非常近�！�

南加州大學(xué)的阿拉溫德·阿索克（Aravind Asok）則擔(dān)心，過度強(qiáng)調(diào)形式化，可能會讓數(shù)學(xué)研究變得同質(zhì)化。

即便是在布爾巴基框架下蓬勃發(fā)展的代數(shù)學(xué)、拓?fù)鋵W(xué)、分析學(xué)等領(lǐng)域，一些數(shù)學(xué)家也認(rèn)為該學(xué)派的影響過于深遠(yuǎn)。在他們看來，證明的撰寫方式和理論的構(gòu)建模式，已經(jīng)變得過于單一。

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

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

證明與前景

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

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

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

證明助手的工作原理

證明助手Lean通過檢驗數(shù)學(xué)家的推導(dǎo)過程、自動化證明中的部分步驟，協(xié)助其證明定理。

1. 數(shù)學(xué)家在Lean中搭建證明的基本框架，設(shè)定推導(dǎo)步驟的順序

2. Lean的數(shù)學(xué)庫（mathlib）中包含名為“策略”（tactic）的程序，可執(zhí)行證明中的具體推導(dǎo)步驟

3. 核心算法依據(jù)簡單的規(guī)則，檢驗證明的正確性

4. 驗證通過的定理，會被納入mathlib數(shù)學(xué)庫中

（mathlib：用Lean語言編寫的數(shù)學(xué)知識庫，數(shù)學(xué)家會持續(xù)為其補充新的知識）

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

羅格斯大學(xué)的阿列克謝·康托羅維奇（Alex Kontorovich）稱，Lean具有“革命性”，部分原因在于它能將單個證明拆解為多個部分，各部分可獨立處理、驗證，還能在其他證明中復(fù)用�！霸囅胍幌拢热裘看谓ㄔ煊钪骘w船，每位工程師都必須了解每一個組件的全部細(xì)節(jié)——從鐵礦石的開采、冶煉，到組件的設(shè)計。而如今，借助這些形式化體系，數(shù)學(xué)家們首次可以像‘外購零件’一樣開展研究，無需事事親力親為�！�

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

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

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

凱文?巴扎德（Kevin Buzzard）目前正借助 Lean 工具對費馬大定理的證明過程進(jìn)行形式化處理，這一定理是數(shù)學(xué)領(lǐng)域最負(fù)盛名的成果之一�！拔蚁Ｍ@個論證能成為一件精妙的杰作，” 他說，“我希望它能通俗易懂、令人信服。”

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

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

不斷演變的“生命體”

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

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

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

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

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

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

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

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

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

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

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

過度修正

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

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

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

借助Lean進(jìn)行形式化，將延續(xù)這種以證明為核心的趨勢，但這并非數(shù)學(xué)家們設(shè)想的數(shù)學(xué)發(fā)展唯一未來。阿索克表示，研究者們被灌輸了一種觀念——“數(shù)學(xué)研究的唯一發(fā)展方向，是讓論文都通過Lean完成形式化驗證”�！岸艺J(rèn)為，另一種可行的方向是，我們稍作停頓，減少研究成果的產(chǎn)出。但這與當(dāng)下的學(xué)術(shù)激勵機(jī)制相悖�！�

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

參考資料

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

小樂數(shù)學(xué)科普近期文章

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

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見易得

易傳易及

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

收藏、分享、轉(zhuǎn)載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數(shù)學(xué)科普不迷路！