人工智能在數學領域的應用：進展、挑戰與展望

https://arxiv.org/pdf/2601.13209v1

AI for Mathematics: Progress, Challenges, and Prospects

人工智能在數學領域的應用：進展、挑戰與展望

摘 要

人工智能用于數學（AI for Mathematics，簡稱 AI4Math）已作為一個獨立領域出現，它利用機器學習來探索那些對早期符號系統而言歷來難以處理的數學領域。盡管20世紀中期的符號方法成功實現了形式邏輯的自動化，但由于搜索空間的組合爆炸，它們在可擴展性方面面臨嚴重限制。近期數據驅動方法的引入重新激發了這一研究方向。

在本綜述中，我們對 AI4Math 提供了系統性的概述，強調其主要目標是開發人工智能模型以支持數學研究。至關重要的是，我們指出這不僅限于將人工智能應用于數學活動；它同時也包括構建更強大的人工智能系統——其中數學所具有的嚴謹性可作為推進通用推理能力的頂級試驗平臺。

我們將現有研究劃分為兩個互補方向：一是面向特定問題的建模（problem-specific modeling），涉及為不同數學任務設計專用架構；二是通用建模（general-purpose modeling），聚焦于能夠支持更廣泛推理、檢索與探索性工作流的基礎模型（foundation models）。

最后，我們討論了關鍵挑戰與未來前景，倡導開發超越僅確保形式正確性的 AI 系統，轉而致力于促成有意義成果與統一理論的發現，并認識到一個證明的真正價值在于它為整個數學領域所提供的洞見與工具。

關鍵詞：機器學習，深度學習，形式驗證，自動形式化，數學發現，自動推理，數學信息檢索

1 引言

自人工智能（AI）誕生以來，數學推理的自動化一直是其核心目標之一。機械化推理的夢想甚至早于數字計算機的出現，可追溯至20世紀20年代，當時大衛·希爾伯特（David Hilbert）提出了一個綱領，旨在將全部數學形式化，以期在一致的公理系統內證明所有定理。盡管這一樂觀愿景在1931年受到庫爾特·哥德爾（Kurt G?del）不完備性定理的理論挑戰——該定理表明，任何足夠豐富的形式系統必然是不完備的——但哥德爾的結果并未終結這一研究方向。正如烏拉姆（Ulam）[116]所指出的，馮·諾依曼（von Neumann）認為這些發現應促使人們重新思考形式主義的角色，而非徹底放棄它。后續研究進一步表明，經典數學的大部分內容可以進行有窮主義的約簡[111]，從而維持了部分機械化夢想的活力。

隨著數字計算機的出現，這些理論構想被付諸實踐。20世紀50年代，馬丁·戴維斯（Martin Davis）實現了普雷斯伯格算術（Presburger arithmetic）的一個判定過程[27, 35]，這可被視為計算機機械驗證邏輯命題的首個實例。不久之后，紐厄爾（Newell）、西蒙（Simon）和肖（Shaw）開發了“邏輯理論家”（Logic Theorist）[97]，被廣泛認為是第一個真正意義上的人工智能程序，它能在符號邏輯中進行定理證明。在符號主義時代，一個尤為具有影響力的里程碑是吳文俊（Wen-Tsun Wu）提出的幾何定理機器證明方法[131, 133]。他通過將幾何問題轉化為代數方程組，并應用特征集方法，展示了復雜的邏輯推論可以被算法化地導出。

然而，大多數這類符號方法面臨一個關鍵瓶頸：搜索空間的組合爆炸。隨著證明復雜度的增加，可能的邏輯路徑數量呈指數級增長，使得窮舉搜索變得不可行。近幾十年來，機器學習的引入重新激發了這一研究方向，提供了數據驅動的方法來導航這些復雜的數學空間。自2010年代起，聯結主義人工智能（connectionist AI）迅速崛起，在計算機視覺和自然語言處理領域取得了顯著成功。數學家們隨后開始利用這些模型來識別可引導人類直覺的模式[34, 39, 57]，通過強化學習（RL）構造反例[54, 109, 119]，以及訓練神經定理證明器[10, 132]。更近以來，大語言模型（LLMs）的飛速發展已能夠生成新的數學構造[50, 98, 105]、實現自動形式化（autoformalization）[95, 135]，并支持協作式定理證明[156]。

這一融合催生了跨學科領域“人工智能用于數學”（AI for Mathematics，簡稱 AI4Math）。我們強調，AI4Math 不僅是將人工智能工具應用于數學任務，還包含構建更強大的人工智能系統——其中數學所具有的嚴謹性可作為推進通用推理能力的頂級試驗平臺。廣義而言，該領域的研究可分為兩個互補方向：

• 面向特定問題的建模（Problem-Specific Modeling）：涉及為特定研究問題或狹窄類別的數學問題設計專用架構，例如在紐結理論中引導直覺，或在封閉幾何系統中進行推理。除了在目標任務上具有高度有效性外，這些模型通常所需的數據量和計算資源顯著較少，使更廣泛的科研人員能夠使用。然而，若不進行大量修改，它們很少能遷移到其他領域。
• 通用建模（General-Purpose Modeling）：聚焦于開發基礎模型（foundation models），包括專門面向數學的語言模型到通用推理引擎，旨在支持跨多個數學領域的廣泛工作流。盡管具備通用性，但這類方法需要海量訓練數據、大量計算資源以及深厚的工程專業知識。此外，當應用于定義明確的狹義數學問題時，它們可能無法達到專用模型那樣的針對性和有效性。該方向涵蓋自然語言推理的進展、通過自動形式化彌合非形式與形式數學之間的鴻溝，以及構建能夠自動定理證明和信息檢索的智能體系統。

值得注意的是，AI4Math 的技術范疇實際上超出了邏輯推理，還包括“人工智能用于計算數學與科學計算”。該子領域致力于構建人工智能模型以輔助數值計算，例如求解偏微分方程（PDEs）、優化問題和反問題。這一方向的根源可追溯至1980至1990年代，當時研究者探索使用淺層神經網絡近似微分方程的解。然而，該領域在2015年前后隨著深度學習的興起而迎來復興。盡管這些計算方面的進展構成了更廣泛 AI4Math 圖景中的重要支柱，但本綜述將聚焦于數學推理——包括數學發現、形式化與證明。對 AI4Math 計算方面感興趣的讀者可參考其他綜合性綜述文獻[6, 17, 21, 38, 70, 130]。

本文對 AI4Math 的進展、挑戰與前景提供系統性概述。我們的目標并非窮盡所有工作，而是突出具有代表性的成果，以展現該領域的演進脈絡。對特定子領域感興趣的讀者可參閱關于幾何自動推理[25, 134]或用于定理證明的深度學習[85]等現有綜述。第2節考察面向特定問題的建模，第3節回顧通用建模。最后，第4節討論未來面臨的關鍵挑戰，倡導開發超越簡單驗證、邁向發現深刻數學洞見的系統。

