先說明白這篇文章聊的不是“AI能不能替代數學家”而是更具體的“AI尤其是大語言模型LLM在重大數學發展里到底有哪些已經成熟、正在嘗試或者至少值得一試的應用示例”。所謂重大數學發展可以粗略理解成一個新猜想被提出一個懸置多年的老猜想出現關鍵證明或者某個大型研究計劃進入了新階段。這類工作通常有幾個共同特征文獻量大、推理鏈長、符號體系復雜、需要反復驗證。LLM進入這個場景的價值不是直接給你一個已完成、可發表的證明而是把原本需要幾周甚至幾個月才能做完的整理、枚舉、轉譯和初步驗證工作壓縮到幾天。適合閱讀這篇文章的主要是三類人一是做數學或數學物理研究的人想了解AI工具現在能頂到哪一步二是做形式化驗證、定理證明輔助工具的工程師想知道LLM怎么接入Lean、Isabelle這類流程三是對AI for Math感興趣的開發者。我的基本判斷是現在的LLM還遠遠沒有到“自動解決重大數學難題”的階段但它足夠做一套“先產生候選結果再由人來驗證”的科研協作流水線。下面我會按實際落地順序講清楚能做什么、不能做什么、用什么判斷標準以及踩了哪些坑。1. 先想清楚LLM在數學發展里做的是“參考系”而不是“答案機”1.1 數學任務和通用文本任務的區別很多人第一次用LLM做數學題第一反應是“它能解微積分、能寫證明那是不是也能推動數學研究”這種判斷容易踩坑。普通問答里的數學題大多有明確答案、固定解法、短邏輯鏈模型只要見過類似例題就能模仿出一篇看起來合理的解答。但重大數學發展里的問題通常不是“計算一道題”而是“在一堆已知結論和未驗證假設之間搭建新的邏輯路徑”。后者對邏輯自洽性、符號一致性、引用可靠性的要求極高而這些恰恰是概率生成模型的天然弱點。更準確地說LLM給的是“有可能成立的參考系”不是“已經證明的真理”。它可以幫你快速找到可能的思路、可能遺漏的引理、可能存在反例的方向但它給出的每一步都需要重新驗證。把模型輸出直接當證明用是這類工作流里最大的失敗原因。所以我的建議是一開始就要給LLM設定正確的角色。它不是“證明機”而是“科研助手里的第一階段篩選器”。你在前面做問題拆解它負責生成候選假設、整理文獻線索、翻譯證明草稿最后由你或者形式化工具負責驗證。這樣既能發揮它的廣度和速度又不至于被它的“流暢表達”帶偏。1.2 先用一個經典小定理建立判斷直覺我一般會建議用幾道經典小定理來測試當前模型到底適合哪類任務。比如“證明根號2是無理數”“證明素數有無窮多個”這類基礎但完整的證明。別覺得這些題目太簡單它們的價值在于證明結構完整、邏輯鏈清晰、錯誤容易發現你能快速判斷模型是在“真正推理”還是在“回憶相似文本”。實測時你很快會發現幾種典型現象模型能寫出歐幾里得素數無限證明的大體框架但在“為什么若p1...pn的乘積加1的質因子不在列表中”這一步偶爾會出現含糊表述。有些模型會把“反證法”和“構造法”混在一起讀起來像證明但實際存在循環論證。有些模型會引用一個“顯然成立”的引理但這個引理本身就是目標命題。這些現象不是模型太笨而是它的訓練目標決定了它更擅長“生成概率上合理的詞序列”而不是“維護一個貫穿全文的邏輯狀態”。所以當你拿到一段證明第一件事不是看它寫得順不順而是把它拆成步驟逐條對照定義和前提看有沒有跳步。用經典小定理建立基線之后再拿它測試你研究領域里的中等難度問題。這樣能形成一張“模型能力地圖”哪些任務它能穩定輸出半成品哪些任務它基本在胡說。有了這張地圖后續在大問題上才不會被一次漂亮輸出誤導。1.3 重大數學發展中LLM真正能插入的環節如果只是一句“LLM能做數學”太泛了。放到重大數學發展這個具體場景里我覺得有三個環節最值得關注文獻線索整理大型研究計劃往往有幾百篇相關論文LLM可以快速提取某條思路的相似定義、證明技巧、后續發展并生成一份帶公式的筆記。候選命題與反例搜索從已知定理做類比擴展生成“如果滿足這些條件會不會有類似結論”的候選命題同時提出可能讓結論失效的邊界例子。證明草稿補全研究人員有整體思路但中間缺少某個引理LLM可以補一個版本再由人判斷或交給形式化工具檢查。這三個環節的共同點模型只負責“產出可能性”真正做最終裁決的是人、數值實驗或定理證明器。我不知道未來LLM會不會直接證明黎曼猜想但我知道至少在當下把它當“會讀很多論文、檢索速度快、但容易一本正經胡說”的實習生來用更合適。2. 一個可復現的最小案例讓LLM幫忙整理證明思路2.1 準備環境和輸入構造先不要一步到位部署大模型。做這類實驗入門階段用API或者在線Demo就夠了重點是“怎么把數學問題寫成模型能吃透的提示詞”。我在實際測試時發現很多人不是模型選錯而是問題描述太含糊。數學證明任務必須把三樣東西寫清楚目標命題用標準數學符號寫清楚要證明什么。可用工具允許使用哪些已證明的定理、定義、公理。輸出格式要求模型給出定義、證明思路、關鍵步驟、待驗證風險點而不是一段“散文式證明”。下面是我常用的一種提示詞框架你可以根據自己的任務調整【任務】 請幫我拆解下面這個命題的證明思路。 【目標命題】 對任意滿足條件 H 的對象 X證明性質 P(X) 成立。 【已知工具】 1. 已有定理 A說明 ... 2. 基本不等式或性質 B說明 ... 3. 可以使用反證法、歸納法、構造法等標準證明方法。 【輸出要求】 1. 先列出題目中需要明確的所有符號、定義和假設。 2. 給出證明的主思路不要一步一步寫滿但要讓讀者知道整體走向。 3. 對每個關鍵步驟標注“優先級必須驗證”。 4. 額外指出這個思路可能失敗的地方或者可能存在的反例。 【注意】 如果某個步驟引用了未說明的引理請單獨列出并說明為什么需要它。這個模板的核心作用不是讓模型直接輸出“完美證明”而是讓它在可控范圍內給出結構化的半成品。我在實際使用時會發現一旦要求模型“標出必須驗證的步驟”它的生成質量會明顯好很多因為提示詞迫使它把隱含假設暴露出來。2.2 判斷一個輸出是否值得繼續投入模型輸出了一段內容接下來不是直接信也不是直接丟。要快速做一輪“可投入度”判斷我的標準很簡單能不能把輸出翻譯成一系列可檢查的步驟。如果輸出只是一大段流暢的自然語言沒有任何定義、引理、條件分類那基本不能用于研究場景。下面這張表可以幫你快速區分可用輸出和垃圾輸出維度可用輸出垃圾輸出符號定義對每個變量、集合、映射都有說明使用未定義的符號或同一符號在不同位置含義不同邏輯關系步驟之間明顯是從前提到結論的推進前面講A后面突然跳到結論C缺少B引理引用明確說“引用定理X條件是...”并且條件確實滿足提到一個聽起來很專業但不存在的定理名風險標注會指出哪一步需要驗證、哪里可能有反例每一步都像“顯然成立”可驗證性能提取出具體條件放到數值實驗或證明器里試都是空泛的邏輯連接詞沒有可執行內容在收到第一次輸出后我會先把“待驗證風險點”提取出來作為下一步驗證清單。比如模型說“這里需要使用柯西-施瓦茨不等式但需要先確認函數在區間上平方可積”那我接下來就去檢查這個平方可積條件是否滿足。如果不滿足這條路線可能要先修正而不是繼續往下走。2.3 從單條測試到批量評估一旦單條任務跑通了你會想同時測試多個問題、多個模型或者多個提示詞版本。這里一定要控制節奏。我一開始踩過一個坑寫了一個循環一口氣提交了50個證明任務結果很快觸發了接口限流而且有一大半輸出因為輸入格式錯誤被截斷最后只能重新跑。更穩妥的方式是分三步批次規模先壓到5到10條。跑通之后檢查每條輸出是否進入預期目錄、是否占用太多資源、是否有異常報錯。給每條任務設置唯一ID把模型名稱、提示詞版本、輸入命題、輸出結果、人工評級都記錄到一張表里。這樣才能回溯是哪一輪改動導致質量下降。開一個小型隊列不要一次性并發太多。如果使用API可以限制每秒或每分鐘的請求數如果本地部署則需要觀察顯存和GPU利用率避免多個任務相互爭搶。這樣做的好處是后續你可以對每次實驗做清晰的對比。畢竟在數學研究里很多東西沒法用“感覺更好”來評判把結果結構化之后才能用數據說話。3. 在重大數學發展里更常見的三類落地點3.1 猜想形成階段讓模型生成候選命題和特例重大數學發展很少是憑空冒出來的很多時候是先有大量數值實驗和類比再被凝練成猜想。LLM在這個階段能做兩件事一是生成“類比命題”二是生成“可能讓命題失敗的特例”。舉個例子你已知某個定理在“有限生成群”條件下成立那你自然想問在“可數生成群”或者“有限表示群”條件下結論還能不能成立這種問題對數學家來說需要翻閱很多文獻因為“是否有人研究過”本身就是信息。LLM可以幫你在大量論文摘要、綜述、知識庫中做初步匹配并生成“從已知結果看條件變化后最可能失效的是哪一步”的判斷。同時它會根據已有定理的證明結構列出可能破壞結論的邊界例子。比如“如果換成分裂域”“如果去掉緊致性條件”“如果不要求光滑只是連續”等等。這些候補特例不一定對但它們能幫助你快速縮小搜索空間。我自己的習慣是把模型生成的特例拿到數值計算軟件里快速驗證能篩掉一大批明顯錯誤剩下那些不容易驗證的再人工攻。當然這條路的局限也很明顯模型沒有真正的“數學直覺”它靠的是訓練語料里的統計關聯。所以它能給出的類比通常很直接不太可能產生那種需要跨領域抽象才能發現的深刻猜想。把它當成“靈感收集器”比當成“新時代拉馬努金”更實際。3.2 交互式定理證明用LLM輔助Lean等證明腳本這是目前我覺得最接近“工程可落地”的方向之一。Lean、Isabelle、Coq這些交互式定理證明器要求每一個證明步驟都能被機器檢查。以往寫這類形式化證明非常耗時尤其是從自然語言草稿翻譯成形式化策略。LLM擅長的是“看到當前證明狀態生成下一步要執行的策略”這個模式非常適合接入證明器。流程大致是在Lean里把定理陳述寫成標準形式例如一個目標命題。把當前“證明狀態”goal和已有的上下文喂給LLM。讓模型生成一系列策略或中間斷言。把模型輸出交給Lean執行查看是否通過。這里有個關鍵認知模型不需要一次寫完整份證明它只需要生成“下一步”或者“下一步的一小段”然后通過證明器反饋來修正。這種交互模式利用了證明器的確定性彌補了模型的概率性。換句話說模型負責“出招”證明器負責“驗證”二者配合得好的時候會比我憑空讓模型寫完整證明穩定很多。但也要注意坑形式化證明的語法、庫函數命名、策略選擇都和具體版本強相關。同一個模型在Lean4和Lean3上的表現可能差異巨大。所以不要直接拿網上老的示例代碼跑先確認你的Lean版本、Mathlib版本和運行環境都正確。報錯信息里的“unknown identifier”經常不是模型思路錯而是庫里的函數名變了。3.3 長篇數學論述的梳理和交叉檢查一份重大證明草稿可能長達幾百頁里面會反復引用前面已經證明過的引理、定義和記號。人工做全文一致性檢查既辛苦又容易漏。LLM雖然不能替你證明但在“文本層面的結構梳理”上可以幫上大忙。比如你可以把文檔按章節切塊喂給模型讓它輸出每章使用了哪些定義、引理、定理和假設。然后把這些輸出匯總成一張依賴表交叉檢查某個引理到底有沒有被證明、有沒有循環引用。這種做法本質上是在做“文檔工程”但它能把人的注意力集中在真正需要數學判斷的地方而不是耗在翻頁和檢索上。再比如你可以讓模型檢查“同一個符號在不同章節是否保持一致”或者“某個定理的假設條件在使用時是否被再次驗證”。這類任務不一定要求模型理解全部數學內容它只需要對文本做結構化掃描因此成功率較高。我用下來后最明顯的感受是這類輔助工作占用時間從原來的整個半天縮短到半小時而且因為輸出結構統一我還能繼續用腳本做二次檢查。4. 判斷模型能力的關鍵指標以及怎么設置“及格線”4.1 適合用LLM處理的數學任務特征不是所有數學問題都適合交給LLM。結合我自己的測試適合的任務通常有這幾個特征允許啟發式輸出目標是尋找思路、生成候選命題、整理文獻而不是一步到位證明。有清晰驗證手段輸出可以被數值實驗、已有文獻或形式化驗證器檢查哪怕檢查本身也要花時間。邏輯鏈不超過一定長度如果問題本身需要連續推理20步以上當前模型很容易在中間某個位置出現斷裂。上下文相對完整模型能看到足夠多的定義、條件和樣例不需要“猜測”你腦中的隱含信息。下面這張表是我給任務分類的參考任務類型是否適合LLM說明生成若干候選引理適合輸出后需人工或計算驗證搜索反例的思路比較適合可以提供數值嘗試方向但需運行實驗自然語言證明翻譯為形式化策略中等配合證明器反饋可以逐步修正數百頁手稿的一致性檢查適合屬于文本結構任務不是數學推理任務直接證明未解大猜想不適合輸出無法成為可驗證的“證明”除非后續流程極嚴格要特別注意即使任務“適合”也只是一開始適合。真正落地時模型的回答質量和你的提示詞、驗證機制、容錯設計強相關。4.2 哪些任務容易被模型的“流暢表達”騙過去最容易翻車的數學任務通常是那些“模型見過很多類似文本”的任務。比如常見的數論定理、經典不等式、基礎群論結論模型很容易在開頭引用正確中間開始堆砌已知結論最后用一句“因此”收尾。表面上很完整實際上并沒有構造出有效的證明鏈。更隱蔽的是“存在性證明”和“構造性證明”混合的任務。模型可能會說“定義映射f為該集合到另一集合的映射”但完全沒說明映射的存在性、良定義性或者是否依賴于選擇公理。對受過訓練的人來說這種跳步可以被發現但如果只是讀一遍很容易被它的“專業感”迷惑。因此在大型數學發展里用LLM時我建議對所有模型輸出設置一個共同原則任何沒有被獨立驗證的聲明都只當作候選材料處理。哪怕它引用了某個定理也要去查原文獻確認定理條件確實適用于當前情境。這不是不信任模型而是概率模型本身的邊界決定了它無法保證邏輯確定性。4.3 怎么給模型輸出設置“及格線”“及格線”不是“模型回答得對不對”而是“這份回答能不能進入下一步驗證流程”。我一般用四個層次L0無法使用。輸出混亂、符號未定義、邏輯跳躍直接丟棄。L1可以摘取片段。整體不可靠但里面某幾個例子、某個引理名稱、某個數值方向有價值可以提取出來。L2可以進入半自動驗證。輸出結構完整可分離出關鍵斷言我可以用計算腳本或證明器逐一檢驗。L3可以作為草稿繼續推進。大部分步驟都合理需要補充的只是具體計算和細節整理。用這個分級標準每次模型輸出后都有明確的去向而不是籠統地“覺得還行”。在研究了幾個真實案例之后你會發現L2和L3的比例通常不高但這并不代表LLM沒用因為L1里經常藏著有價值的線索。真正重要的是你不能把L1當成L3來用。5. 資源環境與批量化本地、API和集群怎么選5.1 入門階段的最低配置如果你只是想試一下這個主題先不需要急著部署本地大模型。用常見API、開源模型的在線Demo或者跑一個量化過的中小型模型都可以完成大部分實驗。這個階段需要的不是滿血的推理能力而是低成本、快速迭代。本地部署的低配參考大概是16GB內存加一張8GB顯存的GPU能跑7B參數級別的量化模型處理單條數學證明思路沒問題但速度不快。如果是13B、14B模型最好有16GB以上顯存如果沒有獨顯只靠CPU也能跑但你要有等待的心理準備一個長文本生成任務可能要幾分鐘甚至更久。比較穩妥的順序是先用API或在線環境驗證提示詞和流程等確認這套流程有穩定價值后再考慮本地部署。千萬不要一開始就花大量時間配置服務結果發現你的問題根本不適合LLM處理。5.2 批量任務的資源管理和日志結構當你開始批量測試最重要的事情就不是單個模型有多強而是任務管理有多規范。我建議至少記錄以下信息字段說明任務ID每個輸入的唯一編號方便回溯模型名稱包括版本號例如“某個開源模型的7B量化版”提示詞版本因為你一定會多次修改提示詞輸入命題原始目標命題輸出文本模型生成的完整結果人工評級L0/L1/L2/L3驗證結果是否通過了數值驗證、證明器或人工檢查錯誤信息如果有超時、截斷、格式錯誤記錄原始異常批量任務不要一上來就開最大并發。如果你的接口有限速并發太大會直接觸發429或者被斷開如果你本地部署多個請求同時跑會導致顯存溢出或響應時間急劇上升。我一般會從“1個并發”開始跑通后再逐步增加到2、4、8同時觀察成功率和延遲的變化。5.3 本地部署時我自己踩過的幾個坑本地部署數學任務時最常遇到的問題不是模型不會推理而是環境配置把你的時間吃掉了。列幾個高頻坑端口被占用啟動服務時提示“端口已被使用”先查進程不要直接換端口因為你后面對接的代碼可能寫死了地址。上下文長度限制數學證明往往需要把前面的定義和引理塞進上下文很多模型默認的context window不夠用。生成到一半突然丟失前文輸出后半段就會跑偏。max_tokens限制一次生成的最大長度設置太小模型還沒寫完整就被截斷。這個問題會把一個有潛力的證明思路切成殘稿。顯存溢出批量任務或長文本生成時最容易出現。解決辦法一般是降低批量數、降低推理精度、或者切斷超長輸入。我建議的排查順序是先用最短的輸入做一次生成確認服務能啟動、輸出不是空然后逐步增加輸入長度觀察顯存和內存占用最后再跑批量。這樣你才能確定一個“最大安全輸入長度”避免后續任務集體失敗。6. 失敗模式和排查順序為什么“模型說得對”不等于“證明是對的”6.1 最常見的三類失敗用LLM做數學研究失敗是常態關鍵是要識別它們。我遇到最多的三類失敗是這樣的幻覺引理模型引用一個聽起來很標準的定理但實際并不存在或者條件與當前命題不匹配。比如明明是在實變函數問題的證明里突然搬出一個“據復分析里的某某定理”之類的說法。符號漂移同一個變量在文章前半段表示集合后半段變成映射或者“n”在第一個引理表示正整數在第二個引理里變成某個生成元的個數。這種錯誤在長篇生成里幾乎無法避免。邏輯跳步模型知道開頭和結論但中間省略了關鍵的構造或驗證步驟。省略的原因可能是上下文被截斷也可能就是模型覺得“太簡單不用寫”。這三種失敗都不是偶發問題而是概率生成模型的結構性特征。我們需要接受這個現實然后用流程去兜底。6.2 數學場景下的排查鏈路如果模型輸出出了問題先不要急著換模型、調溫度、改并發。我建議按下面的順序排查先看輸入提示詞是否完整。目標命題、可用工具、輸出格式是否寫清楚如果連“需要定義的符號”都沒讓模型寫它當然容易亂造。再看模型輸出中的變量、定理引用和邏輯步驟。把每一步單獨拆出來和原始定義、已知條件對照。重點不是“這句話通不通”而是“這個變量的類型對不對”“這個引理的適用條件滿不滿足”。如果輸出是形式化證明腳本運行證明器看具體報錯。比如Lean的“unsolved goals”“type mismatch”會準確告訴你問題在哪一步。此時不要因為模型寫了10行策略就忽略最后一行錯誤。最后才調整模型或參數。溫度、top_p這些參數主要影響隨機性不能解決邏輯斷裂。如果同樣的輸入反復失敗問題多半不在參數而在任務分解或驗證機制。我把這個順序寫成了一個清單每次實驗前都過一遍。你會發現很多時候“模型不行”其實是輸入材料或驗證過程沒跟上。6.3 降低風險的具體策略與其期待模型變得更強不如在流程設計上降低風險。我常用的幾招強制分步輸出在提示詞里要求“先列出需要的引理再給出證明思路”。這樣即便最終證明失敗你也能拿到一份引理清單繼續排查。要求標注待驗證聲明讓模型對每個關鍵步驟標出“這里需要獨立驗證”。這可以逼它把隱含假設暴露出來。自動抽查關鍵信息把輸出中的定理名、公式、變量提取出來和已有論文或符號庫做匹配。雖然不能驗證邏輯但能很快發現“引用一個不存在的定理”這種問題。重要結論必須過證明器或人工復核只要一條路線可能進入正式論文就不能停留在“模型說可以”。這些策略不會讓模型變聰明但它們能把“模型產生的噪音”控制在可管理的范圍內。7. 我的經驗先把“小定理跑通”再談“重大發展”7.1 從經典問題開始建立基線如果你想在這個方向認真投入我特別建議先花一兩周時間做“小定理跑通”訓練。選一個你熟悉的數學分支找三到五個經典引理讓LLM給你生成證明思路再逐條驗證。不要選太容易的也不要選世界難題選那種“你完全知道標準證明但過程有幾步需要仔細檢查”的問題。記錄下三個指標結構完整率輸出中是否有完整的定義、條件和結論。可驗證步驟比例輸出的步驟有多少能直接進入計算或證明器驗證。有效修正次數在人工介入后你需要修正多少次才能得到可靠證明。這些數據會告訴你這個模型在你這個領域里到底處于什么水平。我測試下來不同模型在不同數學分支上的表現差異很大不能簡單說“某模型擅長數學”。7.2 把LLM當作科研流水線上的“第一階段篩子”在真正涉及重大數學發展的工作中我更愿意把LLM看成“第一階段篩子”。它的作用不是做最終判斷而是快速擴大搜索范圍。比如一個研究方向有100種可能的路徑人的精力只能認真看5種LLM可以幫你從100種里挑出15種“至少在文本層面沒有明顯矛盾”的路徑然后你再重點投入。這個篩選過程不是“用模型代替判斷”而是“用模型降低試錯成本”。一條路徑會被淘汰往往不是因為它在數學上真的不可行而是因為資料查找和初步嘗試的成本太高。LLM把這一步成本壓下來之后整個科研流程的推進速度會明顯更快。當然這也意味著你需要有一套嚴格的“淘汰標準”。我習慣在篩選時就明確寫出什么樣的情況算“值得繼續”什么樣的情況算“直接放棄”。比如說如果模型給出的證明思路在第一步就需要一個未被證明且看起來很難證的引理那我可能立刻降低優先級如果模型給出的主要困難恰好是當前研究計劃里已經準備處理的步驟那就可以繼續。7.3 給想入坑的人三條建議最后給想在這個方向投入的人三條建議都是我自己踩過坑以后才總結出來的從可驗證的小問題入手不要直接挑戰大猜想。大猜想如果失敗你分不清是模型能力問題、提示詞問題還是這個猜想本身太難小問題可以幫你把變量控制住。給模型的輸出預設驗證機制不留“可能對”的模糊地帶。每一步輸出都應該能映射到某個可執行檢查數值計算、已有文獻、證明器、人工重寫。把每一次實驗記錄成可復現材料。包括提示詞、模型版本、輸入命題、輸出結果、驗證結論。沒有記錄就無法判斷自己是在進步還是在原地打轉。我更傾向于把LLM看成“數學工作的協處理器”而不是“證明機”。它真正能幫上忙的地方是讓那些大量重復、文獻密集、結構繁瑣的前期工作變得不那么消耗人。至于最終證明是否成立還是要靠形式化工具、同行評審和你自己的數學判斷。如果你能把這兩者結合起來現在就能把很多“不可能完成”的初期調研任務變成“只要花一個下午就能跑完的實驗”。