2012 奇階定理大案：Gonthier 團隊用 Coq 征服 255 頁群論巨著#
報案人：有限群論。案情：一個長達 255 頁的證明，無人能完全驗證。 偵探：Georges Gonthier 率領的 MathComp 團隊。兇器：Coq ＋ SSReflect ＋ MathComp。
案發現場#
1963 年，Walter Feit 與 John Thompson 發表了群論史上最著名的長證明之一：奇階定理。
它斷言：每一個奇數階的有限群都是可解群。用符號寫出來，就是對任意有限群 \(G\) ，若 \(ord(G)\) 為奇數，則 \(G\) 可解。
這個定理是有限單群分類大計畫的開端，被稱為「巨著中的巨著」。原文刊於《Pacific Journal of Mathematics》，全文長達 255 頁，充滿局部分析、特徵標理論與複雜的計數論證。
案件的疑點在半世紀後浮現：
- 證明太長，沒有任何一個數學家敢說自己從頭到尾檢查過每一步。
- 推理鏈條跨越特徵標理論、群作用、模表示，任何一處筆誤都可能讓整棟大廈倒塌。
- 2005 年 Gonthier 才剛用 Coq 封印四色定理，群論學家不禁要問：奇階定理會不會是下一個藏有暗門的懸案？
- 紙本證明依賴大量「顯然」「易見」「留給讀者」的跳步，機器無法接受這種證詞。
於是 2006 年起，微軟劍橋研究院的 Gonthier 召集了一個跨國團隊，立下豪語：把整個 Feit-Thompson 證明搬進證明助理 Coq，一個字都不放過。
偵查過程#
線索一：為何選 Coq？為何要發明 SSReflect？#
團隊的第一個判斷是：原生 Coq 寫不動這種規模的數學。傳統的 Coq 腳本冗長、結構鬆散，面對群論這種「定義層層疊疊」的領域會直接迷路。
Gonthier 在四色定理案中已經學到教訓，於是打造了 SSReflect（Small Scale Reflection），中文可譯為「小規模反射」。
其核心思想可以用一句話概括：讓計算來代替推理。形式化地說，對於一個命題 \(P\) ，若能找到一個可判定的布林函數 \(b\) ，使得 \(P\) 與 \(b = true\) 等價，那麼證明 \(P\) 就化約為計算 \(b\) 。
團隊建立了著名的反射引理模式：
它表示命題 \(P\) 與布林值 \(b\) 互為鏡像。當 \(b\) 計算出 \(true\) 時， \(P\) 自動成立，無需冗長的邏輯推演。
舉例來說，有限群上的成員判斷 \(x \in G\) ，在紙本上是一個邏輯命題，在 SSReflect 中同時是一個可執行的布林函數 \(mem(x, G)\) 。兩者之間的橋樑是：
這樣一來，大量有限結構的推理都可以交給計算完成，證明腳本縮短了一個數量級。
線索二：MathComp 函式庫——重建整座城市#
光有方法還不夠，還需要地圖。團隊從零開始建造了 Mathematical Components（MathComp）函式庫，系統性地形式化了：
| 層次 | 內容 | 規模 |
|---|---|---|
| 代數結構 | 群、環、域、模的階層式結構 | 數千個定義 |
| 有限群論 | 子群、正規子群、商群、群作用 | 核心戰場 |
| 線性代數 | 矩陣、行列式、特徵標理論基礎 | 支撐表示論 |
| 數論與組合 | 整除性、計數引理、級數 | 彈藥庫 |
| 邏輯基礎 | SSReflect 擴展、反射引理、重寫策略 | 偵探工具箱 |
MathComp 採用「典範結構」（canonical structure）來組織代數階層，使得 \(G\) 既可以被看成集合，又可以被看成群，還可以被看成作用對象，而類型推斷會自動找到正確的視角。
線索三：決戰奇階定理的戰略#
Feit-Thompson 證明的整體結構是一個極小反例法。假設存在非可解的奇階群，取其中階最小者 \(G\) ，推導出矛盾。
團隊將其拆解為兩大戰役：
- 局部分析：研究 \(G\) 的極大子群結構，證明它們都是可解的，且具有特定的半直積形式 \(M = V \rtimes H\) ，其中 \(V\) 是初等阿貝爾群， \(H\) 是作用其上的群。
- 特徵標理論決戰：利用特徵標的正交關係與分歧理論，構造出不可能存在的特徵標值，最終得到 \(ord(G)\) 必為偶數的矛盾。
關鍵的計數引理之一是類方程：
其中 \(Z(G)\) 是中心， \(C_{G}(x_{i})\) 是代表元的中心化子。團隊必須把這種「紙上一行，形式化一百行」的論證全部補齊。
最終的形式化成果約為 15000 個定義、 170000 行 Coq 腳本，外加 4 本手寫對照書。這是當時人類史上最大的形式化證明。
結案報告#
2012 年 9 月，Gonthier 團隊宣布：奇階定理在 Coq 中得到完整驗證。Coq 核心檢查器對整個證明說了「OK」，相當於法官敲下法槌。
此案的遺產極為深遠：
- 信任的轉移：255 頁紙本證明從此有了機器背書，不再依賴任何個人的權威。
- MathComp 成為標準：它從專案附屬品變成整個 Coq 社群的通用數學函式庫，後來的形式化代數幾乎都站在它的肩膀上。
- SSReflect 方法論確立：「小規模反射」證明了計算與演繹可以混合，深刻影響了後來 Lean 的 tactic 設計。
- 通往分類定理之路：奇階定理只是有限單群分類的第一塊磚，此案證明了整條分類大定理的形式化在原則上是可行的。
用偵探小說的話說：這不是破了一樁案，而是證明了「再大的案子都能破」。
證據與工具#
證據一：反射引理的典型寫法
Lemma mem_reflect (T : finType) (x : T) (A : {set T}) :
reflect (x \in A) (x \in A).
這裡的 \(reflect\) 把成員命題和布林計算綁在一起，後續證明可以直接用 \(rewrite\) 加計算完成。
證據二：群階的定義片段
Definition order (G : {group gT}) := #|G|.
Lemma odd_order_soluble (G : {group gT}) :
odd #|G| -> solvable G.
這就是奇階定理在 MathComp 中的最終陳述：若群 \(G\) 的階 \(#|G|\) 為奇數，則 \(G\) 可解。
證據三：偵探工具箱
| 工具 | 作用 |
|---|---|
| Coq | 依賴型別證明助理，擔任最終法官 |
| SSReflect | 小規模反射語言，縮短證明、強化結構 |
| MathComp | 有限群、代數、組合的完整城市地圖 |
| CoqIDE / Proof General | 互動式審訊室，逐行盤問證明 |
延伸閱讀：Gonthier et al., "A Machine-Checked Proof of the Odd Order Theorem"（2013）；MathComp Book《Mathematical Components》；Feit-Thompson 原始論文（1963）。