為什麼機器驗證的形式化證明沒有被數學界廣泛採用？

一方面，是不是這樣的系統，它還太過複雜，寫出來的東西太過羅嗦，不具有使用價值？比如：僅用Coq等定理證明器，學習諸如實分析之類的數學課程是否現實？。它又為什麼會太過複雜呢（相比人類結果的「簡潔」）？換句話說，人類的「簡潔」中到底隱藏了什麼細節？這些細節都可靠嗎？一個結果，只要它通過了同行的審核，就可以被認為是正確的嗎？

另一方面，這樣的形式化證明，它的表達力夠不夠呢？它能不能表達人類所能理解的所有數學內容？

還有就是，數學界能否接受這種東西呢？將來應不應該投稿必須要是經過形式化驗證的？還是說天馬行空的「想法」「創意」更重要，即使實際上是有 gap 的？但是將來能不能藉助機器學習，就像化解（如）圍棋（等人類認為有靈性的東西）中的直覺、找到優良的策略一樣，來有效地做數學呢？比如如何評價DeepMath?

據說 Voevodsky 就是因為自己犯了巨大的錯誤才轉向研究形式化的？（同時參考【推薦】一份 Voevodsky 的幻燈片）

相關問題：

如何評價Vladimir Voevodsky？

形式證明與普通數學證明的區別是什麼，為什麼說費馬定理是沒有形式證明的？

形式化證明沒有被廣泛採用的原因有很多，但主要原因正如問題里提到的，一是複雜性，二是表達力。這個回答主要針對主流的，邏輯框架是類型論的定理證明器。

複雜性：

機器證明之所以誕生，是由於數學家有使證明 error-free 的需求。要在一個互動式定理證明器里形式化一個定理，用戶會被要求填補上所有的技術細節，小到哪怕是一個MP規則。這就使得數學家感到在定理證明器中寫證明非常繁瑣。為了令機器自動填補平凡的細節，就需要寫 tactics 來完成自動化。所謂「寫 tactics」，有兩種意思，一是指數學家使用 tactics 來構造證明，一些 tactics 常自帶 unification 這樣簡單的自動化，這就免去了手動構造 proof terms 時需要補完所有細節的麻煩。二是指用戶可以寫自己的 tactics，這使得數學家可以根據自己的需求來添加自動化。

tactics 固然好，麻煩也有很多。第一種意義的使用 tactics，雖然減輕了使用者的負擔，但會相應降低證明的可讀性。這一方面是因為 tactics 通常是自結論開始反嚮應用定理，另一方面是因為有些tactics 會引入比較底層的定理。我們知道主流的定理證明器是基於類型論的，這樣的系統里底層的定理通常是 type-theoretic 的。如果 type-theoretic 的定理被引入，比如像調用 recursor 的定理，就會使展開後的 proof terms 非常不好看，非常地不（常規意義上的）數學。數學家讀寫證明的目的之一是理解證明並從中提煉有用的想法；使用 tactics 寫的證明相對難以理解，數學家自然就喪失了不少興趣。第二種意義的使用 tactics 則加深了閱讀困難，因為 tactics 本質是一段指引證明搜索的程序，大量的自定義 tactics 使得讀證明變成讀代碼。更重要的是，因為 tactics 是一段代碼，它本身的正確性是沒有邏輯框架保證的，如果學過遞歸論，會知道不存在 tactics 驗證程序，這使得讀 tactics 比讀錯誤的證明更容易浪費時間。

因此機器證明的複雜性是個兩難的問題，如果減輕了使用者的負擔，那麼讀者的負擔就會加重，反之亦然。而這還是在假定用戶和讀者都熟悉類型論的情況下。要用好主流的定理證明器，熟悉類型論是必不可少的，而要精通類型論，對 lambda 演算和證明論就不得不有一定的了解，要學好證明論，又需要有紮實的數理邏輯功底，這些 prerequisites 都不是一兩年內能積累起來的，所以形式化證明是有一定的學習成本的。

表達力：

表達力相對於複雜性的影響沒有那麼大。如果暫時不考慮「人類所能理解的所有數學內容」的精確定義，通常認為 CIC 是足以形式化數學家所要解決的問題的。但是 CIC 也有問題，它作為形式化全部數學的系統，不像 ZFC 那麼簡潔，「類型「也不具備「集合」那樣的直觀。要在類型論里定義一個數學對象，由於不能採用 ZFC 的公理和通常數學教材里的集合論定義，用戶必須知道如何用類型論的語言來描述直觀。

比如對於有窮樹，集合論里可以定義一棵有窮樹為一個圖 ，擁有一個節點 使得對任意 存在唯一的 中的 -路徑。而一個圖 則由一個有限集 和 上的一個子集 組成。如果 ，那麼一條 -路徑是一個節點的有限序列 使得 並且對任意 有 。而在類型論里，要直接描述這個定義就相當繁瑣，首先是類型論中簡單定義的集合性質不同於集合論中的集合（比如你無法說出傳遞集）。其次，在集合上取卡式積，就其定義和應用而言都遠沒有在類型上定義的卡式積方便，這是因為在類型上定義的函數一旦被限制在集合上，會要求額外的定理來描述函數的性質。所以用戶需要原生地在類型論中定義有窮樹，這通常需要利用 inductive types 來完成：