2 面向特定問題的建模

隨著數據驅動技術的快速發展，研究人員開始設計專門的機器學習模型，以應對特定的數學研究問題。這些工作大致可分為三個方向：
（1）在高維數據中識別模式，以引導人類直覺并激發新猜想；
（2）構造例子或反例，以嚴格檢驗或證偽數學假設；
（3）在封閉的公理系統（如歐幾里得幾何）內進行形式推理。
本節將回顧這三個領域的最新進展，并討論各自的優勢與局限。

2.1 通過機器學習引導人類直覺
利用機器學習輔助提出數學猜想的早期范例之一是文獻[18]。該研究采用線性回歸預測大量F理論幾何結構中幾何規范群的秩，成功重新發現了關于規范群秩的一個已有猜想。在此基礎上，作者進一步將邏輯回歸應用于涉及E?規范群的分類問題；通過對模型進行歸因分析（attribution analysis），他們提出了一個全新的猜想，隨后由人類數學家完成了證明。

然而，真正展示深度學習在數學研究中廣泛潛力的關鍵性工作是文獻[34]。該研究的核心貢獻是一個系統性框架，旨在加速猜想生成過程——傳統上，這一過程耗時漫長，需數學家反復提出關系假設、嘗試證明并迭代優化思路。在[34]提出的流程中，數學家首先假設兩個數學對象之間可能存在某種關系；隨后訓練一個專門設計的神經網絡，用其中一個對象的特征預測另一個量；接著使用歸因方法識別最具影響力的輸入成分，從而引導數學家形成更精確、更精細的猜想。該循環不斷重復，直至得出具有數學意義的命題。利用這一方法，作者在紐結理論中發現了一個代數不變量與幾何不變量之間的新關系[33]，并基于對稱群的組合不變性猜想提出了一個候選算法[15]。

受此范式啟發，文獻[39]為仿射Deligne–Lusztig簇（ADLV）的研究設計了另一套AI引導直覺的框架。該工作不僅獨立重新發現了算術幾何中的經典“虛擬維數公式”，還建立了一個新穎且精確的下界定理。該結果通過提供一種填補重要理論空白的定量刻畫，展示了AI引導直覺在純數學深層領域促成嚴格發現的有效性。

除精煉猜想外，機器學習還被證明能揭示全新的數學現象。一個突出的例子是文獻[58]：作者將橢圓曲線表示為向量，并訓練邏輯回歸分類器以區分不同秩的曲線。為解釋分類器的優異性能，他們對向量表示進行了主成分分析（PCA）。在繪制固定秩和導子（conductor）的橢圓曲線的Frobenius跡平均值時，他們發現了一種令人驚訝的振蕩模式，并將其命名為“低語”（murmurations）。這一現象此后成為深入理論研究的對象[16, 81, 158]。越來越多的文獻正持續利用機器學習在各類數學領域中發現或重新發現關系[5, 12, 14, 18, 42, 55, 72, 77, 79, 80, 106]。

2.2 構造例子與反例
將機器學習用于構造例子和反例的開創性工作之一是文獻[119]。該研究將圖編碼為0–1序列，并應用強化學習（RL）中的深度交叉熵方法，搜索可作為現有猜想反例的圖結構。在此先例之后，RL被廣泛用于多種結構性問題。例如，文獻[11]將代數幾何中奇點消解的核心框架——廣中（Hironaka）博弈——建模為馬爾可夫決策過程（MDP）。通過結合蒙特卡洛樹搜索與深度Q網絡，作者成功訓練出一個智能體，能將奇點替換為光滑點，在du Val奇點上實現了近優的消解。類似地，文獻[109]研究了Andrews–Curtis（AC）猜想。作者首先使用經典搜索算法驗證了Miller–Schupp序列無限子族的AC平凡性，并在Akbulut–Kirby序列中實現了長度縮減；隨后將一般問題形式化為MDP，并在不同難度的問題實例上訓練RL智能體，最終發現了兩個此前經典搜索方法未能找到的平衡展示（balanced presentations）的新型AC平凡化。

除強化學習外，多種其他機器學習技術也被用于數學構造。文獻[4]在合成數據上訓練Transformer模型，以預測穩定動力系統的Lyapunov函數；訓練后的模型被用于發現非多項式系統的新Lyapunov函數。在組合數學中，文獻[19]提出了一種迭代自舉（bootstrapping）流程：該方法首先通過局部搜索算法生成候選構造，再在得分最高的候選集上訓練神經網絡，然后從網絡中采樣新種子以初始化下一輪局部搜索。利用此方法，作者成功找到了一個存在30年之久的猜想的反例。此外，文獻[13]應用遺傳算法生成2至5維的自反多面體（reflexive polytopes），在5維中識別出若干此前未知的多面體。其他利用機器學習構造例子或反例的工作還包括[23, 24, 54, 112]。

2.3 面向特定問題的形式推理

AlphaGeometry [115] 是一種神經符號方法，用于求解奧林匹克級別的歐幾里得幾何問題。它將一個符號化的幾何推理引擎與一個用于建議輔助構造的語言模型相結合。其符號組件基于演繹數據庫（Deductive Database, DD）[26]和代數規則（Algebraic Rules, AR），能夠對給定前提集進行窮盡式推導，生成其演繹閉包。然而，純粹的符號演繹無法引入新的幾何對象——而這一能力在復雜證明中常常是必需的。為此，系統利用語言模型提出有用的輔助點。為克服人類證明數據稀缺的問題，作者通過交替執行符號演繹與隨機點插入，生成了一個大規模的合成證明圖數據集，并通過回溯（traceback）提取出最簡證明。在推理階段，系統以循環方式運行：符號引擎擴展演繹閉包，語言模型提出高概率的輔助點，循環重復直至達到目標結論。該架構使 AlphaGeometry 的性能顯著優于基于啟發式的系統，達到了國際數學奧林匹克（IMO）銀牌水平。

其后續版本 AlphaGeometry2 [22] 通過在表達能力和效率兩方面的增強，進一步推進了這一范式。形式化幾何語言被擴展，以支持軌跡描述、線性幾何關系以及非構造性陳述；底層符號引擎也經過重新設計，速度更快、魯棒性更強。這些改進使得語言模型能夠使用更大、更多樣化的合成訓練集進行訓練。此外，AlphaGeometry2 引入了一種新穎的搜索算法——“共享知識搜索樹集成”（Shared Knowledge Ensemble of Search Trees, SKEST），該算法并行執行多個搜索樹，并允許它們交換所發現的信息，從而顯著提升了對輔助構造空間的探索能力。因此，AlphaGeometry2 在 IMO 級別幾何問題上達到了金牌水平。

除了基于神經網絡的輔助點生成方法外，近期工作如 HAGeo [41] 提出了一種純啟發式策略，通過引入具有優良幾何性質的輔助構造（如直線與圓的交點、中點、點反射等），同樣實現了金牌級別的性能。其他關于歐幾里得幾何問題求解的工作可見于 [59, 147, 151, 152, 157]。

