“在我看來,，在傳統(tǒng)的人類審查與計算機驗證之間的選擇，就像科學(xué)上在日晷與原子鐘之間的選擇一樣,?！薄獪贰ずＲ?Tom Hales, 參見 [4])

“由于計算機與人是非常不同的,，計算機的快速進展促使這點發(fā)生了戲劇性的變化,。例如，阿佩爾(Appel) 與哈肯(Haken)使用了巨量的自動運算完成了四色定理的證明,，引起了大量的爭論,。在我看來,，這些爭論幾乎不涉及到人們對定理的真實性或者證明的正確性。這反映出了,，除了對‘定理是正確的’這種知識以外,，人類還想要理解定理，這是一種持續(xù)的欲望,?！?——比爾·瑟斯頓( Bill Thurston,參見[6])

一個機器檢驗的證明(machine-checked proof)是在叫做“證明助手”(proof assistant)的軟件中撰寫的證明。這個證明助手保證了撰寫的明證之于“數(shù)學(xué)公理”與“邏輯規(guī)則”是可以編譯的,。在定理證明中使用計算機的影響是兩極化的,。關(guān)于這個話題，上面的引用代表了涉及到這個主題的一些觀點,。

1.到底什么是計算機輔助證明？

2.使用計算機來證明定理有什么長處與缺點,？

3.對證明助手的學(xué)習(xí)使用有興趣的人,，應(yīng)該如何起步呢？

動機的問題

計算機輔助的證明是一門技術(shù),。當(dāng)時使用舊技術(shù)不能解決一些問題的時候，數(shù)學(xué)家就會關(guān)心新技術(shù),。這就是我們的動機的問題：

我們來看兩個已經(jīng)解決了的問題。第一個是魔方,。第二個是安德魯·懷爾斯(Andrew Wiles)作出的費馬大定理的證明,。

證明丟番圖方程與解魔方之間有一個很大的差別：當(dāng)一個人解決了魔方的問題，他立即知道問題解決了,，然而懷爾斯的證明花費了幾個月的時間來進行正式的審查,。

隨著我們數(shù)學(xué)教育階段的提升。我們檢查答案的能力在下降,。比如,，我的啟蒙數(shù)學(xué)課是我母親教我的數(shù)數(shù)。就比較小的加法來說,，我可以使用數(shù)手指的辦法來檢查我的答案,。從一到十的基本數(shù)字以及用手指驗證答案都是母親教會我的。一個人學(xué)會了解代數(shù)方程,，也就學(xué)會了使用變量代換來檢查答案,。檢查微積分就更加的棘手了，我們尚可以對Wolfram Alpha報以比較大的信心（譯者注,，Wolfram Alpha是一個數(shù)學(xué)軟件,，可以做符號運算。具有計算積分的功能，還能告訴你得到答案的步驟）,。至于實分析與抽象代數(shù),，學(xué)生們最終是把作業(yè)交給老師，看看教授們是否相信他們的論證,，這樣來檢查他們的作業(yè)正確與否的,。

什么是證明助手?

一個計算機證明助手可以對數(shù)學(xué)論證做更加系統(tǒng)化的檢查。用戶使用半形式化的語言(既不像形式邏輯那么形式化,，也不像日常數(shù)學(xué)那么非形式化)來撰寫他們的證明。證明助手基于某些數(shù)學(xué)基礎(chǔ)來檢查證明,。正常情況下,，我們想起數(shù)學(xué)基礎(chǔ)，我們想到的是集合論,。然后由于技術(shù)的原因，證明助手是就“類型論”的基礎(chǔ)來實現(xiàn)的,。在提出ZFC集合論的大致同時,，羅素與懷特海提出了類型論作為另一個數(shù)學(xué)基礎(chǔ)。有不同的數(shù)學(xué)基礎(chǔ),，這在哲學(xué)上產(chǎn)生了不同的影響。對于我們來說,，這是有爭議的,，我們在這個問題上就此打住,。

下圖展示了證明助手Lean中的一個正確的證明與一個不正確的證明：

紅色錯誤信息已經(jīng)很清楚地顯示了上面的證明是錯誤的,。下面的證明,，由于沒有錯誤,，可以迅速看出是正確的,。就像魔方一樣，一個證明是否正確可以很清楚的看出來,。

這看起來有點復(fù)雜,。這是必須的嗎？可能是,。比如,，海耶斯的開普勒定理的證明由于太復(fù)雜而不能讓期刊編輯來檢查,。那個證明最終是用證明助手HOL-light來檢查的。那個形式化地驗證開普勒猜想的計劃叫做Flyspeck計劃,。Flyspeck花費了幾年數(shù)年時間與微軟Azure Cloud 五千個處理器小時才完成,。一些人期望一個不那么重度依賴于計算機的證明，以便數(shù)學(xué)家可以閱讀那個證明,。

喬治·貢蒂爾(Georges Gonthier)及其微軟研究院的同事作出了第一個經(jīng)過形式驗證的四色定理的證明,。這個不同于那個最開始的基于計算機的四色定理的證明。本質(zhì)上,，那個原始的證明是擁有非常大量的計算機計算的標(biāo)準(zhǔn)數(shù)學(xué)論證,。貢蒂爾的工作審查了這一點：支撐四色定理證明的算法，事實上,，做了我們相信它做的,。

費特-湯普森奇階定理(Feit-Thompson odd order theorem)，是有限單群分類的基石,。貢蒂爾的團隊使用證明助手Coq形式證明了它,。費特-湯普森奇階定理的原始論文有255頁。這個團隊其它被高關(guān)注度的項目還包括素數(shù)定理,、哥德爾不完全定理以及中心極限定理的形式證明。