其中 。實際實現中，由於 時會造成沒有歸納基礎，你可能需要引入一個單獨的構造子 ，或者用一些類型論技巧，比如利用定義 來獲得簡潔優雅的良定義。

在表達力方面，通常不是系統本身有所限制，而是用戶對類型論了解的多少限制了使用定理證明器的深度。

其實就複雜性和表達力兩點總結而言，就是對使用形式化證明技術的數學家的類型論和邏輯要求非常高。不了解類型論，就難以找到合適地表達定理的方法，也難以優雅地構造 proof terms。如果要以 tactics 方式自定義 domain-specific 的自動化，那麼又會在類型論的基礎上加上對證明論和模型論的了解。你首先需要知道你想處理的目標理論是什麼，比如是帶有等詞的完全一階邏輯，還是無量詞的 equational logic，還是它的 universal 片段？對每一個目標理論，你需要考慮：這個理論是可判定的嗎？它有有窮模型性質嗎？它接受量詞消去嗎？它接受 cut elimination 進而獲得子公式性質嗎？如果是可判定的，它的完備且高效的判定過程是什麼？如果這個理論是半可判定的，那麼應該怎樣設計 heuristic ？要回答這些問題，用戶就需要對遞歸論，模型論，和傳統的判定過程有一定了解。這就是為什麼說，數理邏輯中最能夠被計算機科學應用的是（結構）證明論，（初等）模型論和（在 上的經典）遞歸論。

回到問題，將來有沒有可能藉助機器學習來做定理證明呢？當然是可能的，但是至今都沒有突破性的方法，Alan Bundy 的圈子裡的人嘗試了 premise selection，雖然有一定效果，但是對於關鍵的構造 proof terms 並沒有涉及。我們想知道的是，比如，機器學習有能力在讀了數百萬個證明後準確實例化某個引理中的存在量詞嗎？數學家又是如何洞察到一個特殊而複雜的數學對象滿足引理中描述的某個性質的？

想起來答辯時老闆問我的最後一個問題是，你覺得十年內，你做的這個定理的形式化，能被完全自動化嗎，或者說機器能做到什麼程度？我跟他說我完全看不到任何希望，我不知道什麼演算法能讓機器具備數學家的直觀。其實這倒不是我說的，是兩年前我問老闆時他自己跟我說的，他當時的說法是，他有生之年恐怕都看不到希望，雖然說得很委婉。

但是如果哪天機器真的完全實現了自動推理，那恐怕我們離強AI也就不遠了。

目前而言，形式化證明的確沒有廣泛的被數學屆採用。主要原因包括：

• 自動化程度。能夠用來形式化數學的定理證明器通常基於有相當表達力的邏輯（如HOL和CIC等），而在這類邏輯上的全自動推理還是相當困難的，與之相對的是弱表達力但是強自動化的邏輯如一階邏輯甚至布爾邏輯。不可避免的，在高表達力的邏輯下進行證明需要相當的人工引導，所以這類證明系統被稱之為互動式定理證明器(interactive theorem prover)。如何提高自動化（減少人工）一直是該領域的研究方向之一，而（提高）自動化的方法主要基於兩類：a) 在不影響正確(soundness)的前提下，把一部分高表達力的邏輯下的問題轉化到高自動化的邏輯中，並用成熟的自動定理證明器(如Z3,CVC4,Vampire,E,Spass等)來求解；b) 針對特定種類問題實現特定的策略(tactic), 比如當我們在定理證明中里遇到這樣的一階實數類問題 該如何解決？(目前的主流證明器中方法是sums-of-suquares，有興趣的同學可以自行搜索)。儘管在過去三十年定理證明器中的自動化程度已經有了長足的提升，我們還是希望可以進一步的減少形式化證明的成本。目前而言，在已有前置定理的情況下，在Isabelle證明器中形式化分析類的證明平均一頁需要一到兩周。
• 數學定理的證明是有先後的，比如我們只能在形式化了Cauchy』s Integral Theorem之後才能開始Cauchy』s Residue Theorem以及Prime Number Theorem的證明。考慮到目前已被形式化的結果離前沿數學還有相當的距離，在這個方面我們還需要等待形式化的結果在各主流定理證明器中的積累。當然我們也可以直接假設一些重要的結果，不過這樣會極大地損害我們對當前證明結果正確性的信心，畢竟我們是希望每一條證明出來的定理都能基於定理證明器核(kernel)中假設的顯而易見的公理。
• 用戶習慣。一定年紀的傳統數學家還是比較難以接受在定理證明器中形式化自己的證明。所幸，不少新一代的數學／計算機學家對形式化證明已有一定的了解，包括CMU,Cambridge在內的大學都開設了相關的課程。一個做類型理論(type theory)的大佬曾經開玩笑說：「我們無法教授現在的數學家們形式證明，我們只要等待這一代數學家死掉了就好」(We can』t teach them (mathematicians) proof assistants. We just need to wait for them to die out.)。
• 交互界面，證明管理。形式化證明和碼代碼(C++,Java)沒有本質上的區別，這裡面都要涉及命名、重構、函數（定理）搜索等問題。對於寫代碼我們有包括Visual Studio等的大型集成開發環境(IDE),相比之下基於Emacs(Coq, HOL, PVS) 和jEdit(Isabelle)的定理證明開發環境還略顯不足。
• 各主流的證明器採用不同的底層邏輯與基礎定義。證明器有著不同的底層邏輯，包括基於集合論的Mizar (untyped set theory)和Isabelle/HOL(simply-typed set theory)，與基於類型論的Coq。 除以0的問題：Isabelle中定義x/0=0,Coq里通過依賴類型(dependent type)的方式要求用戶排除這種情況。不同的證明範式給統一的數學形式化也造成了一定的困難。