2.4 討論

本節所討論的三類方法——通過識別模式引導直覺、構造反例、以及在封閉系統中進行形式推理——各自具有獨特優勢，同時也面臨不同的挑戰。

AI引導直覺的范式之所以強大，在于它使數學家能夠發現高維數據中難以或耗時手動檢測的模式，從而有效縮小探索性研究中的搜索空間。然而，該方法并非普遍適用。它依賴于精心選擇的問題，因為目標問題必須能夠生成足夠大且具有代表性的數據集。此外，成功實施需要較高的雙重專業門檻：除了標準的機器學習考量（如架構設計、損失函數工程）外，深厚的數學洞察力對于解釋模型輸出并將經驗性關聯轉化為嚴格數學理論至關重要。最終，由于證明和驗證通常仍由人類數學家完成，該工作流的自動化程度仍然有限。

另一方面，利用機器學習構造例子與反例可顯著加速猜想的提出與檢驗，尤其能發現違背人類直覺的對象。然而，這一方向也面臨技術障礙，特別是分布外（out-of-distribution, OOD）泛化問題。例如，文獻[4]中從采樣解反向生成問題的方法可能產生具有特定分布的訓練集，這在泛化到典型問題實例時會帶來挑戰，通常需要精心設計的機制（如作者提出的促進Lyapunov函數多樣性的機制）來確保魯棒性能。此外，當使用強化學習時，將數學問題映射為馬爾可夫決策過程（MDP）并非易事。定義合適的狀態表示、動作空間和獎勵函數可能非常復雜[119]，而稀疏獎勵和長規劃視野等問題還會進一步加劇學習難度[109]。

最后，像 AlphaGeometry 這樣的面向特定問題的形式推理系統表明，在結構化領域中，將符號引擎與神經語言模型結合可達到專家級性能。然而，這些系統的成功通常依賴于特定領域的符號引擎（例如用于幾何的演繹數據庫[26]）以及生成大規模合成數據的能力。因此，這類架構往往高度定制于其特定問題范圍，若不進行大量修改，難以遷移到數學的其他領域。

3 通用建模

通用建模標志著從為孤立問題設計的專用算法，轉向能夠處理廣泛數學領域的可適應系統。與面向特定問題的建模不同——后者針對每個新任務都需要定制特征和架構——通用建模方法利用在海量語料上訓練的基礎模型（foundation models），學習數學知識的通用表示。這些模型旨在支持多種活動，從求解多樣化的習題集，到檢索定理，再到協調復雜的發現工作流，而無需為每個新領域進行大量修改。

我們將通用建模領域的近期進展劃分為四個互補方向：
（1）利用語言直觀力量的自然語言推理模型；
（2）通過與證明助手交互以確保嚴謹性的形式推理模型；
（3）將推理錨定于既有知識的數學信息檢索系統；
（4）整合上述能力以探索新成果的數學發現智能體。

本節首先分析基礎模型（尤其是大語言模型，LLMs）的能力與內在局限，為后續對這四個關鍵方向的詳細綜述奠定背景。

3.1 基礎模型與大語言模型（LLMs）
與傳統機器學習模型（通常針對單一、狹義定義的任務進行訓練）相比，大語言模型作為基礎模型：采用單一架構，在廣泛的數據和任務集合上以統一方式進行訓練。從數學角度看，這一區別代表了一種范式轉變——從函數逼近（function approximation）轉向算子逼近（operator approximation），而這一過程與元學習（meta-learning）密切相關。

其成功的一個關鍵因素在于處理多樣化數據類型的能力：分詞（tokenization）將異構輸入轉換為統一的序列表示，而“下一個詞元預測”（next-token prediction）目標則提供了一條適用于模型所遇所有任務的統一學習規則。在此框架中，基于注意力的架構至關重要。除了能有效隨模型規模和數據量擴展外，注意力機制在訓練過程中通過強制長上下文一致性，成為推理的核心引擎。這使得模型能夠捕捉并維持長序列中的復雜依賴關系——這是邏輯演繹的先決條件。通過接觸多樣化的領域和監督信號，模型被迫將海量異構數據壓縮為共享的內部表示，并在不同任務與語言之間發現共同的低維結構。一個自然的假設是，該低維結構中的關鍵組成部分對應于通用推理能力，這種能力可在不同語言和領域中表達。

數學天然契合這一框架。數學工作受嚴格邏輯規則支配，許多數學任務可被表述為在計算、推導或證明中生成下一個有意義的步驟——這正是“下一個詞元預測”目標所設計建模的逐步結構。因此，當大語言模型作為基礎模型在足夠豐富的數學與科學語料上訓練時，支撐跨領域泛化與長上下文一致性的相同機制，也可用于學習和運用廣泛的數學推理能力。

然而，在掌握標準化考試與從事研究級數學之間仍存在根本性鴻溝。盡管當前模型在求解定義明確的本科水平問題上表現出色，但真正的數學研究要求開放式的探索、絕對的邏輯嚴謹性，以及駕馭高度專業化領域知識“長尾”的能力——在這些方面，隨機性文本生成往往力有不逮。要將人工智能從一名勝任的解題者提升為可靠的科研伙伴，通用建模必須超越簡單的“下一個詞元預測”，通過整合形式驗證、語義檢索與智能體工作流，彌合“看似合理文本”與“嚴格真理”之間的鴻溝。

3.2 自然語言推理

當前的自然語言數學推理方法通常分為兩類：數學專用的大語言模型（math-specific LLMs） 和 通用推理模型（general-purpose reasoning models）。

數學專用的大語言模型通常通過對通用基礎模型進行專門的預訓練和后訓練流程（pre-training and post-training pipelines）加以適配。在預訓練階段，過濾流水線（filtering pipelines）[107, 141] 從網絡語料（如 Common Crawl）、教科書和研究論文中提取高質量的數學內容，以最大化領域相關性。后訓練階段則通過監督微調（Supervised Fine-Tuning, SFT）和強化學習（RL）對模型進行進一步優化。

用于監督微調（SFT）的數據通常以“思維鏈”（Chain-of-Thought, CoT）[129]對的形式組織，包含問題及其分步解答；或采用“工具集成推理”（Tool-Integrated Reasoning, TIR）[53]示例，其中整合了外部代碼執行。一個突出的例子是 NuminaMath [83]，它通過對高質量的 CoT 和 TIR 數據集進行微調，在首屆 AIMO 進展獎（AIMO Progress Prize）中拔得頭籌。盡管這類模型 [9, 107, 141, 144] 在基礎數學和競賽級基準測試（如 GSM8K [28]、MATH [60]、AIME）上表現出色，但其在高等數學方面的能力仍較少被探索。