如何起步,？

這些工具并不是只能用于那種耗費數(shù)年的大規(guī)模的證明,。也存在一些庫包含了如下學(xué)科的定理與定義：實分析、一般拓撲學(xué),、表示論與抽象代數(shù)。在工業(yè)界,，證明助手也用于驗證軟件與算法,。這是非常強大的。一旦一個人可以用數(shù)學(xué)上嚴格的方式來宣稱“這個程序P沒有缺陷(bug)”,，他就能證明這件事,。利用形式證明軟件，程序員可以確信他們的程序是沒有錯誤的,。

市面上有很多證明助手軟件供人使用,。它們都是免費的。

Isabelle-HOL是勞倫斯·保爾森(Lawrence Paulson)編寫的一個證明助手,。它基于高階邏輯,。Isabelle 擁有大量可以使用的庫以及一些強大的'自動化技術(shù)'。這里自動化技術(shù)指的是證明助手能為你自動找出一些比較短的證明,。HOL-Light是約翰·哈里森(John Harrison)所寫,、擁有更小的內(nèi)核的類似程序,。

Coq 與Lean都基于依賴類型論。開發(fā)它們的團隊分別被蒂埃里·科康(Thierry Coquand) 與 里奧·德·莫拉(Leo de Moura)所帶領(lǐng),。依賴類型論意味著數(shù)據(jù)類型可以依賴于其它數(shù)據(jù)類型——這正是我們所希望的,。例如，對于任意的k, 我們希望有這么一個類型Fin(k),，它是成員基數(shù)為k的有限集合,。這些證明助手，即使是近期發(fā)布的,，自動化能力也較弱,；由于技術(shù)原因，在依賴類型論中實現(xiàn)自動化,，是更困難的辦法（至少目前是這樣）,。

上面提到的證明助手都有在線手冊。Lean 2有一個交互式的網(wǎng)頁版教程(https://leanprover./tutorial/),。Lean的當(dāng)前版本號是3,，不過筆者發(fā)現(xiàn)閱讀這個教程是總體上品味證明助手思想的好方式。

問題與展望

對于一線數(shù)學(xué)家來說,，證明助手當(dāng)前還沒有好到可以讓他們自如的使用的地步,。海耶斯確實在他的開普勒問題的工作中使用了HOL-light，不過,，除非數(shù)學(xué)家迫不得已,，他們是不愿意做這樣類似的事情的。當(dāng)前的庫,，還沒有足夠大到包括關(guān)于日常定理的日常論證,。例如，我們本來想證明一個關(guān)于緊李群的標(biāo)準(zhǔn)結(jié)論,，發(fā)現(xiàn)哈爾定理(Haar’s theorem,，證明哈爾測度存在性的)不在我們的庫里。這個定理經(jīng)常被引用,，它的證明冗長,，而且，就當(dāng)前的技術(shù)來說,，得到我們希望的那種形式證明還需要花費數(shù)年時間,。

還有另一個更加本源的反對理由。用瑟斯頓的語言來說,，數(shù)學(xué),，最終是關(guān)于數(shù)學(xué)對象的理解，防止我們的理解走入迷途的證明僅僅是第二位的,。用偉大的組合學(xué)家羅塔(G.-C. Rota)的話說,，“說一個數(shù)學(xué)家‘證明了定理’就像是說一個作家‘寫了一串單詞’一樣”,。他的意思是，算法化的“證明搜索”那種形式的論證不是我們所想要的,。

不過,，并沒有什么證據(jù)表明，一個人理解數(shù)學(xué)對象與使用計算機證明助手是相沖突的,。機器檢驗并不是證明搜索的同義詞,。當(dāng)前，期刊有人類審查員來檢查細節(jié)的技術(shù)性的論證,。如果能夠使用計算機來檢查這些,，我們損失任何東西，反而得到了更多的可核查性,。

史蒂芬·沃爾弗拉姆(Steven Wolfram)最近對形式證明產(chǎn)生了興趣,。沃爾弗拉姆的團隊已經(jīng)在努力工作以使Mathematica與形式證明合作[1]。相關(guān)的語言學(xué)家,、計算機科學(xué)家以及數(shù)學(xué)家時常在考慮那些讓計算機代碼看起來更像日常數(shù)學(xué)的方法,。最終目標(biāo)是提高審查過程的效率。

所有的期刊都要求我們使用LaTeX來寫論文——雖然并不一直如此,。也許在未來,，一些期刊將會為了計算機檢查而要求半形式化語言的證明。那樣,，期刊編輯將把更多注意力放在清晰性以及數(shù)學(xué)文章的總體展示上面——這就是加深了人類對數(shù)學(xué)的理解,。

致謝

我對卡耐基梅隆大學(xué)的杰里米·阿維加德(Jeremy Avigad)和匹斯堡大學(xué)的湯姆·海耶斯(Tom Hales)致以最大的感激，是他們教會我我所知道的關(guān)于證明助手的知識,。 我同樣對約翰霍普金斯大學(xué)的艾米利·里爾(Emily Riehl)表示感謝,，是他讓我知道了比爾·瑟斯頓(Bill Thurston)的《論證明與數(shù)學(xué)的進展》(On Proof and Progress in Mathematics)。這篇杰出的文章,，我在本文中引用了多次,。最后，我把這個筆記獻給晚年的弗拉基米爾·沃沃斯基(Vladimir Voevodsky),。我個人從未見過他，不過,，他給我的多位老師的影響,，他的論文，他的講稿記錄,，都是我的本科教育中最重要的東西,。