儘管如此，形式化證明精確(no ambiguity)，高可信度(almost no 「obviously」 / gaps / bugs)且在一些時候相對可讀(legible)的特點已經在數學界引起了不少人的注意。

比如，以下是一個在Isabelle定理證明器中,關於質數的平方根不是有理數的證明：

在Isabelle定理證明器的支持下，計算機能理解以上的證明並且能檢查每一步推理的正確性（基於所假設的公理）。另外，這樣的機械化證明也具有了一定的可讀性(human readable)：完全不懂形式化證明的同學，也可以在不運行證明器的情況下對以上證明的思路有大致的概念。

另外一個例子。在Isabelle/HOL中，我們已經有了對Jordan Curve Theorem的形式化,其命題表述如下(當然證明就不在這裡展開了)：

形式化證明的精確性體現在命題中各個函數都是被準確地機械化定義的，從而命題本身也不會有模凌兩可的情況。比如其中的「有界」(bounded)定義如下：

而「邊界」(frontier)有著如此定義：

另外，有興趣的同學也可以看看前段時間在劍橋的Big Proof研討會：

Isaac Newton Institute for Mathematical Sciences

不少大佬都在會上發表了自己對數學形式化的看法。其中一個比較有意思的設想是在大規模形式化還不現實的當下，鼓勵大家在寫數學文章的時候提交一個形式化的摘要（不需要證明，僅僅是對所解決問題的形式化表述）。

綜合來說，形式化證明在數學上還處於啟蒙階段，但相信這樣嚴格、精確、高可信的證明方式在以後會有著更大的影響力也能被更多的數學家所接受。

在此緬懷Michael J. C. Gordon, FRS 和 Vladimir Voevodsky。

現代數學, 比如代數幾何, 一個 "Obviously," 寫成formal proof估計得幾千行. 然而現在代數幾何 的paper動輒幾百頁, 已經嚴重超長了. 如果都用formal proof, 數學家一輩子估計就只能寫一條證明了.

Formal methods 已經被證明是條人工智慧的死路,走不通了. 說啥都沒用.

他們都不是真正的數學家

——羅素

謝邀。本人不是數學專業的，所以一下的言論只是IMHO。

所謂證明，是公元前600年希臘先賢泰勒斯提出的，其定義就是藉助於一些公理或真實性的命題來論證其他命題的真實性。

注意這裡的公理是沒辦法用數學來證偽的，只能通過實證來證明其真偽。

就如同你看到所有的天鵝都是白的，就定義天鵝的顏色一定是白的一樣。直到有一天，有人發現了一隻「黑天鵝」！

同樣幾何學有歐式幾何，也有非歐式幾何。

公理不分對錯，只分應用的場景。如何判斷？人腦來做！

目前的機器學習/人工智慧說到底只是編程的一種實現。

而編程的定義：為了使計算機能夠理解人的意圖，人類就必須將需解決的問題的思路、方法和手段通過計算機能夠理解的形式告訴計算機，使得計算機能夠根據人的指令一步一步去工作，完成某種特定的任務。這種人和計算體系之間交流的過程就是編程。

就目前而言，機器學習的短板是只能模擬/近似來計算一些定義好的問題，這些問題的定義是人類代辦的。

對於原創性的（或者說諸如題主所說的天馬行空的「想法」「創意」），目前的「弱人工智慧」還沒能達到。（竊以為遷移學習就是為了「近似」的來應對這種情況的，至於效果好不好，看人類啦，別甩鍋給AI。）

Galois said:「Jump above calculations, group the operations, classify them according to their complexities rather than their appearance; this, I believe, is the mission of future mathematicians; this is the road I"m embarking in this work.」

how to use AI to improve?