與此同時，通用大語言模型（general-purpose LLMs）憑借規模擴展和新穎的推理策略，在數學領域也取得了顯著進展。早期版本如 GPT-3 在基本算術任務上表現不佳，而 GPT-4 [1] 在 GSM8K 上達到了 92.0% 的準確率。隨著“測試時擴展”（test-time scaling）的引入，該領域發生了范式轉變——模型在推理階段投入更多計算資源用于推理。OpenAI 的 o1 模型在 AIME 上展現出強大性能，后續的推理模型 [30, 56, 114, 140] 進一步驗證了這一方法的有效性。截至 2025 年，增強型推理模型（如 Google 的 Gemini Deep Think）僅依靠純自然語言推理，就在國際數學奧林匹克（IMO）中達到金牌水平，標志著該技術在中學奧數領域已趨于成熟。

然而，從奧數問題過渡到高等數學提出了更嚴峻的挑戰。先前研究表明，盡管 GPT-4 能輔助處理本科階段的內容，但仍需人類的關鍵監督 [29]，且在研究生層次上常常失敗 [45]。近期的基準測試量化了這一差距：文獻 [69] 報告稱，DeepSeek-R1 在研究生代數（FATE-H）上的證明準確率為 71.0%，但在博士資格考試（FATE-X）上驟降至 33.0%。同樣，在由未發表的研究級問題組成的 FrontierMath 基準測試 [51] 中，Gemini 3 Pro 在研究級子集上的得分僅為 18.75%，表明穩健的研究級推理能力仍是一個開放性問題。

為實證評估當前最先進模型的能力，我們構建了一個包含 100 道題目的數據集，題目選自北京大學（PKU）11 門本科數學課程的期末考試。我們評估了五個模型：GPT-4、o1、o3-mini、DeepSeek-R1 和 Gemini 2.5 Pro。附錄 B 提供了樣題及模型回答。人類專家根據 0–5 分制（評分標準見表 A）對輸出進行打分，歸一化后的結果如圖 1（左圖和中圖）所示。盡管 GPT-4 得分低于 60，但經過推理增強的模型（OpenAI o 系列、DeepSeek-R1、Gemini 2.5 Pro）表現顯著提升，其中多個模型得分超過 90。

此外，我們還在北京大學博士資格考試（涵蓋分析、概率、代數、幾何與拓撲）的 58 道題目上評估了 o3-mini。如圖 1（右圖）所示，o3-mini 的平均得分為 84.4。進一步分析各科表現可發現明顯差異：該模型在代數方面表現最強，而在幾何與拓撲方面得分最低。假設這些考試對人類學生構成相近難度，則這一結果表明，當前的人工智能系統在處理抽象代數結構方面相對更擅長，而在需要幾何直覺的任務上相對較弱。盡管由于潛在的數據污染風險以及考試題目與開放性研究問題之間的本質差異，這些結果需謹慎解讀，但它們提供了有力證據：頂尖模型如今已能處理相當一部分研究生層次的數學內容。

綜合上述發現，我們觀察到一條清晰的發展軌跡：大語言模型的數學推理能力已從掌握基礎運算和中學競賽，發展到勝任本科課程內容，并正開始進入研究生乃至研究級數學的領域。

3.3 形式推理
盡管頂尖的大語言模型（LLMs）如今已能解決某些研究生層次甚至部分研究級數學問題，但對其能力的評估仍是一個重大瓶頸，需要大量人工投入。隨著數學復雜性的增加，評估高度依賴領域專家；然而，由于自然語言本身具有內在的模糊性，即便是經驗豐富的數學家也可能誤判論證。一個著名的歷史案例發生在1994年：《數學年刊》（Annals of Mathematics）發表了一篇論文，聲稱Busemann–Petty問題在四維及以上維度具有負解 [148]。該結論后來被證明是錯誤的 [73, 74]，而1999年的一篇論文最終確立了該問題在四維情形下實際上具有正解 [149]。這一事件表明，即使在頂級期刊嚴格的同行評審流程中，錯誤仍可能長期存在。因此，為了實現對數學推理快速且可靠的驗證，研究必須轉向一種更機械化、更無歧義的框架。形式系統（formal systems）恰好提供了這樣的基礎。本節將討論形式系統對數學研究的益處及其在增強大語言模型推理能力方面的價值，隨后綜述自動定理證明與自動形式化（autoformalization）領域的最新進展。

3.3.1 形式系統
形式系統提供了一種精確的符號語言，并配以嚴格定義的機制，用于構造和驗證證明。目前存在多種形式系統，其區別在于底層邏輯基礎：HOL 系統（如 HOL Light、Isabelle/HOL）采用簡單類型論（simple type theory）；Coq 和 Lean 使用依賴類型論（dependent type theory）；Metamath 基于一階邏輯并顯式指定公理；而 Mizar 則建立在 Tarski–Grothendieck 集合論之上。一旦將數學論證翻譯成交互式定理證明器（Interactive Theorem Prover, ITP）的形式語言，即可對其進行絕對嚴謹的驗證。倘若1994年那篇關于 Busemann–Petty 問題的錯誤結果當初在形式系統中被形式化，其潛在的邏輯缺陷很可能立即被發現，從而避免錯誤結論的發表。

除了對數學正確性本身具有內在價值外，形式系統對人工智能發展還提供了一個關鍵優勢：它們提供了可靠且可驗證的監督信號。與初等數學不同（其答案常為數值，易于核對），面向證明的高等數學問題缺乏簡單的驗證器，難以生成可靠的訓練信號。交互式定理證明器通過為每一步邏輯推理提供精確反饋，彌補了這一缺口。這種能力為強化學習（RL）提供了高質量的訓練信號，從而使模型能夠在嚴格環境中發展出更強的推理能力。

在眾多交互式定理證明器中，Lean [36, 37] 已培育出一個尤為強大的生態系統。其統一的數學庫 mathlib4 通過大規模社區協作迅速擴展，截至2025年12月，已包含超過25萬條定理和12萬個定義。該領域的一項里程碑式成就是由 Johan Commelin 主導的“液態張量實驗”（Liquid Tensor Experiment），該項目形式化了 Peter Scholze 關于液態向量空間的一個核心定理。Scholze 最初對該證明的正確性存有疑慮，后來稱該定理可能是他“迄今為止最重要的成果”2。該項目歷時約18個月，不僅驗證了該結果，還簡化了 Clausen–Scholze 原始證明，幫助 Scholze 更深入地理解了論證的結構3。此外，“液態張量實驗”還推動了 mathlib4 中代數基礎設施的發展：它促成了同調代數與范疇論的早期形式化，并吸引了一大批代數學家加入社區。

其他值得注意的里程碑包括：Polynomial Freiman–Ruzsa（PFR）猜想的形式化、球面翻轉定理（sphere eversion theorem）的形式化，以及由 Kevin Buzzard 領導的費馬大定理（Fermat’s Last Theorem）形式化工作。在應用數學方向，近期研究還在 Lean4 中建立了數值優化的形式化基礎，特別是驗證了一階算法的收斂性 [82]。

