人類數學：形式數學宇宙中的滄海一粟

你能想像嗎？人類幾千年來發現的所有數學知識，竟然只是「所有可能數學真理」中的一粒微塵。根據最新研究（arXiv:2603.20396），這個令人震驚的事實正是理解數學本質的關鍵起點。

研究者提出一個根本性的區分：人類數學（Human Mathematics, HM）是我們發現並重視的數學，而形式數學（Formal Mathematics, FM）則是所有有效推導的總和。換言之，人類數學只是形式數學這個龐大宇宙中「極小的一部分」。

這意味著什麼？數學家的使命並非「發明」或「發現場所有真理」，而是在無垠的數學宇宙中，辨識出對人類有意義、有價值的特定區域。

從符號到意義：數學推導的運作機制

那麼，數學推導究竟是什麼？研究者的模型將數學推導描述為一串原始符號的字串操作。想像一條由「+」、「-」、「∫」、「dx」等符號組成的長鏈，這就是數學證明的基本形態。

在這個框架下：

  • 每個基本符號代表一個不可再分割的運算單位
  • 推導過程是依據邏輯規則重新排列這些符號
  • 定義和定理本質上是「命名過的子字串」或「巨集」

這就像寫程式時使用函式庫：我們不需要每次都從頭撰寫所有程式碼，而是呼叫已命名、已定義的功能區塊。數學中的「畢氏定理」或「微分基本定理」正是這樣的「巨型指令」，它們壓縮了大量的符號操作。

壓縮：人類數學的核心特徵

研究的核心論點在於：人類數學之所以「人類」，正是因為它的可壓縮性。並非所有形式數學都對人類有意義——只有那些能透過層次嵌套的定義、引理和定理來壓縮的內容，才會進入人類數學的範疇。

舉例來說，實分析中的「導數」概念看似簡單，卻壓縮了：

  • 極限的嚴格定義
  • 連續性的要求
  • 差商的極限運算
  • 一連串代數推導

沒有這些壓縮機制，我們必須在每次使用導數時重複整個推導過程——數學將變得完全無法使用。這正是人類數學與純形式系統的根本差異：我們選擇的不只是「為真」的命題，更是「對人類認知有意義」的結構。

單子理論：數學結構的抽象建模

研究者選擇單子（Monoid）作為建模工具，這是代數結構中的一種優雅抽象。簡單來說，單子是一個配備封閉運算的集合，滿足結合律並擁有單位元素。

為何單子適合描述數學推導？

在數學單子中：

  • 集合由所有可能的符號序列組成
  • 運算是「串接」——將兩個推導連在一起形成新推導
  • 單位元素是「空推導」——什麼都不做的操作

當定義和定理被視為「命名巨集」時，它們就成為了單子中的特殊元素——這些元素雖然在表面上是一個符號，但在「執行」時會展開為完整的一系列基本操作。這正是數學壓縮的代數本質。

對 AI 數學家的啟示

這項研究的實際意義在於：若要開發能真正「做數學」的 AI 系統，僅有推導能力是不夠的。AI 必須學會：

  1. 識別可壓縮的模式：從大量符號操作中發現重複結構
  2. 建構層次結構：將低層操作組織為高層概念
  3. 評估認知價值：判斷哪些數學結構對「理解」有意義

真正的數學發現不只是證明新定理，更是在混沌的形式系統中，找到那條能讓人類理解的捷徑。這或許是 AI 數學家與人類數學家最本質的共同點。