原文作者，Jacob Gross，牛津大學數學博士。
翻譯作者，風無名，哆嗒數學網翻譯組成員，[email protected]。
校對，math001。
關注微信：哆嗒數學網 每天獲得更多數學趣文
新浪微博：http://weibo.com/duodaa
“在我看來，在傳統的人類審查與計算機驗證之間的選擇，就像科學上在日晷與原子鐘之間的選擇一樣。”——湯姆·海耶斯(Tom Hales, 參見 [4])
“由於計算機與人是非常不同的，計算機的快速進展促使這點發生了戲劇性的變化。例如，阿佩爾(Appel) 與哈肯(Haken)使用了巨量的自動運算完成了四色定理的證明，引起了大量的爭論。在我看來，這些爭論幾乎不涉及到人們對定理的真實性或者證明的正確性。這反映出了，除了對‘定理是正確的’這種知識以外，人類還想要理解定理，這是一種持續的慾望。” ——比爾·瑟斯頓( Bill Thurston,參見[6])
一個機器檢驗的證明(machine-checked proof)是在叫做“證明助手”(proof assistant)的軟件中撰寫的證明。這個證明助手保證了撰寫的明證之於“數學公理”與“邏輯規則”是可以編譯的。在定理證明中使用計算機的影響是兩極化的。關於這個話題，上面的引用代表了涉及到這個主題的一些觀點。
1.到底什麼是計算機輔助證明？
2.使用計算機來證明定理有什麼長處與缺點？
3.對證明助手的學習使用有興趣的人，應該如何起步呢？
動機的問題
計算機輔助的證明是一門技術。當時使用舊技術不能解決一些問題的時候，數學家就會關心新技術。這就是我們的動機的問題：
我們來看兩個已經解決了的問題。第一個是魔方。第二個是安德魯·懷爾斯(Andrew Wiles)作出的費馬大定理的證明。
證明丟番圖方程與解魔方之間有一個很大的差別：當一個人解決了魔方的問題，他立即知道問題解決了，然而懷爾斯的證明花費了幾個月的時間來進行正式的審查。
隨著我們數學教育階段的提升。我們檢查答案的能力在下降。比如，我的啟蒙數學課是我母親教我的數數。就比較小的加法來說，我可以使用數手指的辦法來檢查我的答案。從一到十的基本數字以及用手指驗證答案都是母親教會我的。一個人學會了解代數方程，也就學會了使用變量代換來檢查答案。檢查微積分就更加的棘手了，我們尚可以對Wolfram Alpha報以比較大的信心（譯者注，Wolfram Alpha是一個數學軟件，可以做符號運算。具有計算積分的功能，還能告訴你得到答案的步驟）。至於實分析與抽象代數，學生們最終是把作業交給老師，看看教授們是否相信他們的論證，這樣來檢查他們的作業正確與否的。
什麼是證明助手?
一個計算機證明助手可以對數學論證做更加系統化的檢查。用戶使用半形式化的語言(既不像形式邏輯那麼形式化，也不像日常數學那麼非形式化)來撰寫他們的證明。證明助手基於某些數學基礎來檢查證明。正常情況下，我們想起數學基礎，我們想到的是集合論。然後由於技術的原因，證明助手是就“類型論”的基礎來實現的。在提出ZFC集合論的大致同時，羅素與懷特海提出了類型論作為另一個數學基礎。有不同的數學基礎，這在哲學上產生了不同的影響。對於我們來說，這是有爭議的，我們在這個問題上就此打住。
下圖展示了證明助手Lean中的一個正確的證明與一個不正確的證明：
紅色錯誤信息已經很清楚地顯示了上面的證明是錯誤的。下面的證明，由於沒有錯誤，可以迅速看出是正確的。就像魔方一樣，一個證明是否正確可以很清楚的看出來。
這看起來有點複雜。這是必須的嗎？可能是。比如，海耶斯的開普勒定理的證明由於太複雜而不能讓期刊編輯來檢查。那個證明最終是用證明助手HOL-light來檢查的。那個形式化地驗證開普勒猜想的計劃叫做Flyspeck計劃。Flyspeck花費了幾年數年時間與微軟Azure Cloud 五千個處理器小時才完成。一些人期望一個不那麼重度依賴於計算機的證明，以便數學家可以閱讀那個證明。
喬治·貢蒂爾(Georges Gonthier)及其微軟研究院的同事作出了第一個經過形式驗證的四色定理的證明。這個不同於那個最開始的基於計算機的四色定理的證明。本質上，那個原始的證明是擁有非常大量的計算機計算的標準數學論證。貢蒂爾的工作審查了這一點：支撐四色定理證明的算法，事實上，做了我們相信它做的。
費特-湯普森奇階定理(Feit-Thompson odd order theorem)，是有限單群分類的基石。貢蒂爾的團隊使用證明助手Coq形式證明了它。費特-湯普森奇階定理的原始論文有255頁。這個團隊其它被高關注度的項目還包括素數定理、哥德爾不完全定理以及中心極限定理的形式證明。
如何起步？
這些工具並不是只能用於那種耗費數年的大規模的證明。也存在一些庫包含了如下學科的定理與定義：實分析、一般拓撲學、表示論與抽象代數。在工業界，證明助手也用於驗證軟件與算法。這是非常強大的。一旦一個人可以用數學上嚴格的方式來宣稱“這個程序P沒有缺陷(bug)”，他就能證明這件事。利用形式證明軟件，程序員可以確信他們的程序是沒有錯誤的。
市面上有很多證明助手軟件供人使用。它們都是免費的。
Isabelle-HOL是勞倫斯·保爾森(Lawrence Paulson)編寫的一個證明助手。它基於高階邏輯。Isabelle 擁有大量可以使用的庫以及一些強大的"自動化技術"。這裡自動化技術指的是證明助手能為你自動找出一些比較短的證明。HOL-Light是約翰·哈里森(John Harrison)所寫、擁有更小的內核的類似程序。
Coq 與Lean都基於依賴類型論。開發它們的團隊分別被蒂埃裡·科康(Thierry Coquand) 與 里奧·德·莫拉(Leo de Moura)所帶領。依賴類型論意味著數據類型可以依賴於其它數據類型——這正是我們所希望的。例如，對於任意的k, 我們希望有這麼一個類型Fin(k)，它是成員基數為k的有限集合。這些證明助手，即使是近期發佈的，自動化能力也較弱；由於技術原因，在依賴類型論中實現自動化，是更困難的辦法（至少目前是這樣）。
上面提到的證明助手都有在線手冊。Lean 2有一個交互式的網頁版教程(https://leanprover.github.io/tutorial/)。Lean的當前版本號是3，不過筆者發現閱讀這個教程是總體上品味證明助手思想的好方式。
問題與展望
對於一線數學家來說，證明助手當前還沒有好到可以讓他們自如的使用的地步。海耶斯確實在他的開普勒問題的工作中使用了HOL-light，不過，除非數學家迫不得已，他們是不願意做這樣類似的事情的。當前的庫，還沒有足夠大到包括關於日常定理的日常論證。例如，我們本來想證明一個關於緊李群的標準結論，發現哈爾定理(Haar’s theorem，證明哈爾測度存在性的)不在我們的庫裡。這個定理經常被引用，它的證明冗長，而且，就當前的技術來說，得到我們希望的那種形式證明還需要花費數年時間。
還有另一個更加本源的反對理由。用瑟斯頓的語言來說，數學，最終是關於數學對象的理解，防止我們的理解走入迷途的證明僅僅是第二位的。用偉大的組合學家羅塔(G.-C. Rota)的話說，“說一個數學家‘證明了定理’就像是說一個作家‘寫了一串單詞’一樣”。他的意思是，算法化的“證明搜索”那種形式的論證不是我們所想要的。
不過，並沒有什麼證據表明，一個人理解數學對象與使用計算機證明助手是相沖突的。機器檢驗並不是證明搜索的同義詞。當前，期刊有人類審查員來檢查細節的技術性的論證。如果能夠使用計算機來檢查這些，我們損失任何東西，反而得到了更多的可核查性。
史蒂芬·沃爾弗拉姆(Steven Wolfram)最近對形式證明產生了興趣。沃爾弗拉姆的團隊已經在努力工作以使Mathematica與形式證明合作[1]。相關的語言學家、計算機科學家以及數學家時常在考慮那些讓計算機代碼看起來更像日常數學的方法。最終目標是提高審查過程的效率。
所有的期刊都要求我們使用LaTeX來寫論文——雖然並不一直如此。也許在未來，一些期刊將會為了計算機檢查而要求半形式化語言的證明。那樣，期刊編輯將把更多注意力放在清晰性以及數學文章的總體展示上面——這就是加深了人類對數學的理解。
致謝
我對卡耐基梅隆大學的傑里米·阿維加德(Jeremy Avigad)和匹斯堡大學的湯姆·海耶斯(Tom Hales)致以最大的感激，是他們教會我我所知道的關於證明助手的知識。 我同樣對約翰霍普金斯大學的艾米利·里爾(Emily Riehl)表示感謝，是他讓我知道了比爾·瑟斯頓(Bill Thurston)的《論證明與數學的進展》(On Proof and Progress in Mathematics)。這篇傑出的文章，我在本文中引用了多次。最後，我把這個筆記獻給晚年的弗拉基米爾·沃沃斯基(Vladimir Voevodsky)。我個人從未見過他，不過，他給我的多位老師的影響，他的論文，他的講稿記錄，都是我的本科教育中最重要的東西。
原參考文獻
[1] Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. Intelligent Computer Mathematics, 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings.
[2] Gonthier, G.: Formal proof—the Four Color Theorem. Notices of the AMS 55(11), 1382–1393 (2008)
[3] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Fran¸cois Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry, A machine-checked proof of the odd order theorem, Interactive Theorem Proving – 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings (Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, eds.), Lecture Notes in Computer Science, vol. 7998, Springer, 2013, pp. 163–179.
[4] Hales, T., & Hales, T. C. (2012). Dense sphere packings: a blueprint for formal proofs (Vol. 400). Cambridge University Press.
[5] Hales, T.C. Introduction to the Flyspeck project. In Thierry Coquand, Henri Lombardi, and Marie-Franc¸oise Roy, editors, Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2006. Internationales Begegnungs- und Forschungszentrum f¨ur Informatik (IBFI), Schloss Dagstuhl, Germany. http://drops.dagstuhl.de/opus/volltexte/2006/432.
[6] Thurston, W.: 1994, ‘On Proof and Progress in Mathematics’, Bulletin of the American Mathematical Society 30(2), 161–177.
關注微信：哆嗒數學網 每天獲得更多數學趣文
新浪微博：http://weibo.com/duodaa
閱讀更多 哆嗒數學網 的文章