然而，這些項目仍然高度依賴人力，需要專家手動將定義和證明翻譯為代碼。這種高昂的成本推動了自動形式化工具與自動定理證明器的發展，以加速數學知識的數字化進程——即將標準的非形式化數學轉化為 Lean 等嚴格形式系統中的內容。

3.3.2 自動形式化（Autoformalization）
自動形式化是指以自主方式（例如通過語言模型）將自然語言中的數學陳述和證明翻譯為形式化代碼的任務。該領域的早期工作采用序列到序列（sequence-to-sequence）模型，并在對齊數據上進行訓練。例如，文獻[126]通過將Mizar形式陳述“非形式化”（informalizing）來構建數據集，用于訓練翻譯模型。為應對對齊語料稀缺的問題，文獻[125]隨后探索了基于循環一致性損失（cycle-consistency losses）的無監督方法：模型在無需顯式監督的情況下，通過在非形式與形式領域之間來回翻譯并重建原始陳述來學習映射關系。

大語言模型（LLMs）的出現從根本上改變了這一范式。研究表明，現成的LLMs通過少樣本提示（few-shot prompting）即可生成合理的形式化結果[3, 8, 46, 135]。尤為關鍵的是，文獻[135]觀察到一種不對稱性：對模型而言，將形式代碼翻譯為自然語言（即“非形式化”）遠比反向操作（即形式化）更容易。這一洞見催生了大規模合成數據集的構建——研究者利用LLMs對龐大的形式庫（如mathlib4）進行非形式化，從而生成高質量的對齊語料，用于訓練專用的自動形式化器[48, 66, 87, 90]。

近期工作聚焦于提升這些系統的質量與語義根基（grounding）。Herald [48] 提出了一種分層非形式化策略，該策略尊重mathlib庫的依賴圖結構：通過按拓撲序翻譯聲明，確保在翻譯依賴定理時，其前提概念的自然語言描述已可用。Herald還通過基于策略（tactic-based）的狀態合成進一步擴充數據，在miniF2F驗證集上實現了超過96%的準確率。為增強語義根基，RAutoformalizer [87] 引入檢索機制，將生成的代碼錨定于已有的形式化聲明之上。針對研究級數學中常見的“缺失概念”問題，文獻[122]提出了Aria——一個基于LLM的智能體系統。

更一般地，基于LLM的智能體（agent）指一類通過與環境顯式交互循環運行的系統：它維護中間狀態，基于觀測進行推理，執行多步規劃，并據此選擇行動。這些行動可包括調用外部工具，如語義檢索、符號推理模塊或代碼合成組件，而環境反饋則用于指導后續決策。此類智能體設計能夠將復雜任務分解為結構化的子任務，并支持超越單次生成的迭代優化[123]。在此框架下，Aria將非形式陳述分解為概念依賴圖；若某概念在mathlib庫中缺失，該智能體會通過語義搜索與合成，自底向上遞歸地定義該概念，從而有效處理數學術語中的“長尾”現象。

評估與驗證
自動形式化的評估并非易事。盡管人類專家評審是黃金標準，但其不可擴展。因此，核心挑戰在于開發自動化的正確性度量方法：

• 有參考真值（With Ground Truth）：當存在參考形式陳述時，正確性應通過邏輯等價性（而非簡單的字符串匹配）來評估。例如，BEq [87] 利用神經定理證明器檢驗生成陳述與參考真值是否可相互推導。類似等價性檢驗方法也在[88, 101]中被探討。
• 無參考真值（語義驗證，Semantic Verification）：在缺乏參考形式陳述的情況下，需驗證語義正確性——即形式代碼是否忠實捕捉了非形式陳述的意圖。一種樸素方法是“回譯”（back-translation）：讓LLM將代碼再翻譯回英文進行比對[48, 143]。然而，這種方法容易出錯，因為LLM可能忽略細微的邏輯差異。為緩解此問題，文獻[139]提出了Mathesis——一個細粒度評估框架。Mathesis將陳述分解為假設與結論，分別評估各組成部分的一致性，并通過模糊積分（fuzzy integral）聚合得分，以嚴格排除不一致情況。為進一步輔助驗證，Aria [122] 通過檢索每個形式術語的詳細元數據（類型、取值、非形式描述）來豐富上下文，從而支持更準確的語義判斷。

可靠的驗證器不僅對評估至關重要，還可作為強化學習（RL）中的關鍵獎勵模型，形成一個反饋閉環，持續提升自動形式化的性能[63, 90, 139]。

注：本節聚焦于陳述的自動形式化。而證明的自動形式化——即不僅翻譯定義，還需轉換邏輯推理步驟——與自動定理證明密不可分。因此，我們將在下一節關于證明生成的討論中一并闡述證明的自動形式化。

3.3.3 自動定理證明
形式系統中的自動定理證明旨在為形式化陳述生成有效的證明。基于深度學習的方法大致可分為兩類：單模型方法（single-model approaches） 和 智能體方法（agentic approaches）。單模型方法又可進一步細分為證明步驟生成（proof step generation） 與完整證明生成（whole-proof generation）。

證明步驟生成（Proof Step Generation）

證明步驟生成方法將定理證明建模為一個樹搜索問題。在此框架中，搜索樹的每個節點對應一個證明狀態（proof state），每個動作對應應用一個策略（tactic），從而將證明器轉移到新的證明狀態。一旦找到一條通往“無剩余目標”狀態的路徑，即成功構造出證明。圖2展示了此類方法生成的證明樹示例及其最終形式化證明。

該方法的優勢在于可重用性與探索能力。在搜索過程中，證明狀態是可重用的：若新遇到的狀態與先前已探索的狀態一致，則可合并。此外，系統在每一步嘗試多種策略，展現出強大的探索能力。然而，這些方法常因樹搜索的計算開銷而面臨推理速度慢、訓練不穩定，以及對高效交互式工具在訓練和推理階段的高度依賴等問題。

該領域最早的神經方法之一是 Holophrasm [132]，它采用蒙特卡洛樹搜索（MCTS）進行探索，并集成三個神經組件：用于檢索有用定理的相關性網絡、用于提出變量替換的生成網絡，以及用于估計可證性的價值網絡。后續工作大多將策略預測視為分類問題，代表性工作包括 GamePad [62]、DeepHOL [10] 和基于圖的方法 [99]。超越純分類范式，GPT-f [103] 訓練了一個 Transformer 模型，通過條件語言建模目標生成證明步驟，并使用最佳優先搜索（best-first search）構造證明。類似地，文獻[76]引入了超樹（hypertree）搜索結合在線訓練策略，其中策略網絡與評判網絡定期根據重復證明搜索所收集的數據進行更新。

該領域的一大挑戰是大規模形式化數據的稀缺。為應對這一問題，REALProver [110] 提出了一套集成流水線：包含一個陳述自動形式化器（用于翻譯非形式陳述）、一個基于檢索增強的證明器（其策略生成以相關前提為條件），以及一種專家迭代（expert iteration）范式。在該循環中，模型在生成的狀態-策略對上訓練，執行證明搜索，并從成功搜索中迭代收集新的訓練數據。

