最近兩三年數學界與人工智能社區的交叉比以往任何時候都要密集Lean 證明助手被用來推進頂尖分析學結論的形式化驗證深度強化學習模型在幾何問題上給出了人類選手級別的解答“自動形式化”這一概念也開始從論文走進工程實踐。本文想從技術角度聊一個更大的話題當 AI 真正參與數學的發現、證明與傳播時延續了幾百年的“英雄時代”是否正在落幕數學家的工作方式又會從“個體天才驅動”走向怎樣的新范式1. 背景數學的“英雄時代”是什么1.1 數學史中長期存在的“天才敘事”翻開數學史我們會看到大量以“天才個體”為核心的故事歐拉憑一己之力建立分析學的基礎伽羅瓦在決斗前夜寫下群論思想黎曼用一篇短短的論文改變了整個幾何學方向拉馬努金一邊靠直覺寫下公式一邊等待后人驗證格羅滕迪克幾乎憑個人努力重構了代數幾何的框架。這種“英雄時代”并不僅僅是一種敘事風格它背后有一套完整的研究方法論某個數學問題被英雄式的人物提出又由同一個人憑直覺找到解法最后由小圈子的同行在論文和學術通信中完成驗證。整個過程高度依賴單個大腦的工作記憶、短期注意力和靈感爆發數學也因此被看作最需要“天才”的學科。從技術角度來看這樣的研究方式并非人類天生就適合而是受限于紙質傳播和人工推導的客觀條件在必須靠紙筆驗證的時代個體洞察確實是最高效的生產力來源。但代價也很明顯證明過程難復現、錯誤難以發現、知識高度中心化。1.2 為什么說“英雄時代”正在結束進入 20 世紀后半葉數學研究對象越來越復雜單個證明動輒上百頁。最典型的例子是有限單群分類定理它的證明分散在數百篇論文中總篇幅超過一萬頁至今仍有數學家認為“完整驗證”本身就是一個難以完成的工程。計算機的出現改變了這一切。四色定理在 1976 年首次通過計算機輔助證明隨后 Kepler 猜想也在 1998 年被機器輔助驗證。這類工作標志著一個轉折數學證明的正確性不再由某個天才大腦完全把控而是轉移給了“可枚舉的計算過程”。當 Lean、Coq、Isabelle 等交互式證明助手進入主流視野后數學驗證的顆粒度又進一步下降每個符號、每條推理規則都能由機器檢查。近年 AI 技術的沖擊則更直接。符號計算系統讓代數變形變成自動化的查表操作深度學習模型能在大量數學數據中搜索模式強化學習模型在平面幾何、數論實驗等任務上開始做出接近人類選手的判斷。數學家已經不能忽視一個事實機器不僅在“幫我們算”還在“替我們想”。1.3 何謂“世界心智”“World-Mind”并不是科幻意義上的單體超級智能而是一種去中心化的認知網絡人類研究者負責提出方向、構造抽象概念機器負責大規模搜索、符號演算、形式化驗證群體則通過開源社區、形式化證明庫和可復現代碼共同維護知識的正確性。在這種新范式下數學的發現不再是一個大腦在封閉空間里的頓悟而是多個大腦與多臺機器組成的協作系統共同完成的過程。單個數學家仍然重要但其重要性的來源不再是“一個人能戰勝所有支線”而是“這個人能提出值得機器去驗證的問題”。2. 當 AI 走進數學主要技術路線2.1 定理證明器從 Coq 到 Lean定理證明器是“英雄時代”終結最直接的工程標志。它把數學證明變成一種可執行的程序我們寫出定理聲明然后用一系列推理規則構造證明項最后交給內核檢查。檢查過程是機械的、確定的不存在“我認為這個引理顯然成立”的模糊空間。Lean 是目前社區熱度較高的一套證明助手。它的一大特點是數學庫 Mathlib 組織得非常好覆蓋了大量基礎數學內容。一個廣為人知的標志性事件是 Liquid Tensor ExperimentPeter Scholze 提出了一個分析學中的關鍵猜想Lean 社區通過形式化工作把它翻譯成機器可驗證的證明進而幫助數學家確認了其中一些此前懸而未決的技術細節。從工程視角看定理證明器的價值不是取代數學家的思考而是把“審稿人靠直覺判斷”轉變成“機器靠規則判斷”。一個證明只要通過內核檢查它就不再需要被同行反復閱讀每一個符號因為它已經被壓縮成了一段可復現、可審計的代碼。2.2 自動形式化把論文變成代碼自動形式化Autoformalization是連接自然語言數學與定理證明器的橋梁。數學家習慣用自然語言寫“我們考慮一個連續函數 f”而定理證明器要求我們精確地表達“f 的類型是什么、定義域是什么、連續性是在哪個拓撲意義上定義的”。這個轉換通常非常繁瑣也是很多人剛接觸證明助手時最大的挫敗來源。近幾年大語言模型開始被用于輔助這一過程模型閱讀一段論文陳述嘗試生成對應的 Lean 或 Coq 代碼再由證明器判斷代碼是否正確。這種“生成-驗證”循環對幻覺有天然約束因為即使模型胡編了一個定理證明器也會立刻報錯。需要注意的是自動形式化目前遠未成熟。對于復數乘法、測度論積分這類高度重構的數學對象自然語言到形式語言的翻譯仍然需要人工介入。它的工程意義在于降低了新用戶的上手門檻讓數學家可以更多聚焦在問題本身而不是證明系統語法。2.3 符號計算與猜想發現符號計算系統是 AI 數學研究中常常被低估的一環。SymPy、SageMath、Mathematica 擅長處理多項式展開、因式分解、微分、積分、方程求解等操作。嚴格來說它們不是“思考”但在實驗數學中它們是發現猜想的發動機。典型的做法是當一個數學家懷疑某個恒等式成立時先用符號計算生成大量特殊取值快速驗證前一百項、前一千項再決定是否值得投入時間做證明。這種“機器實驗 人類證明”的組合已經持續了幾十年AI 的作用在于把原來依賴手工的試錯變成自動化的統計搜索并能覆蓋更高維、更復雜的對象。2.4 強化學習與搜索AlphaProof 思路的啟示AlphaProof、AlphaGeometry 這類系統采用的方法是把數學問題視為一個搜索問題通過強化學習不斷生成證明步驟再用符號引擎或證明助手判斷每一步是否合法。這種思路和證明助手的“校驗”角色天然互補校驗器負責判定對錯搜索器負責尋找路徑。在奧數幾何題這種規則空間相對封閉的任務上這種組合已經能接近人類選手水平。背后的工程實現并不神秘一個策略網絡負責生成候選步驟一個價值網絡負責評估“大概率有前途”的搜索分支再利用蒙特卡洛樹搜索進行探索。數學里的“靈感”在這里被建模為對搜索空間的有效裁剪。2.5 大語言模型在數學中的位置大語言模型在數學任務上的表現常被誤解。它可以流暢地寫出數學證明草稿甚至能在很多標準化任務上給出正確答案但它并不具備對“正確性”的絕對判斷能力。模型內部沒有形式系統它的輸出本質是“最接近訓練數據中常見模式”的文本序列。因此大模型的最佳定位不是“最終裁判”而是“第一輪過濾器”它能把一個模糊的研究問題整理成清晰的分支結構能幫助快速生成證明草案也能把自然語言陳述翻譯成形式化框架。但任何關鍵結論都必須交給證明器或嚴格的人工驗證。3. 從“猜想”到“證明”AI 時代的證明流水線3.1 傳統數學研究的閉環傳統數學研究通常是這樣運作的研究者憑直覺或實驗觀察提出猜想然后花費數月甚至數年尋找嚴格證明最后寫成論文并投稿到期刊。論文發表后由兩到三名審稿人閱讀給出“認為正確”或“認為有問題”的結論。這個閉環最大的弱點是“驗證”環節的不可靠性。審稿人也是人也會疲勞、誤讀、遺漏細節更重要的是當證明過長時沒有人能真正逐字驗證。數學史上出現過多次“發表多年后才發現證明有漏洞”的案例。這個問題的根源并不是審稿人不夠負責而是驗證工具太原始。3.2 AI 介入后的新閉環AI 時代的新閉環把驗證環節徹底工具化。一條典型的流水線包括用符號計算或機器學習實驗生成猜想用大語言模型輔助將猜想轉化為形式化聲明用證明助手、強化學習搜索或人工交互構造證明用驗證器自動檢查證明是否正確將證明與代碼打包發布讓全球社區共同維護。這個閉環中最核心的變化是“可復現性”從模糊的“我按你的思路重算了一遍”變成了“我用同一套證明腳本跑通了機器檢查”。一個定理是否成立不再取決于它是否被某個權威認可而是取決于它能否在公開可執行的環境中通過驗證。3.3 人機協作的三種典型模式在現階段人機協作大致有三種模式。第一種是“人在環路中”AI 給出證明建議數學家判斷方向是否合理再手動細化。第二種是“機器在環路中”數學家定義搜索空間和判定規則機器負責枚舉大量分支自動化程度更高。第三種是“群體驗證”多個獨立的證明系統、多個研究團隊同時對一個問題發起驗證最終給出交叉確認。選擇哪種模式取決于問題特征。競賽幾何、組合恒等式這類封閉問題適合機器主導搜索抽象代數、代數幾何這類高度依賴概念重構的問題則更適合“人在環路中”模式。理解這三種模式就不必擔心“AI 完全取代數學家”這類過于夸張的想象。4. 動手實踐搭建一個最小的“AI 數學助手”4.1 環境準備下面通過一個小例子展示“AI 數學助手”的最小實現。我們不依賴某個具體云平臺重點演示三個組件符號計算、形式化驗證、大模型輔助推理。版本需要根據你的項目實際情況調整本文示例以常見環境為例重點演示配置思路。推薦環境如下Python 3.10 及以上用于運行 SymPy 和調用大模型 APILean 4 編輯器可選擇 VS Code 配合 Lean 擴展一個大模型推理服務可以是 OpenAI 兼容接口也可以是本地部署的模型服務。安裝 Python 依賴pip install sympy openai python-dotenv如果你使用本地推理服務只需把base_url指向本地地址即可不需要修改核心邏輯。4.2 用 Python 做符號計算先來看一個最簡單的符號計算示例展開與因式分解。# 文件路徑math_assistant/symbolic_check.py from sympy import symbols, expand, factor x, y symbols(x y) expr (x y)**2 print(展開結果:, expand(expr)) print(因式分解結果:, factor(expand(expr))) # 恒等式檢查左邊是否恒等于右邊 lhs (x y)**2 rhs x**2 2*x*y y**2 print(恒等式是否成立:, lhs.equals(rhs))運行之后會輸出展開結果: x**2 2*x*y y**2 因式分解結果: (x y)**2 恒等式是否成立: True在這個例子中equals方法內部會對兩個表達式做代數運算并判斷差是否恒為 0。它適合處理多項式、分式等場景用來快速驗證猜想或排除明顯錯誤的恒等式非常方便。4.3 用 Lean 寫第一個形式化證明符號計算能發現“看起來成立”但不能代替嚴格證明。下面用 Lean 4 寫出一個最小形式化證明。theorem two_plus_two : 2 2 4 : by rfl這個定理的意思是“證明 2 2 4”。rfl是“reflexivity”的縮寫表示等式兩邊在定義上是相同的在 Naturals 的定義中2 是 1 的后繼4 是 3 的后繼計算 2 2 會得到 4因此反射性可以直接閉合證明。把這段代碼保存為Examples.lean在 Lean 擴展環境中打開代碼左側會出現“No goals”或編譯通過的提示。這是核心片段更復雜的證明需要引入 Mathlib 庫且不同版本的語法會有差異。我剛接觸 Lean 時容易產生一個誤解既然rfl能證明 2 2 4那它是否也能證明所有簡單算術答案是否定的。rfl只能處理定義相等的命題對于需要交換律、結合律的等式我們必須顯式調用庫里的定理或者使用omega、ring、linarith這類決策過程。import Mathlib.Data.Real.Basic -- 需要交換律才能證明a b b a example (a b : ?) : a b b a : by ring在這個例子中ring能夠自動處理實數域上的交換律和分配律。但前提是導入 Mathlib并且 Lean 環境能夠訪問對應版本的數學庫。如果你運行時報出unknown identifier ring多半是缺少導入或庫版本不匹配。4.4 讓大模型扮演“數學助手”大模型可以扮演證明思路的“討論伙伴”。下面是一個調用 OpenAI 兼容接口的 Python 示例它向模型提出一個數學問題讓模型先檢查斷言是否成立再列出證明骨架。# 文件路徑math_assistant/llm_assistant.py import os from openai import OpenAI # 使用環境變量保存密鑰本地服務可改成對應 base_url 與 model client OpenAI( api_keyos.environ.get(OPENAI_API_KEY, sk-local), base_urlos.environ.get(OPENAI_BASE_URL, https://api.openai.com/v1), ) prompt 你是一位數學助手。請根據以下要求回答 1. 先判斷斷言是否成立 2. 若成立寫出證明骨架 3. 指出證明中可能存在的關鍵缺口。 斷言對任意正整數 n有 1^3 2^3 ... n^3 (n(n1)/2)^2。 resp client.chat.completions.create( modelos.environ.get(MODEL_NAME, gpt-4o-mini), messages[{role: user, content: prompt}], temperature0.2, ) print(resp.choices[0].message.content)這里的關鍵設計是“先判斷再給骨架再找缺口”。如果你只是簡單提問“請證明這個等式”模型通常會直接生成一段漂亮但未必嚴謹的歸納證明。但當你要求它“指出關鍵缺口”時輸出會更有鑒別價值。需要注意的是這段代碼運行前請確認目標服務可用并且api_key、base_url、model_name都要按你的實際環境調整。不要把密鑰硬編碼到代碼倉庫里建議統一使用環境變量。4.5 運行與驗證整體流程可以分為三步第一步用 SymPy 快速檢查恒等式在小規模樣本上是否成立第二步讓大模型給出證明思路并指出風險點第三步把最終證明翻譯成 Lean 代碼交給驗證器。為了讓“驗證”更可靠可以增加一個簡單的窮舉檢查腳本對大模型給出的結論做數字采樣驗證# 文件路徑math_assistant/sample_check.py def cube_sum(n: int) - int: return sum(i**3 for i in range(1, n 1)) def closed_form(n: int) - int: return (n * (n 1) // 2) ** 2 for n in range(1, 200): assert cube_sum(n) closed_form(n), ffailed at {n} print(前 199 個正整數均滿足恒等式可以作為啟發式驗證。)必須說明窮舉檢查不是數學證明。它只能用來排除錯誤不能用來證明無窮多個情況。這就是后續需要 Lean 這類驗證器的原因——機器不會因為“看起來都成立”就放行。5. 常見問題與排查思路5.1 形式化證明常見報錯問題現象常見原因解決思路unknown identifier ring未導入 Mathlib 或運行環境缺少數學庫增加 import或檢查 Lean 與 Mathlib 版本type mismatch表達式類型不符合預期檢查變量類型、聲明定義逐步用#check查看類型goals accomplished但顯示紅色警告使用了不安全的 axiom 或sorry刪除sorry補全證明Lean 無法編譯環境版本太舊或緩存損壞升級到匹配版本清理緩存解決這些報錯最有效的方式不是盯著錯誤提示猜而是從最小的例子開始增量構造。先證明rfl能處理的最小等式再逐步引入需要交換律的公式最后再上難度。5.2 大模型給出的數學證明包含幻覺大語言模型在數學上的“幻覺”幾乎不可避免。它可能引用一個不存在的引理可能把一個錯誤符號寫成看似合理的形式甚至在歸納證明中把“假設成立”和“證明成立”混在一起。最好的防御不是要求模型“不要出錯”而是建立驗證關卡先做數值采樣再用符號計算檢查最后用證明助手核驗。當一條證明管線中只有“大模型生成”而沒有“驗證器把關”時不管模型多大輸出都只能當作草稿。5.3 數學資料的版權與使用邊界訓練和評測大模型時數學論文是一個重要的數據來源但并非所有論文都可以隨意爬取和復制。arXiv 上的論文大多允許非商業使用但仍有明確許可協議出版社論文的版權通常掌握在出版方手中。在工程實踐中應盡量使用開源數學庫和帶明確授權許可的數據集不要為了訓練一個內部模型去大規模抓取未授權的受版權保護論文。對于以“最小可用”為目標的個人項目優先使用公開 API 或已授權的開源模型即可。5.4 如何選擇工具鏈如果你是剛起步建議從輕量組合開始SymPy 負責代數運算Lean 負責形式化驗證一個可訪問的大模型接口負責討論和翻譯。不要一開始就搭建完整的大規模訓練基礎設施這會把大量時間花在非數學問題上。當項目進入穩定期后再考慮引入本地部署模型、自建測評集、自動化 CI 驗證等工程手段。重點不是把所有工具塞進一個系統而是保證模型中每個組件都有“可驗證的下游”大模型的輸出必須有符號系統或證明器接受否則它只是生成了一堆文本。6. 數學家的新角色與工程建議6.1 從“解題者”到“問題設計師”“英雄時代”的落幕并不等于數學不再需要個體能力。更準確的描述是數學家的核心競爭力正在從“我能親手算完這一大步”轉向“我能定義出值得自動化求解的問題”。當一個證明的主要步驟可以被機器搜索、驗證和支撐時研究者最獨特的貢獻反而不是某個細節技巧而是對問題結構的理解、對抽象層次的把握以及“把直覺轉化為可驗證規格”的能力。這其實就是一種工程能力把模糊的數學問題拆解成計算機能參與處理的任務。6.2 把證明變成可執行產物在傳統的論文發表模式中讀者拿到的是排版好的 PDF里面是一整套自然語言描述。真正想復現的人必須手動跟隨作者思路完成非常耗時的推演。AI 時代的論文可以做得更好把證明源文件、構建腳本、測試用例一并提交到代碼倉庫。建議在項目中使用版本管理工具管理證明文件每次變更都自動運行驗證器。一個簡單的 CI 工作流可以這樣構建推送新證明后自動編譯 Lean 文件運行測試腳本收集符號計算檢查結果最后生成一份可讀的報告。這能讓“形式化驗證”成為項目持續集成的一部分而不是論文之外的一次性工作。6.3 工程實踐建議代碼與證明文件混在一個倉庫時工程規范會直接影響維護成本。下面幾條建議尤其值得重視配置管理模型 API Key、base_url、模型名全部放入.env或環境變量不要寫死在代碼中異常處理網絡請求要做超時重試驗證器報錯要保留上下文日志安全邊界AI 生成的代碼不可直接運行尤其是涉及文件系統、網絡、系統命令的代碼必須經過人工審查并在隔離環境中測試版本鎖定Lean 與 Mathlib 的版本高度耦合建議鎖定版本并用 lockfile 管理 Python 依賴命名規范證明文件與論文章節一一對應盡量做到“看到文件名就知道對應哪個定理”。以上每一點都是在長期維護數學項目時容易踩坑的地方。尤其是“AI 生成代碼”的安全邊界不能因為代碼看起來能編譯就盲目運行。6.4 對學術出版與審稿的影響當證明可以形式化、可以機器驗證之后學術出版的標準也會隨之變化。未來很可能出現一種新的審稿模式論文投稿時同步提交形式化證明附件編輯先跑一遍驗證器再請專家判斷“這個問題本身是否重要、方法是否有啟發性”。這并不會取消人工審稿而是把審稿工作從繁瑣的細節檢查中解放出來讓專家把精力放在更根本的問題上。審稿人的價值不再是逐字核對推導而是判斷研究方向的創新性和概念層面的正確性。7. 總結與學習路線7.1 核心要點回顧本文圍繞“AI 是否終結了數學的英雄時代”展開核心可以概括為三點。第一數學研究正在從個體靈感中心化的模式走向多方參與、容器化驗證的網絡模式。第二AI 在數學中最真實的角色是驗證器與搜索器的組合而不是“突然會證明一切”的超級模型。第三對普通開發者來說現在就能通過 SymPy、Lean 和大模型 API 搭建一套最小可用的數學輔助與證明工具鏈。7.2 下一步學習路線如果你剛開始接觸這個方向我建議按下面的順序推進第一步用 SymPy 復現本文中的符號計算示例熟悉expand、factor、equals的能力邊界第二步在 VS Code 中安裝 Lean 擴展從rfl和簡單定理開始逐步編寫自己的證明第三步閱讀一個已形式化的開源數學項目觀察數學證明如何被拆成可維護的模塊第四步嘗試用大模型輔助翻譯一段論文中的自然語言證明再用 Lean 驗證它是否正確第五步關注自動形式化工具和 Mathlib 社區的最新進展及時更新自己的方案。這個路線不需要做大規模投入核心是建立“生成-驗證”的閉環意識。真正有價值的不是讓模型說出一個漂亮結論而是讓驗證器能持久地接受這個結論。7.3 給實踐者的最后提醒數學的“英雄時代”并不是被某一次技術突破突然終結的。它是被一個漫長而堅定的工程化進程逐步重塑的符號計算先承擔了繁瑣的代數操作證明助手再接管了嚴謹性驗證大模型的出現則進一步降低了從自然語言到形式語言的轉換成本。當你愿意從一個最簡單、最底部的證明開始慢慢把它擴展成可復現、可驗證的工程項目時“世界心智”對你就不再是一個抽象概念而是一個你正在參與其中的真實現實。這也正是這個時代最值得期待的數學實驗方式。