第四部：機器代勞的終極審判
如果一個數學證明需要幾百萬次的加減乘除，多到人類一輩子都看不完，那它還算是真正的「證明」嗎？
1. 召喚鋼鐵巨獸
1970 年代，伊利諾大學香檳分校的兩位數學家——肯尼斯·阿佩爾 (Kenneth Appel) 與 沃爾夫岡·哈肯 (Wolfgang Haken)，決定接下四色猜想這個燙手山芋。
當時的圖論學者已經知道，要證明四色猜想，就必須找出一個包含所有可能地圖特徵的「不可避免集 (Unavoidable Set)」，並且證明這個集合裡的每一種構型都是「可還原的（也就是可以被四色塗滿）」。
但這個集合龐大得令人絕望。阿佩爾和哈肯將範圍縮小到了 1936 種 不同的複雜圖形結構。
要用紙筆去檢查這 1936 種結構的所有上色可能性？那是幾萬頁的計算量，人類絕對不可能做到不出錯。
於是，他們把目光轉向了學校裡那台 IBM 360 超級電腦。
2. 1200 小時的暴力破解
1976 年，阿佩爾與哈肯將這 1936 種構型轉化為電腦程式。他們霸佔了學校的超級電腦，讓機器不分晝夜地進行窮舉計算。
這是一場人類智慧與機器算力的殘酷接力賽。人類負責設計演算法與排除不必要的圖形，機器則負責進行無休止的邏輯驗證。
這台 IBM 電腦總共運轉了 1200 個小時，檢查了數以百億計的著色組合。
終於，在 1976 年的某個深夜，印表機吐出了最後一張報表。所有的 1936 種構型全部通過了測試。四色猜想，這個困擾了人類 124 年的世紀詛咒，終於被證明是正確的了！
伊利諾大學為此狂歡，當地的郵局甚至在寄出的信件上蓋上了一個特製的郵戳：「四種顏色就夠了 (FOUR COLORS SUFFICE)」。
3. 數學界的哲學大地震
然而，當這份震撼的論文發表後，迎來的卻不是全體數學界的掌聲，而是猛烈的質疑與憤怒。
傳統的數學家崩潰了。
在過去兩千年裡，從歐幾里得到高斯，數學證明一直被視為人類心智最高貴、最純粹的結晶。一個好的證明應該像詩一樣優美，你可以在幾頁紙內讀完它，並且在腦海中感受到那種「啊哈！原來如此！」的真理之美。
但阿佩爾與哈肯的四色定理證明呢？ 這是一本厚達幾百頁的書，加上一大堆寫在磁帶裡的電腦日誌。沒有任何一個活著的人類，有辦法在腦海中從頭到尾驗證這 1200 小時的電腦計算是否有錯。
如果電腦的記憶體在運算中發生了一次隨機的位元翻轉 (Bit flip) 怎麼辦？如果他們的程式碼裡藏著一個隱蔽的 Bug 怎麼辦？
許多保守派數學家拒絕承認這是一個「數學證明」。他們認為這頂多算是一個「極度精確的物理實驗結果」。《紐約時報》甚至發表社論，哀嘆這標誌著「純數學黃金時代的終結」。
4. 擁抱矽基算力的新時代
儘管爭議不斷，但時間站在了電腦這一邊。
隨著計算機科學的進步，後來的科學家又用更先進的演算法與形式化驗證工具（如 Coq），重新驗證了四色定理，並將 1936 種構型精簡到了 600 多種。今天，已經沒有人再懷疑四色定理的正確性。
四色定理成為了數學史上的一道分水嶺。它是人類歷史上第一個由電腦完成的重大數學證明。
它強迫高傲的純數學家們承認一件事：人類的大腦是有極限的。有些數學真理的結構就是如此龐雜，沒有任何捷徑，沒有優美的公式，你只能依賴機器的暴力算力去將它粉碎。
點與線的謎題，就這樣無意間推開了計算機時代的大門。
下一集：圖論不再只是在地圖上塗顏色了。1956 年，一位荷蘭的電腦科學先驅在咖啡館裡構思了 20 分鐘，寫下了一個演算法。這個演算法，將成為今天全球 GPS 導航系統與網際網路路由器的絕對霸主。