一個顯著的里程碑是 AlphaProof [64]。AlphaProof 訓練了一個30億參數的證明網絡，可同時輸出策略與價值估計。其訓練流程包括：在3000億詞元上預訓練，在30萬組狀態-策略對上進行監督微調，并在8000萬條自動形式化陳述上進行強化學習。這些形式陳述源自約100萬道非形式問題，其自動形式化模型在（非形式陳述，形式化思維鏈，形式陳述）三元組上訓練，每道問題生成多個不同翻譯。對于特別困難的任務，AlphaProof 還采用測試時強化學習（test-time RL），通過構建并訓練專用課程（curriculum）來適應問題結構。結果，其性能達到IMO銀牌水平。其他值得注意的方法包括 [67, 84, 102, 121, 138, 142]。

完整證明生成（Whole-Proof Generation）

相比之下，完整證明生成方法旨在通過單次前向傳遞生成整個形式化證明（可能輔以內聯注釋）。其主要優勢在于高推理速度，以及在生成過程中無需依賴交互式工具。然而，其探索能力相較于逐步搜索較為有限；它們通常依賴行為克隆（behavior cloning），且由于無法訪問中間證明狀態，更容易出現錯誤累積。

該范式高度依賴數據的質量與數量。由于缺乏先驗的、原則性的數據質量判定方法，評估通常通過模型性能間接進行。為解決數據量問題，文獻[136]提出了一套集成流水線：包括自動陳述形式化、過濾（剔除平凡或錯誤陳述）、陳述證明，以及在所得驗證對上進行迭代訓練。在此基礎上，DeepSeek-Prover-V1.5 [137] 通過構建更豐富的數據集（包含形式代碼前撰寫的非形式證明及內聯非形式注釋）并應用來自驗證器反饋的強化學習（RLVF），進一步提升了性能。采用該范式的其他工作包括 [9, 40, 44, 144, 150]。

智能體方法（Agentic Approaches）

智能體方法代表了從單模型系統向模塊化工作流的范式轉變。這些方法將定理證明分解為若干協調的子任務（如檢索、分解、驗證），并通過結構化工作流將語言模型與外部工具集成。其有效性依賴于三個核心組件：魯棒的檢索系統、LLM 的推理能力，以及模擬數學研究過程的工作流設計。

Draft, Sketch, and Prove (DSP) [68] 是該范式的原型。它首先生成非形式證明，將其翻譯為帶有開放子目標的形式化草稿（sketch），再使用輕量級證明器閉合這些子目標。LEGOProver [120] 在此基礎上擴展，維護一個持久的引理池（lemma pool）。其獨特之處在于，通過維度擴展、關鍵概念識別、參數化和復雜度增強等策略，將已驗證的引理演化為新引理。Hilbert [118] 則通過遞歸子目標分解（由定理檢索引導）將非形式證明轉化為形式草稿。Seed-Prover-1.5 [20] 同樣采用專用草稿模型與專用證明器模型，在研究生級基準 FATE-H/X [69] 上取得優異成績。

針對非形式推理與形式代碼之間的粒度鴻溝，文獻[128]提出了兩階段的“狀態鏈”（Chain of States, CoS）框架。該方法在生成具體轉換策略前，先提取與非形式論證邏輯流對齊的中間形式狀態序列，從而在計算資源受限的情況下顯著降低策略生成的復雜度。

更先進的智能體如 Aristotle [2] 將非形式推理與形式驗證交織進行：它以引理序列為單位起草證明，對其進行形式化并嘗試驗證，并根據反饋迭代優化輸出。Aristotle 結合幾何求解器，在 IMO 金牌水平上取得成果。最后，Gauss 智能體 [95] 展示了人機協作的力量：在專家搭建的腳手架（scaffolding）支持下，僅用三周便完成了強素數定理（strong Prime Number Theorem）的形式化。

這些成果表明，精心設計的智能體工作流能夠有效融合模型的內在推理能力與外部工具，從而在自動定理證明中實現顯著突破。

3.4 數學信息檢索（Mathematical Information Retrieval, MIR）

數學信息檢索旨在從大規模數學文檔集合中檢索數學內容，包括公式、定理和問題解答。與標準文本檢索不同，MIR 必須顯式考慮數學表達式的獨特結構與語義。數學公式本質上是結構化對象，其含義取決于符號的組合方式與關系結構，而非簡單的詞匯重疊。因此，一個有效的 MIR 系統必須應對諸如匹配數學結構與符號模式等挑戰，同時利用周圍的文本上下文來消解歧義并解釋語義。

尤為重要的是，MIR 不僅是供人類用戶使用的搜索工具，更是現代自動定理證明（ATP）和 AI 智能體系統的基礎組件。在 ATP 中，“前提檢索”（premise retrieval）——即從龐大的數學庫中識別出對證明新定理有用的定理、引理或定義——往往是主要瓶頸。隨著數學庫規模擴大至包含數十萬條形式化陳述（如 mathlib4），能否高效檢索到“大海撈針”般的關鍵前提，直接決定了證明器能否成功解決問題，還是因超時而失敗。對于智能體系統而言，MIR 使其能夠訪問長期的數學記憶，從而將推理建立在已確立的知識基礎上，而非憑空生成未經支持的“幻覺”事實。這要求檢索范式從傳統的關鍵詞匹配轉向基于推理的檢索。一個魯棒的 MIR 模型必須理解邏輯蘊含與數學等價性；例如，它應能識別出“方陣行列式非零”這一陳述，是回答“該矩陣列向量是否線性無關”這一查詢所必需的關鍵前提，即便兩者之間沒有任何共享關鍵詞。

根據檢索目標的粒度與查詢的性質，MIR 涵蓋若干緊密相關的任務，主要包括：語義檢索（semantic retrieval）、問答檢索（question-answer retrieval）和前提檢索（premise retrieval）。

語義檢索（Semantic Retrieval）

語義檢索旨在根據數學含義（而非表面相似性）從數學語料庫中識別出數學上等價或高度相關的陳述。該任務源于實際需求，例如在大型數學庫中進行定理搜索。例如，Lean 用戶在構造證明時常需在 mathlib4 中定位相關定理。在此場景中，查詢可以是自然語言或形式代碼，而檢索語料庫通常由 mathlib4 的形式化聲明組成。

為彌合非形式查詢與形式語料之間的鴻溝，LeanSearch? 構建了一個源自 mathlib4 的對齊非形式–形式語料庫，并在聯合表示空間中執行檢索 [47]。該方法實現了跨表示模態的語義匹配，顯著提升了自然語言查詢的檢索效果。除 LeanSearch 外，其他為 mathlib4 開發的語義搜索工具還包括 Moogle?、LeanExplore [7]、LeanFinder [89] 和 LeanDex?。

