從陶哲軒的十分鐘談起：AI時代下數學本質的變與不變

Wayne Peng

東吳大學數學系

陶哲軒與 Gemini DeepThink

上個月底，他在部落格寫到：他花了 10 分鐘透過 Gemini DeepThink 解決了 Erdős Problem 367。
他認為：透過 AI 協助來解決 Erdős 問題，已經是這項數學工作的日常。

原始貼文

Part I
AlphaProof：AI 如何通過「證明地獄」

那麼用什麼來檢查？

答案是 Lean：一種形式化語言 / 定理證明器。

lean-lang.org

AlphaProof 的工作流程

  • 大量數學文本 → 翻譯成 Lean（使用類 AlphaZero 的 AI）
  • 用這些 Lean 文本訓練 ＡlphaProof → 生成證明
  • 用 Lean 驗證證明是否通過
  • 如果有一個題目很難解的時候怎麼辦？

Part II
什麼是公理化系統？

Part III
實數完備性與微積分的危機

微積分發展史：人物與關鍵事件

%%{init: { 
  'theme': 'light', 
  'themeVariables': { 'darkMode': false },
  'gantt': { 
     'barHeight': 40,
     'fontSize': 20, 
     'sectionFontSize': 24,
     'padding': 15,
     'topMargin': 10
  }
}}%%
gantt
    dateFormat  YYYY
    axisFormat  %Y

    section 1. 創立與早期批評
    I. Newton (1643-1727)      :done, 1643, 1727
    G. Leibniz (1646-1716)     :done, 1646, 1716
    B. Nieuwentijt (1654-1718) :done, 1654, 1718
    Bishop Berkeley (1684-1753):crit, 1684, 1753

    section 2. 分析的嚴格化
    A. Cauchy (1789-1851)      :crit, 1789, 1851
    K. Weierstrass (1815-1897) :crit, 1815, 1897
    B. Riemann (1826-1866)     :done, 1826, 1866

    section 3. 無窮小的現代復興
    A. Robinson (1918-1974)    :active, 1918, 1974
    E. Nelson (1932-2014)      :active, 1932, 2014

    section 關鍵事件
    發現連續不可微函數 (1817)    :crit, 1817, 1y
    epsilon-delta 語言 (1857)  :crit, 1857, 1y
    再次確認連續不可微函數 (1861) :crit, 1861, 1y
    Frage's 嘗試公理化集合論（1884）:crit, 1884, 1y
    線性代數公理化（1888）      :crit, 1888, 1y
    羅素悖論 （1901）           :crit, 1901, 1y
    希爾伯特問題與哥德爾不完備性（1931）:crit, 1931, 1y
    無窮小公理可能性 (1960)     :crit, 1960, 1y
    提出無窮小公理系統 (1977)   :crit, 1977, 1y