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