公式檢索（formula retrieval）是語義檢索的重要子任務，其查詢為數學公式或公式模式，目標是從文檔集合中檢索語義相關的公式。該任務帶來獨特挑戰：表示同一數學概念的公式可能因記號差異或代數性質（如交換律）而在表面形式上大相徑庭；反之，視覺上相似的公式在不同數學語境下可能含義迥異。

傳統公式檢索方法主要基于樹表示，以編碼數學表達式的結構組織。公式被表示為樹，相似性通過子樹或路徑匹配，或通過計算樹編輯距離來定義。廣泛使用的表示包括符號布局樹（Symbol Layout Tree, SLT）[145]，其中節點對應符號，邊編碼上標、下標或鄰接等空間關系；以及算子樹（Operator Tree, OPT）[49]，其內部節點表示運算符，葉節點表示操作數。與 SLT 相比，OPT 抽象掉視覺布局，聚焦于數學運算及其層次關系。

基于樹的檢索算法通常通過匹配子樹或路徑，或計算樹編輯距離來比較公式。例如，Approach0 [154, 155] 將公式表示為算子樹，并以葉到根的路徑作為基本檢索單元：先篩選出路徑與查詢重疊的候選公式，再基于最大公共子樹導出的相似性度量對候選結果重排序。

除傳統符號匹配外，近期研究探索了使用文本嵌入模型進行公式檢索。早期方法通過線性化結構化公式編碼，將其嵌入連續向量空間。例如，TangentCFT [93] 對 SLT 和 OPT 進行深度優先遍歷，將所得元組序列分詞后應用文本嵌入模型獲取公式表示。同期工作通過融合周圍文本上下文來更好捕捉語義 [75, 92]。例如，MathAMR [92] 將公式整合進其語言上下文中：結合抽象語義表示（Abstract Meaning Representation, AMR）圖與 OPT，用對應 OPT 的根節點替換 AMR 圖中的公式節點，并使用 Sentence-BERT 嵌入線性化后的圖結構。

問答檢索（Question-Answer Retrieval）

問答（QA）檢索旨在響應自然語言查詢，檢索數學答案、解釋或支持性文檔。數學問題本質上是多模態的，通常結合自然語言與符號表達式、公式或圖表，候選答案也具有類似結構。因此，數學 QA 檢索中的相關性由語義充分性定義——即答案是否正確且有意義地回應了問題，例如提供有效解法、證明或概念性解釋，而非依賴表面詞匯重疊。

早期數學 QA 檢索主要依賴通用文本檢索技術，如 TF–IDF 和 BM25。盡管可直接應用，但這些方法在數學領域表現不佳，因其依賴精確詞匹配，無法建模數學語言的語義或公式中編碼的結構關系。

隨著深度學習興起，研究轉向基于預訓練 Transformer 的神經檢索模型。常見做法是在大規模數學語料上預訓練并微調 Transformer 模型，以獲得更契合數學語法與語義的表示。例如，MathBERT [100] 在富含公式的語料上預訓練，并引入“掩碼公式子結構預測”等目標，以更好地在上下文中建模數學符號。

基于稠密檢索范式，文獻[104] 在 ARQMath 基準 [94, 146] 上研究了 ColBERT [71] 的應用，通過基于規則啟發式選取負樣本，在數百萬問答對上微調神經檢索器。鑒于符號方法與神經方法的互補優勢，若干混合方法也被提出。例如，Mabowdor [153] 將稠密段落檢索與基于結構感知數學索引的稀疏檢索并行結合，并通過學習加權方案融合輸出。該混合策略在 ARQMath-3 [91] 中表現優異，凸顯了將經典數學結構與神經語義表示相結合在 QA 檢索中的有效性。

前提檢索（Premise Retrieval）

在自動定理證明中，一個核心子問題是前提檢索：給定一個猜想和一個包含大量已有數學陳述的庫，系統需識別出哪些前提可能有助于構造證明。

早期方法主要依賴手工設計的相似性度量與啟發式規則 [61, 96]。此類思想的變體與擴展（包括基于樹的相似性評分）在近期工作中仍被探索 [127]。同時，輕量級機器學習方法（如 k 近鄰或稀疏樸素貝葉斯）也曾用于前提選擇 [32]。

過去十年，深度學習方法在前提檢索中日益普及。代表性早期神經方法是 DeepMath [65]：它分別編碼猜想與候選前提，將所得表示拼接后輸入全連接網絡，預測該前提是否有助于證明該猜想。訓練采用監督方式，利用現有證明——出現在證明中的前提視為正樣本，并通過困難負采樣（hard negative mining）構建信息豐富的負樣本。

后續工作試圖更好地利用邏輯公式的內部結構。例如，FormulaNet [124] 將每個公式表示為源自其語法結構的圖，節點對應常量、變量或量詞，再通過圖神經網絡計算嵌入，組合后輸入分類器估計相關性。

超越成對評分模型，后期研究探索了對整個陳述庫的圖級表示。文獻[43] 構建了一個全局圖，其中節點對應數學陳述，有向邊編碼從證明中提取的前提–結論關系。新猜想的前提選擇被建模為鏈路預測問題，使用圖卷積網絡基于節點的文本與結構特征對潛在邊進行評分。

與此同時，另一研究路線采用基于嵌入的檢索方法：將每條數學陳述視為文本，通過學習的嵌入模型編碼為單個向量，相關性通過嵌入空間中的相似性評估，通常再經學習的重排序階段優化候選集。訓練通常依賴對比目標：將猜想與其證明中出現的前提拉近，同時推遠無關陳述。該方法的代表工作包括 [110, 113, 142]。

3.5 數學發現智能體（Agents for Mathematical Discovery）
隨著大語言模型（LLMs）能力的持續增強，基于 LLM 的智能體也不斷進步，近期多項工作已展現出它們在發現新數學構造方面的潛力。

FunSearch [105] 采用進化方法搜索能夠生成目標構造的程序。對于具備明確定義評估器（evaluator）的問題，FunSearch 利用現成的 LLM 迭代地將低分候選程序演化為高分程序。具體而言，該方法維護一個規模大且多樣化的程序池，并反復提示 LLM 對早期候選程序進行改進。通過這一方法，FunSearch 發現了新的大容量帽集（large cap sets）構造，其結果超越了極值組合學中此前已知的最佳成果。

在此基礎上，AlphaEvolve [98] 采用了更強的 LLM，并將進化過程從單個函數擴展至整個代碼文件，同時支持多指標聯合優化。AlphaEvolve 已在多個問題上取得了改進的構造，包括“最小重疊問題”（Minimum Overlap Problem）和 11 維空間中的“接吻數問題”（Kissing Numbers problem）。

受 AlphaEvolve 啟發的開源實現包括 OpenEvolve [108]、ShinkaEvolve [78] 和 DeepEvolve [86]。這類 AlphaEvolve 風格的智能體特別適用于那些可通過編寫代碼來處理、并能通過明確定義的評分函數進行評估的數學問題，尤其擅長尋找新的數學構造。

