1976 - 四色定理計算機證明（數學第一次被機器解決）#

案件摘要#

1852 年，Francis Guthrie 在地圖上為倫敦郡畫縣界時發現：

125 年後，Kenneth Appel 與 Wolfgang Haken 在《Illinois Journal of Mathematics》 發表《四色定理的證明》（1976）——用 1,936 個配置的計算機檢查完成：

這是數學史上第一個「計算機證明的重要定理」——開啟了「機器證明」的時代。

前因 -- 為什麼會有這個案子#

• Guthrie 的觀察（1852）： Francis Guthrie（19 歲）在倫敦郡（London）畫地圖時，注意到：

他把這個問題告訴哥哥 Frederick Guthrie，Frederick 轉告 Augustus De Morgan（De Morgan 定理的提出者）。 De Morgan（1854）寫給 Hamilton 的信：這是一個「漂亮的問題」，但他無能為力。 - Hamilton（1856）的玩笑： William Rowan Hamilton（四元數的發明者）在 1856 年的演講中開玩笑說：

「四色問題可能是無解的，因為四元數只有 4 個單位！」 （四元數 \(\{1, i, j, k\}\) 的 4 個單位與 4 種顏色的巧合——這是巧合，但誤導了半個世紀。） - Tait 的還原（1880）： 1880 年，Peter Guthrie Tait（物理學家，Maxwell 的朋友）證明四色定理等價於：

這把四色問題變成了「圖論」的問題——也是 100 年後計算機驗證的切入點。 - Dehn（1900）的里程碑： Hilbert 1900 年的第五題就是「四色定理」。1901 年，Hugo Dehn證明四色定理等價於 「所有 bridgeless 的平面立方圖的邊染色可分解」—— 這是第一個嚴格地把它「化為別的問題」的證明。

線索與推理 -- 數學式、程式、理論#

第一條線索：平面圖的四色問題（形式化）#

問題：對平面圖 \(G = (V, E)\) 的所有頂點著色，使其鄰接頂點不同色：

平面圖的結構定理（Euler, 1752）：

這給了貪心著色的上界 \(6\) （ \(k\) 重著色的貪心策略）—— 但要降到 \(4\) ，需要更細的結構。

第二條線索：Kempe 鏈與「不可避免配置」#

Kempe 鏈（Kempe chain, 1879, Alfred Bray Kempe）： 對已著色的平面圖，若頂點 \(v\) 是 4 色中某兩色 \(a,b\) 的交界， 則存在一條交替使用 \(a,b\) 色的Kempe 鏈（ \(a\) - \(b\) 鏈）：

Kempe 的定理（1879）：平面圖可用 \(4\) 色著色的證明歸結為：

這個歸結是計算機驗證的突破口——只需驗證有限個配置。

第三條線索：Appel–Haken 的計算機驗證（1976）#

Appel & Haken 的關鍵步驟： 1. 不可避免配置（indispensable configuration）： 一種「紅」配置 \(C\) ，若任何 \(4\) -著色的平面圖都包含 \(C\) 的一個同構。 2. 歸結集合（reducibility）：對所有不可避免配置，

1. 計算機驗證：
2. 1,936 種「歸結配置」被計算機逐一驗證為可歸結：

• 計算時間：IBM 370 上的 1,200 小時（+ 250 小時驗證）。
• 紙本論文：僅 9 頁正文 + 1,482 頁附錄（含所有配置）。

Python：Kempe 鏈與貪心著色的驗證#

import numpy as np

# 1) 貪心著色：平面圖 ≤ 6 色一定能著（六色定理）
def greedy_color(graph, max_colors=6):
    """貪心著色：對平面圖，≤ 6 色一定能著"""
    colors = [-1]*len(graph)
    for v in range(len(graph)):
        used = {colors[u] for u in graph[v] if colors[u] != -1}
        for c in range(max_colors):
            if c not in used:
                colors[v] = c; break
    return colors

def can_color(graph, k):
    """回溯法檢查整個圖是否可 k-著色"""
    nodes = list(graph.keys())
    colors = {n: -1 for n in nodes}
    def backtrack(i):
        if i == len(nodes): return True
        n = nodes[i]
        used = {colors[m] for m in graph[n] if m in colors and colors[m]!=-1}
        for c in range(k):
            if c not in used:
                colors[n] = c
                if backtrack(i+1): return True
                colors[n] = -1
        return False
    return backtrack(0)

# K4（四面體圖）：平面圖，恰好需要 4 色
K4 = {0:[1,2,3], 1:[0,2,3], 2:[0,1,3], 3:[0,1,2]}
c = greedy_color(K4, 4)
print(f"K4 貪心著色：{c}（用掉 4 色）")
print(f"K4 可 3-著色？{can_color(K4, 3)}（不行 → 4 色是緊繃下界）")
print(f"K4 可 4-著色？{can_color(K4, 4)}（行 → K4 是四色定理的極端例子）")

