我聽說現在提議形式化數學時，必須解釋為什麼不使用 Lean。這讓我想起四十年前離開依賴型別世界的原因：那裡的教派主義、封閉性和從眾心態。Lean 是一門優秀的語言，擁有良好的工具、大型函式庫和熱情的用戶社群，近來取得了驚人的成就。但別忘了，數學形式化的歷史已近六十年。在當今的熱潮中，我們必須記得這條路是怎麼走過來的，而不是盲目跟隨潮流。
上述熱潮的一部分是常見的說法「Lean 使數學形式化成為可能」。抱歉，我們早在1968年就達成了這點。NG de Bruijn 的 AUTOMATH 已包含大部分必要元素。到1977年，Jutting 已用它形式化了 Landau 的《分析基礎》，涵蓋從純邏輯構建複數。他處理等價類和有理數集合，正式證明了實數線的 Dedekind 完備性。儘管電腦性能大幅提升，他的成就直到二十年後才被匹敵。最後，在90年代中期，John Harrison（使用 HOL Light）和 Jacques Fleuriot（Isabelle/HOL）再次形式化了實數。
我相信，今天任何系統中已形式化的數學幾乎都能在 AUTOMATH 中完成。它的主要缺點是符號非常難用，且完全缺乏自動化，證明冗長且難讀。
然而，對於等價類的推理，它可能仍優於 Rocq。Rocq 用戶抱怨「集合地獄」，但 Jutting 在論文中冷靜描述了他的等價類形式化，甚至第二次形式化 Landau 的一章，採用等價類因為他認為這是正確方法。
另一個完全不同的領域是 Robert Boyer、J Moore 及其同事的工作。1973年他們首次提出「證明 LISP 函數定理」，目標是程式碼驗證而非數學。他們的「計算邏輯」對一般數學有限制，但仍用於形式化多個深刻結果，從哥德爾不完備定理到二次互反律再到 Banach–Tarski 定理。現今版本稱為 ACL2，主要用於硬體驗證。與眾不同也能走得遠。
開創性的愛丁堡 LCF 專注於程式語言理論，但其以函數式程式語言作為證明助理元語言（即 ML）的理念影響深遠。劍橋、INRIA、康乃爾等地的團隊用 ML 建立工具，包括早期 HOL、Coq（現 Rocq）和 Nuprl。HOL 團隊專注硬體驗證，但浮點硬體驗證需求帶來實分析需求。John Harrison 證明了嚴肅數學，如透過柯西積分公式證明素數定理。他致力於驗證著名的百大定理，HOL Light 常居榜首。Isabelle 有時超越 HOL Light，是因為我借用了許多他們的形式化成果。
到2014年，這些系統已形式化多項高階結果。這些定理多數證明冗長複雜，形式化工作是減少疑慮的關鍵，但很少數學家為之動容，例外者有集合論家 Dana Scott 和 Ken Kunen。
我對 Lean 本身了解不多，但知道它如何席捲數學界。數學家懷疑上述證明未涉及主流數學中的複雜結構，如 Grothendieck 範疇和完美域空間。Tom Hales 有意建立此類定義庫（僅定義，不含證明），選擇 Lean 作為工具。他在 Newton Institute 的 Big Proof 計畫中發表，Kevin Buzzard 聽聞後嘗試用 Lean 教學，後續發展眾所皆知。
Lean 社群一大關鍵是放棄 Rocq 長期執著的「建構性證明」。我曾討論過，直覺主義哲學源於羅素悖論後果，對實數有特殊影響。Martin-Löf 型別理論明顯是直覺主義形式，但 Rocq 就不那麼明確。許多論文提及「建構性證明」時常無關甚至荒謬，這種執著阻礙 Rocq 在數學上的應用，讓 Lean 得以崛起。
命題即型別是一種對偶關係，連結邏輯符號 $∀$, $∃$, $→$, $∧$, $∨$ 與型別構造子 $Π$, $Σ$, $→$, $×$, $+$。它美麗、迷人且理論豐富，但並非唯一方法。我見過「證明助理」被定義為依命題即型別原理檢查證明的軟體，這樣一來，過去半世紀的大部分研究都被抹去，只剩 Rocq、Lean 和 Agda（實作 Martin-Löf 型別理論）。
連 AUTOMATH 也不是命題即型別的實例。雖有 $Π$ 和 $→$，但邏輯是用類似任何邏輯教科書的公理建立。五十年前，de Bruijn 就明白型別與命題類別需分開，原因之一是除法運算需三個參數，且 $x/y$ 的值依賴於證明 $y ≠ 0$。他指出證明的無關性必須存在。
我甚至聽過有見識的人說「LCF 方法就是命題即型別」，這完全錯誤，還有整篇部落格文章澄清這種謬誤。
Rocq 和 Lean 都包含命題類型 Prop，提供證明無關性，特別是所有同一命題的證明物件都評估為相同值，因此這些龐大項目不必要，但仍保留。為什麼？
證明物件不必要是 Robin Milner 為 LCF 的關鍵發現。你只需要一門程式語言（ML！）提供抽象資料型別。將證明核心放入抽象資料型別，推理規則設於建構子，證明即動態檢查。ML 的抽象障壁使作弊不可能。
我曾有過超現實經驗，試圖向一位命題即型別領域的頂尖函數式程式專家解釋這個五十年前的想法。這位專家應該熟知 ML 的起源故事，但我花了很久仍未說服他，這正是我前述封閉性的例子。
在 RAMmageddon 時代，浪費數十兆位元組在無意義的巨大項目上簡直瘋狂。甚至有研究試圖讓這些無用項目變得優雅。
先說明明顯的：如果你的同事用 Lean，他們有 Lean 專業知識，且你的關鍵前置條件在 Lean 函式庫，當然應該用 Lean。
但如果你自由選擇，本文一大目的就是給你考慮 Isabelle 的理由。包括
依賴型別的一大難題是，若正確實作，型別檢查必須是不可判定的。因為等式不可判定，早期這是共識。然而約1990年，觀點轉變。為使型別檢查可判定，等式被降級為定義性或內涵性等式。這就是為何 $T(N+1)$ 與 $T(1+N)$ 是不同型別。雖然此限制對證明有實際影響，測試定義性等式仍是沉重計算負擔。
公平說，若你2017年問我 Isabelle 能處理什麼數學，我會更謹慎。很容易想像依賴型別是處理如
但我們一群人做了研究，學到很多。關鍵是不要強迫一切都是型別。
Lean 做對了很多事，且有潛力具可讀性，甚至支持巢狀證明區塊。現在其用戶社群必須利用這些功能，Isabelle 用戶大多已在做。最終透明度不是電腦能檢查的證明物件，而是人類能真正閱讀的證明文本。
AI 興起使這些差異更明顯。AI 證明往往混亂，但用 sledgehammer 很容易整理。因為結構良好——以我有限經驗，使用 Claude——即使細節過多也可讀。你能看出過程並尋找簡化方法。最近研究中，語言模型本身會呼叫 sledgehammer。最後，AI 可輕鬆將可讀結構化證明從一證明助理轉譯到另一個，這樣你就不用擔心選哪個了。
[非常感謝 Wenda Li 的意見！]
我竟然又忘了提 Mizar。沒有討論 Mizar 及其龐大數學函式庫，數學形式化史不完整。更糟的是，Isabelle 的 Isar 語言大量借鑒了 Mizar。我的下一篇文章保證會談 Mizar！