4 挑戰與展望
盡管人工智能在數學領域（AI for Mathematics）取得了令人鼓舞的進展，該領域仍面臨一個根本性障礙：當前的人工智能系統，尤其是基礎模型，尚缺乏進行研究級數學所需的深度推理能力。彌合這一鴻溝需要從被動輔助轉向在嚴格“邏輯環境”中的主動學習。這要求加速數學的形式化（或數字化）進程，以提供可自動驗證的反饋，從而迭代式地增強 AI 的推理能力。此外，提升這些能力還需將專業數學知識——從高質量數據構建到專用智能體工作流的設計——深度融入模型開發過程。最終目標是將 AI 無縫整合進數學家的日常實踐中，而這一愿景唯有通過 AI 研究者、工程師與數學界持續、緊密的合作才能實現。我們將在下文總結這些關鍵挑戰與未來方向：

1. 領域專業知識與特征工程：在面向特定問題的建模中，輸入特征的設計往往需要深厚的領域專業知識。人類直覺在選擇具有數學意義的特征以及解釋模型輸出以提煉理論洞見方面仍不可或缺。這一依賴同樣適用于面向發現的智能體（如 AlphaEvolve 類系統），它們依賴精心手工設計的表示和評分函數。因此，開發有效的 AI for Mathematics 必須依靠機器學習研究者與領域專家之間長期、緊密的合作，以確保計算成果能轉化為真正的數學進步。
2. 驗證瓶頸與自動形式化：準確高效的驗證是研究級數學的關鍵瓶頸。自然語言固有的模糊性，加上能夠審核高級證明的專家稀缺，使得人工驗證既緩慢又易出錯。為實現可靠性，數學推理最終必須扎根于形式語言之中，其正確性可由機器機械地檢驗。然而，由于高質量形式數據嚴重匱乏，當前 LLM 的形式推理能力遠落后于其自然語言表現。解決這一“形式數據鴻溝”需要開發魯棒的自動形式化工具，以彌合非形式與形式數學之間的差距。通過為特定子領域構建可靠基礎設施，并支持庫級（repository-level）形式化，我們可加速將自然語言推理轉化為形式證明。這將形成一個良性循環：形式可驗證的反饋可作為高質量訓練信號，進一步提升 LLM 在數學乃至更廣泛領域的推理能力。
3. 形式化中的語義一致性：自動形式化面臨一個微妙挑戰：驗證所生成形式陳述的語義正確性。現有模型常難以判斷回譯后的形式陳述是否忠實捕捉了原始非形式猜想的細微含義。這需要開發細粒度、魯棒的語義一致性驗證器。盡管語義意圖的最終判斷理應保留給人類專家以確保概念準確性，但自動化系統可作為高效的第一道篩選機制。通過大幅減少需人工復核的候選數量，這類系統可在不犧牲嚴謹標準的前提下規模化形式化進程。
4. 超越正確性，邁向理解：形式有效性是數學價值的必要條件，但非充分條件。正如威廉·瑟斯頓（William Thurston）著名指出的 [31]：“數學不是關于數字、方程、計算或算法；而是關于理解。”一個有價值的證明不僅確立真理性，更提供洞見、揭示結構，并貢獻可應用于其他問題的技術。類似地，斯坦尼斯瓦夫·烏拉姆（Stanislaw Ulam）[117] 引述斯特凡·巴拿赫（Stefan Banach）的話：“優秀的數學家看到定理或理論之間的類比，而最杰出者則看到類比之間的類比。”這揭示了一個更深層的真理：證明的價值在于其深化我們對數學圖景概念性把握的能力。因此，未來的 AI 系統必須超越單純驗證，協助發現那些能重塑我們思維、揭示此前不可見聯系的證明。
5. 從啟發式到專家常規流程：盡管獨立的 LLM 是強大的推理引擎，但 AI4Math 的未來在于設計能模擬專業數學家復雜工作流的智能體系統。研究級數學極少是線性演繹；它涉及一個復雜的迭代循環：構造例子、查閱文獻、提出猜想，并根據中間失敗不斷調整證明策略。然而，當前的智能體仍大多通用化。一個關鍵前沿是開發能顯式建模這些專家“常規流程”（routines）的架構，學會以反映研究者認知過程的方式協調工具與策略。這包括使用“計算草圖”（computational sketching）——不僅用代碼生成形式證明，還用于構造數值玩具示例或執行符號推導，以快速驗證或證偽人類直覺。此外，這些智能體可自動化高價值但常被人類忽視的“長尾”任務，如證明重組、條件弱化、以及晦澀已有解法的語義檢索。最終目標不僅是模仿人類工作流，更是優化它們，創造出能以超越人類的系統性與規模探索數學思想空間、攻克難題的智能體。
6. 積極的社區參與：呼應領域專業知識的必要性，AI 推理能力的提升需要數學家的主動介入。除了生成形式數據，社區必須積極探索這些系統，以集體構建對其能力與邊界的心理模型。例如，明確模型在代數操作上是否優于幾何拓撲，對確定 AI 可靠部署的場景至關重要。這不僅要求加速數學知識的數字化以創建可驗證的訓練語料庫，還要求開展“對抗性協作”（adversarial collaboration）以識別邏輯漏洞。通過嚴格刻畫這些優劣勢，數學家可引導開發出不僅統計強大、而且數學上可靠（mathematically sound）的模型。
7. 擁抱 AI 輔助研究：我們必須為一場文化轉變做好準備：AI 將從計算工具演變為研究副駕駛（copilot）。2025 年末陶哲軒（Terence Tao）與 Google DeepMind 合作的工作 [50] 正凸顯了這一轉型。陶哲軒觀察到，盡管這些模型可能仍缺乏真正理解，常常只是“模仿思考”，但它們已能自主發現人類直覺難以企及的數學構造。即使模型產生幻覺或推理有缺陷，其生成看似合理結構候選的能力仍使其成為有效的副駕駛——引導研究者走向富有成果的探索路徑，而將最終的嚴格驗證留給專家。

我們認為，即便 AI 的發散式推理（提出隨機或創造性變體）正確概率較低，只要“驗證杠桿”（verification leverage）足夠高，整體研究效率仍會提升。在許多高等數學領域，生成一個解在計算或認知上代價高昂，而驗證一個候選解則相對迅速。這種不對稱性使研究者可將 AI 作為高吞吐量的候選思想生成器——單次有效洞見所節省的時間，遠超剔除錯誤建議的低成本。

然而，實現這一潛力不僅需要強大的模型，更需要精心設計、易于使用的工具。要促進高參與度，必須通過穩健的軟件設計降低使用門檻。近期框架（如 AlphaEvolve）相比早期原型在易用性上的顯著提升表明：工程質量是決定這些技術能否從實驗性新奇物轉變為全球廣泛采用的標準工具的關鍵因素。

原文鏈接：https://arxiv.org/pdf/2601.13209v1