(數學危機 PART 1 數學危機也跟斯斯一樣有兩種)
若干年前在寫某篇小說的構思階段，假想人類所製造的機器人在月球上建立了新的基地，獨立於人類的語言之外開發出了自己的語言系統，後來往宇宙前進的過程裡，透過彎曲時空的方式與整個(地球--登月--宇宙)計畫的緣起連絡上，接回一個時間上的迴圈。
從這個機器人系統(可能使用)的語言，衍生出接下來連續三篇發文。
這是科幻小說無誤，但其中有一部分元素卻正在發展中，關於數學這套語言的基礎。關於甚麼是數學基礎請看 WIKI Foundations of mathematics - Wikipedia
(註: 英文版比中文版要清楚多了。)
以數學去支持各種人類知識的發展自是無庸置疑。數學也粗分為幾何，數論與解析三大塊。(但到了20世紀後，各種數學領域的發展可謂是人馬雜沓，千軍萬馬)
諾貝爾物理學獎得主 Eugene Wigner 提出 The unreasonable effectiveness of Mathematics (有翻譯成不合理的有效性，我倒認為他說的是不可思議的有效性) (可參考這篇介紹: https://jupiter.math.nycu.edu.tw/~mshc/002_201406/002_03.pdf)
幾何，數論與解析這三個領域的共同特徵是使用公理化方法：定義概念 -> 設定公理 -> 透過邏輯(logical，推論)方法，演繹出定理->證明。這原本是歐基里德幾何學(幾何原本)所發展的一套推理方法，後來成為數學領域在發展時所參考的一套流程。
看這個完全沒有爭議的例子，很好理解。 運用曲全公理(一般稱為三段論)，大前提為一般性、小前提為特殊性，符合大前提的小前提是可以推出結論。
-
所有人類都會死。
-
所有希臘人都是人類。
-
因此，所有希臘人都會死。
上面是屬於邏輯學的範疇，也是許多古典數學發展的基礎。
但是既然是用語言來表達，有許多書籍都舉出了三段論似是而非，或者三段論要注意的推論方法(這很容易找到)。常見形式包括：中詞不周延（中詞沒有指代全部）、四詞謬誤（在語意上有歧義）、大/小詞(前提)不當（範圍擴大）、互斥前提（兩否定前提）等。
第一個問題出現在要怎麼寫出有不言自明的前提(無須證明，公認為真理)，也就是公理 (axiom)。(關於公理的發展與討論可以是一本書的內容，這裡我們只要知道，有不需要懷疑的前提就好)。
但這套方法是不是完全能用呢? 有沒有例外? (不能使用，或者使用時有反例出現) – 這時候就會出現"危機”。為了讓公設的方法成為一套穩固且能用的標準，才有了集合論，選擇公理，直覺構造。。。後面文章會提到。
在十九世紀之前，並沒有數學危機的說法(對於甚麼是數學基礎作深入的討論)，以致今日所看到的網路上(重複又重複的內容)所提三大數學危機是指
-
無理數的表達方式 (健全數論)
-
微積分的無窮小觀念 (以極限定義讓微積分成立)
-
樸素集合論的缺失，因羅素悖論而起。
上述三項”發明”的重要性。
一套數學運作的方式必須要是嚴謹的才能將它的發展視為正確(真)的。
那麼，用這樣的標準來看有沒有第四次數學危機?我認為依照上面的想法，數學危機怕不有幾十次改進舊的想法，或者產生新的理論、領域都可以說是危機了。 (為什麼三次而已?似乎太簡化了，不果我承認用"三"來簡化，實際上是可以讓人知道數學一直在進步，請提高學習的興趣!)
以下是一般人不太會注意到的現代三大數學危機的說法。
在另外一篇重要的文章，Ernst Snapper 在 1979年所提到的關於三大數學危機的文章。該篇文章指向數學基礎的發展在19世紀末到20世紀初所遇到問題與發展。 (The Three Crises in Mathematics: Logicism, Intuitionism and Formalism，可參考
https://www.imada.sdu.dk/u/jessica/Snapper_grundlag.pdf )。
該文章回顧了包括邏輯主義，直覺主義以及形式主義的發展與成果(依照發展的時間順序)。(先別被三個主義騙了，其實它們都是在發掘數學基礎的問題希望能夠讓數學的發展夠穩固可靠，只是都沒有完成一統天下。)
上面的內容可以寫成長長的文章，需要一點時間去消化的內容。
不涉及裡面的數學家以及詳細成果，可以簡化成
-
邏輯主義，想把數學等同於邏輯，卻引用了非邏輯的公理(無窮公理與選擇公理)，且無法解決悖論。(羅素的理髮師悖論) (另外，千萬不要把選擇公理認為是因應不同條件而”選擇性地”應用公理(有很多種公理，但選擇公理是針對集合論而產生的一個公理)，選擇公理本身是一道菜，可不是像自助餐選菜色一樣地"選擇”那種意思)
-
直覺主義，想確保數學的直覺真實性，排除邏輯中的排中律，犧牲了大部分有用的古典數學工具，尤其是反證法成為不可靠的工具。
-
形式主義，想證明數學系統的相容性，用形式符號方式推論出數學，後來哥德爾證明了含有算術系統在內就無法自證其相容性。(哥德爾不完備定理)
舉一個例子就好。數學操作可以讓一個球變成兩個球(巴拿赫-塔斯基定理（Banach–Tarski paradox)，邏輯上正確但是卻違反直覺，原來是 Banach、Tarski 想要拒絕選擇公理的使用，指出在選擇公理成立的情況下，可以將一個三維實心球分成有限（不可測的）部分，然後僅僅通過旋轉和平移到其他地方重新組合，就可以組成兩個半徑和原來相同的完整的球。完全合法(規則)，但不合理(直覺)。
那一大段在二十世紀的發展，是少數人感受到了數學的危機，怕數學世界因此崩塌，但全人類沒有，人類世界怕的是核子彈這種完完全全不講武德的發展。
回到這一段的最前面，我在寫小說時發現了甚麼---機器人發展出新的(數學語言)，到底可不可能? 深入這個想法之後才發現原來數學危機的拯救之旅還在發展中啊。
(數學危機 PART 2 數學基礎有沒有大一統的機會)
從邏輯主義者的夢想出發，他們認為
數學 = 邏輯
Snapper的文章中指出，想建構微積分、實數系統，就必須假設有無窮多個數字存在（無窮公理）。然而，”有無窮多個東西存在”這句話並不是邏輯能保證的。
這就像是你原本想證明建築學純粹是幾何學，但最後發現必須先承認磚頭是存在的。一旦承認了磚頭的存在，就從純粹的幾何（邏輯規則）跨越到了材料科學（數學實體，非邏輯公理）。於是
數學 ≠ 邏輯
那麼可以這麼問嗎? 數學是一套設計，邏輯也是一套設計，但是這兩者運用的語言規則最後發現了不相同之處。 有沒有可能有一套語言讓這兩者都對，因為它們都有所應用的範圍，而超出這兩範圍的問題，就必須用更不同的語言來描述與解決了。
這正是目前數學家和邏輯學家的發展方向。從以下幾個層次來看：
-
應用範圍: 在現代數學中被稱為範疇論 (Category Theory) 或 托波斯理論 (Topos Theory)。不再尋找一個唯一的、絕對的真理，而是承認存在不同的”數學宇宙”：
-
更高級的語言：同倫類型論 (HoTT)，這套語言試圖把邏輯、數學、與計算機程式統一起來：
-
它不把數學看作是”集合”，而是看作”類型” (Types)**。
-
它引入了”等價即相等”的觀念（Univalence Axiom）。
-
在 HoTT 的框架下，邏輯命題和數學對象被看作是同一種東西的不同側面。
-
解決超出範圍的問題就用不同語言解決，數學史上有個著名的例子：連續統假設 (Continuum Hypothesis)。哥德爾與柯恩 (Paul Cohen) 先後證明了：在我們現有的 ZFC (選擇公理) 語言中，這個問題是”獨立”的（即無法證明它是對的，也無法證明它是錯的）。
(所以人一旦有意見不合，誤解，也是可以解釋為語境不同，當然，價值觀的”錨點”也類似。)
用一個簡單的比喻來總結：
可以有一套完美的法律邏輯，但如果不先把”人人平等”這條”非邏輯的內容”寫進憲法，你的法律系統永遠推導不出關於權利的結論。(沒有磚塊怎麼築牆)
現在的趨勢不再是強迫數學縮小成邏輯（邏輯主義的失敗），也不再是強迫數學放棄美感（直覺主義的代價），而是發展出像 範疇論 這種”語言的語言” (數學也來這套後設理論啊)，讓我們可以在不同的數學系統之間進行翻譯。
不用爭論哪種語言可以表達更準確，而是開發出了一套能夠在各種語言間自由轉換的”世界語”。
(數學危機 PART 3 計算機科學與AI 的未來)
我的小說想像把機器人丟到月球後，它們發展了 Part 2 結尾說的一套新語言。
在現實的世界，這個叫做同倫類型論 (Homotopy Type Theory, 簡稱 HoTT) 基本上是將 20 世紀三個看似不相關的領域”強行”統一起來的超高級語言：
-
邏輯與證明（命題即類型）: 數學證明不寫在紙上的文字描述，而是一段可以運行的程式碼。程式碼的編譯通過，就是證明的完成。
-
電腦程式（資料類型與函數）: 專門的語言叫做 Agda 或 Coq（證明助理）
-
幾何/拓撲學（空間與路徑）: 同倫 (Homotopy) 的概念，如果兩條不同的證明（路徑）來證明同一個結論，這兩條證明是否可以”連續變形”成彼此。對數學證明的意義巨大：一旦你證明了一個關於 A 的定理，而 B 與 A 等價，那麼 B 自動繼承了這個定理，你不需要重新證明一遍。(單價公理)
這是一種不同的手術方法，在這些語言中寫程式時：
-
先定義一個類型（數學命題）。
-
撰寫函數程式碼（證明步驟）。
-
編譯器 (Compiler) 檢查邏輯：
是不是好像變得很簡單? (哈，不會那麼簡單)，為什麼這能解決數學三大危機 (Snapper所提的三大)。HoTT 提供了一種計算性基礎：
-
它像邏輯主義一樣嚴謹。
-
它像直覺主義一樣強調構造（必須寫出程式碼）。
-
它像形式主義一樣處理符號。
它不再爭論無窮是否存在，而是問”如何構造出處理無窮的程式類型”。
事實上已經有這麼三個著名的例子，
1. 四色定理 —— 第一個”程式證明”。任何地圖只需要四種顏色，就能讓相鄰區域顏色不同。
-
1976 年，阿佩爾和哈肯提出了證明，但其中包含 1,476 種特殊情況，必須由電腦掃描。當時許多數學家不承認這算證明，因為人類無法手算驗證。
-
2005 年，數學家 Georges Gonthier 使用 Coq ，將四色定理的邏輯完全寫成程式碼。讓電腦檢查邏輯推演。當 Coq 顯示編譯通過，Q.E.D (證明結束)
2. 克卜勒猜想 (Kepler Conjecture) ——關於”如何最有效地堆放球體”。
-
1998 年，Thomas Hales提交了一個包含 250 頁手稿和大量電腦程式的證明。當時負責審稿的 12 位專家花了 4 年時間，最後宣稱99% 確定它是對的，但沒體力檢查每一個細節。
-
黑爾斯為了消除質疑，發起了名為 Flyspeck 的計畫，目標是用程式語言（HOL Light 和 Isabelle）重新寫一遍證明。
-
2014 年，計畫圓滿完成。電腦程式成功導出了所有邏輯路徑，徹底解決了這場長達 16 年的爭議。
3. 液態向量空間 (Liquid Vector Spaces) —— 2020-2021年菲爾茲獎得主 Peter Scholze。
-
Peter Scholz 提出新理論（凝聚數學，將拓撲學、代數幾何與泛函分析統一起來），但他自己對其中一個核心引理的證明感到有些不安，擔心邏輯上有問題。
-
他在網路上公開發起挑戰，請求專家使用 Lean（基於 HoTT 的證明助理）來驗證。
-
以 Johan Commelin 為首的團隊以半年時間，將 Scholze 的思路翻譯成程式語言。
-
程式最終驗證通過時，Scholze 表示”這是我這輩子見過最瘋狂的事情之一，我現在終於可以確定這個理論的基石是穩固的。”
傳統數學家常說顯而易見(trivial) 、同理可得(Similarly, it follows that... / Therefore…)，但電腦不會。傳統數學家會看錯符號，產生認知偏誤，電腦不會。現代數學家的證明往往長達數百頁，在大腦中同時保持所有細節是很困難的，電腦不會。
程式證明（如 Lean, Coq, Agda）的運作邏輯是它不允許任何「顯而易見」。必須定義每一顆原子、每一條規則。如果邏輯條件缺了哪怕 0.0000001% ，程式編譯就不會通過。
好，數學與邏輯找到了程式這個第三者來擔任翻譯官。
那麼數學是不是完全要交給電腦了呢?
不會，說到數學，不會就是不會。 (哈)
但是往下的 Part 4 或是我的小說，極有可能就是交給 AI 來續寫了。 (Part 3 完結)
文章定位：