# 2) 方格網（二分圖）：2 色即可著
def grid_graph(rows, cols):
    """方格網平面圖（上下左右相鄰）"""
    adj = {}
    for r in range(rows):
        for col in range(cols):
            u = r*cols + col
            adj[u] = [nr*cols + nc for nr, nc in [(r,col+1),(r,col-1),(r+1,col),(r-1,col)]
                      if 0 <= nr < rows and 0 <= nc < cols]
    return adj

g = grid_graph(4, 4)
print(f"\n4×4 方格網（{len(g)} 個節點）可 2-著色？{can_color(g, 2)}（二分圖，無奇圈）")
print(f"4×4 方格網可 3-著色？{can_color(g, 3)}")

K4 貪心著色：[0, 1, 2, 3]（用掉 4 色）
K4 可 3-著色？False（不行 → 4 色是緊繃下界）
K4 可 4-著色？True（行 → K4 是四色定理的極端例子）

4×4 方格網（16 個節點）可 2-著色？True（二分圖，無奇圈）
4×4 方格網可 3-著色？True

理論與數學式：Kempe 鏈與歸結#

四色定理的證明架構（Appel–Haken, 1976）： 1. 不可避免性：任何平面圖至少含 1,936 種「不可避免配置」之一； 2. 可約性：每個配置都可「約化」——若去掉配置後的圖可 4-著色，原圖亦可。

Kempe 鏈（1879）是「約化」的核心工具：對已 4-著色的圖，取兩色 \(a, b\) ， 其頂點導出子圖的連通塊（「a-b 鏈」）上互換兩色，著色依然合法。 Kempe 用它「證明」了四色定理（證明有洞，1890 由 Heawood 指出）， 但 Kempe 鏈本身是正確的工具——Appel–Haken 用計算機把 1,936 個配置 逐一約化（IBM 370 上 1,200 小時 + 250 小時獨立驗證）。

著色的階梯：

平面性是關鍵假設： \(K_5\) 需要 5 色但不是平面圖—— 四色定理只對平面圖成立，這正是它的微妙之處。

結案 -- 後果與影響#

• 計算機輔助證明的里程碑（1976）：

9 頁正文 + 1,482 頁附錄——這個比例說明了「計算機證明」的特點：

• 後續簡化與改良（1994–1997）：
• Robertson, Sanders, Seymour, Thomas（1997）：把 1,936 個配置降到 633 個， 且證明「不需要檢查那麼多」：

• ** Robertson 的「可歸結性定理」（1995）**：證明不需要「不可避免配置」—— 只需「不可擴展配置（indecomposable）」即可。
• 四色定理的哲學意義：
• 「什麼是數學證明」的轉變：

• T. Hales 的影響（1998 至今）：《Kepler 的推測》（Kepler's Conjecture, 1998） 是另一個例子——1998 年發表、2014 年被完全接受（含 5,000 頁的計算機驗證 + 3 位審稿人耗時 14 年）。
• 可判定性與計算機證明的邊界：
• Hilbert 第十題不可判定（1970, MRDP） vs 四色定理可驗證（1976）：

• 機器證明的前沿（2000s–）：
  • Coq / Lean / Isabelle（2000s–）：形式化證明助理—— 把證明寫成可被機器檢查的語言（Coq 驗證了費馬大定理、Ruby 等）。
  • LiquidHaskell、化學分子設計：AI 輔助證明。
  • AlphaProof（2024）：DeepMind 的 AI 輔助證明（驗證了 IMO 題目與四色相關的問題）。

• 應用（1980s–）：
• 地圖著色的實際應用：VLSI 晶片布局（平面圖著色問題）、排程問題、頻道分配。
• 演算法教學：四色定理是圖論、計算複雜度、NP 完全性的教材。
• 歷史定位：四色定理是「數學 → 計算機科學」的分水嶺——

125 年的人力，變成了 1,200 小時的機器時間—— 這是計算機對數學的第一次根本性衝擊。

關鍵人物與文獻#

• F. Guthrie：四色問題的猜想（1852）；A. De Morgan：De Morgan 定理 (1846)；致 Hamilton 的信 (1854)。
• W. R. Hamilton：開玩笑說四元數的 4 個單位對應 4 種顏色 (1856)。
• P. G. Tait：四色定理的圖論還原 (1880)；H. Dehn：Dehn 定理 (1901)。
• A. B. Kempe：Kempe 鏈方法 (1879)——「Kempe 論證」。
• K. Appel & W. Haken：Every planar map is four colorable, Illinois J. Math. 20 (1976)；1,936 個配置。
• G. Robertson, P. Sanders, P. Seymour, R. Thomas：The Four-Color Theorem（1997）——633 個配置。
• T. Hales：Kepler's Conjecture（1998）——計算機輔助證明的另一個里程碑。
• 相關案件：1900-希爾伯特第十題.md、2003-佩雷爾曼龐加萊猜想.md。