數(shù)學(xué)中，嚴(yán)謹(jǐn)至關(guān)重要，但數(shù)字化證明是否過(guò)猶不及？——譯自量子雜志Quanta Magazine

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

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

圖源：Kristina Armitage / Quanta Magazine

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

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

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

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

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

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

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

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

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

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

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

設(shè)定邊界

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

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

在這本 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)來(lái)看，它在當(dāng)時(shí)并不具備形式化的特征：牛頓和萊布尼茨的論文回避了一些模糊不清的問題。微積分以無(wú)窮和無(wú)窮小量（即微元）為核心概念，可兩人僅用模糊的幾何語(yǔ)言對(duì)其進(jìn)行定義；若公式使用不當(dāng)，便會(huì)得出諸如除以零這類毫無(wú)意義的計(jì)算結(jié)果。

在之后的150年里，這一問題并未引發(fā)任何麻煩，科學(xué)家們?cè)缫衙鞒鑫⒎e分的有效適用場(chǎng)景。但到了19世紀(jì)初，數(shù)學(xué)家們開始遇到一些違背直覺的現(xiàn)象——比如無(wú)窮級(jí)數(shù)、形態(tài)怪異的鋸齒曲線等。

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

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

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

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

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

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

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

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

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

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

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

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

換言之，形式化并非他們的唯一目標(biāo)。事實(shí)上，這段歷史的關(guān)鍵，在于形式化背后的初衷：其研究范圍相對(duì)狹窄，魏爾斯特拉斯及其同僚當(dāng)時(shí)正研究與函數(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)松動(dòng)的地基無(wú)法支撐房間擴(kuò)建的跡象時(shí)，再去加固地基。”

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

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

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

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

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

20世紀(jì)30年代中期，法國(guó)的數(shù)學(xué)研究已衰落數(shù)十年：第一次世界大戰(zhàn)讓法國(guó)失去了一代極具潛力的學(xué)生和研究者；各大學(xué)的數(shù)學(xué)教學(xué)缺乏協(xié)調(diào)、體系零散，使用的教材也早已過(guò)時(shí)。于是，幾位年輕的數(shù)學(xué)家聯(lián)合起來(lái)，創(chuàng)立了布爾巴基學(xué)派。他們最初的目標(biāo)很樸素：編寫一套全新、更系統(tǒng)的教材，讓法國(guó)的數(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é)派將抽象性置于首位，摒棄具體的例子和計(jì)算，只關(guān)注最具一般性的命題。他們呈現(xiàn)的每一個(gè)證明，都是一系列邏輯推導(dǎo)的組合，通常不會(huì)提及背后的直覺和原理。

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

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

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

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

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

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

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

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

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

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

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

證明與前景

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

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

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

證明助手的工作原理

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

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

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

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

4. 驗(yàn)證通過(guò)的定理，會(huì)被納入mathlib數(shù)學(xué)庫(kù)中

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

圖源：Samuel Velasco / Quanta Magazine 譯制：zzllrr小樂公眾號(hào)

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

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

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

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

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

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

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

不斷演變的“生命體”

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

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

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

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

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

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

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

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

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

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

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

過(guò)度修正

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

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

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

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

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

參考資料

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

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

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

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評(píng)論、點(diǎn)贊、在看、在聽

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

查看原始文章出處

點(diǎn)擊zzllrr小樂

公眾號(hào)主頁(yè)

右上角

置頂★加星

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