# 問題工業化命題：從自動證明器到數學研究平台 ## 《AI 時代的科學生產相變：五個未來命題》第二篇 **作者**：Neo.K **機構**：EveMissLab／一言諾科技有限公司 **版本**：v1.0 **日期**：2026-08-02 **文件類型**：未來命題／可反駁猜想論文 **研究狀態**：Conceptual Conjecture / Research-System Hypothesis --- ## 摘要 如果第一篇「證明工業化命題」成立，數學知識生產的下一個自然問題不再只是「AI 能否自動找到更多證明」，而是：**研究問題本身是否會成為可被批量接收、分解、修補、驗證、保存與持續推進的計算對象？** 本文提出「**問題工業化命題**」（Research-Problem Industrialization Conjecture, RPIC）：當 AI 系統具備長時程研究狀態保存、文獻檢索、形式化、猜想修補、反例搜尋、證明搜索、形式驗證、重要性排序與研究歷史管理能力後，數學研究的基本工作單位將逐漸從一次性的「題目—答案」對，轉變為可持續執行的「**研究狀態**」（Research State）。人類提交的不再只是問題文字，而可能是包含定義、背景、證據、限制條件、失敗路線、期望輸出與應用語境的研究物件；AI 平台則將其轉入一個可反覆迭代的 Mathematical Research Runtime。 2026 年已可看到多個早期前兆。Google DeepMind 公開的 Aletheia 數學研究代理能迭代生成、驗證與修訂研究級解答，並被用於數百個開放問題的半自動掃描；OpenAI 的 First Proof 實驗顯示前沿模型已能對研究級問題生成完整候選證明，同時也暴露「長鏈論證即使看似完整仍可能錯誤」的必要外部驗證問題；LeanMarathon、SITA、LEAP 等系統則分別處理長時程自動形式化、抽象結構到具體實例的形式化、以及 agentic formal theorem proving。[1][2][3][4][5] 這些系統尚未構成完整的自動數學研究平台，但它們開始覆蓋本文所描述 pipeline 的不同模組。 本文提出研究狀態模型、問題工業化臨界條件、研究任務分流、Salvageable Structure Extraction、持久研究記憶、形式驗證與重要性排序等概念，並給出可測量指標與失敗條件。本文不預言所有數學問題都會被自動解決；其核心猜想是：**「提出問題」本身將逐漸從一次性人類交流行為，轉變為可被研究基礎設施持續處理的標準化輸入。** **關鍵詞**：AI for Mathematics、研究代理、數學研究平台、自動證明、研究狀態、問題工業化、形式化、猜想生成、反例搜尋、數學研究自動化 --- # 1. 從「解題」到「接管研究狀態」 目前多數 AI 數學互動仍然採取： $$ \text{User Question} \rightarrow \text{Model Response}. $$ 即使模型能產生很長的證明，基本介面依然接近： > 人類提出一個問題，模型回傳一次答案。 然而研究級數學通常不是這種結構。 一個真實研究問題可能包含： - 多套相互競爭的定義； - 已知定理與文獻依賴； - 部分證明； - 已知反例； - 尚未證明的中間引理； - 數值實驗； - 形式化進度； - 歷史上失敗的方法； - 研究者的直覺； - 問題與其他領域的潛在連接。 因此，更合理的研究單位不是： $$ Q=\text{a question string}, $$ 而是： $$ \boxed{ \mathcal R = \text{Research State}. } $$ 本文提出的問題工業化，首先就是從「問題」升級為「研究狀態」。 --- # 2. 當前前兆：不同系統已開始覆蓋研究 pipeline 的局部 ## 2.1 Aletheia：從一次推理轉向反覆研究 Google DeepMind 2026 年公開的 Aletheia 被定位為 math research agent。系統不是只生成一次候選答案，而是反覆： $$ \text{Generate} \rightarrow \text{Verify} \rightarrow \text{Revise}. $$ 官方報告指出，Aletheia 已被用於研究級數學、700 個 Erdős 開放問題的半自動評估，以及若干不同程度的人機協作研究成果。[1][2] 這類系統的重要性，不只在於「解出幾題」，而是顯示研究流程本身開始被表示成可迭代的 agent loop。 --- ## 2.2 First Proof：研究級輸出同時暴露驗證瓶頸 OpenAI 2026 年 First Proof 實驗讓內部模型嘗試十個研究級數學問題。官方後續明確承認，其中一個原本被認為可能正確的解答，在專家與社群進一步檢查後被判定錯誤。[3] 這個例子非常重要，因為它說明： $$ \boxed{ \text{Long Research-Like Output} \neq \text{Reliable Research Completion}. } $$ 因此未來平台不能只是一個超長上下文聊天機器人，而必須內建： - verifier； - counterexample search； - formalization； - provenance； - review state； - confidence separation。 --- ## 2.3 LeanMarathon：長時程形式化需要「研究狀態」而非單次 prompt LeanMarathon 直接指出，研究級長時程 autoformalization 的問題不只在「某個 lemma 很難」，而包括： - statement drift； - dependency tangling； - context decay； - local repair 破壞遠端工作。 因此它使用 evolving blueprint 作為 formal skeleton、自然語言 proof graph 與 shared system of record，並由多代理進行構建、審核、證明與修復。[4] 這正好支持本文的核心判斷： $$ \boxed{ \text{研究級 AI 需要持久研究狀態。} } $$ --- ## 2.4 SITA 與 LEAP：形式化本身也逐漸模組化與代理化 SITA 將形式化過的抽象數學結構當成可重用 template，再將其實例化到具體問題；LEAP 則以 agentic decomposition、informal blueprint 與 Lean compiler feedback 形成形式證明循環。[5][6] 這類工作表明，未來研究平台不必每次從零開始，而可能逐步建立： $$ \boxed{ \text{Reusable Mathematical Research Components}. } $$ 這是問題工業化的重要前提之一。 --- # 3. 問題工業化命題 本文提出： $$ \boxed{ \textbf{Research-Problem Industrialization Conjecture (RPIC)} } $$ > 當 AI 數學系統能以持久研究狀態為核心，將使用者提交的問題、背景、定義、證據、限制與研究歷史轉化為標準化研究物件，並能自動或半自動完成分流、形式化、檢索、反例搜尋、猜想修補、證明探索、驗證、版本管理與價值排序時，數學研究中的「問題處理」將由一次性手工流程逐步轉變為可批量配置、可持續排程與可機器管理的研究基礎設施。 RPIC 並不要求： 1. AI 解決所有問題； 2. 人類退出研究； 3. 平台只接受「高品質」問題； 4. 每個問題都得到證明； 5. 所有形式化都能完全自動完成； 6. AI 自己能可靠判斷所有研究的重要性。 它要求的只是： $$ \boxed{ \text{研究問題可以被持續地機器處理，而不只是被一次性回答。} } $$ --- # 4. 研究狀態：未來平台的真正輸入單位 定義一個最小 Research State： $$ \mathcal R = ( Q, D, K, C, E, F, H, O ). $$ 其中： - $Q$ ：Question / target statement； - $D$ ：Definitions； - $K$ ：Known results / literature context； - $C$ ：Constraints / assumptions； - $E$ ：Evidence / examples / computations； - $F$ ：Formalization state； - $H$ ：History of attempts； - $O$ ：Desired outputs / research objectives。 一個成熟平台接受的便不是： > 「請證明這個。」 而是： $$ \boxed{ \mathcal R_0 \rightarrow \mathcal R_1 \rightarrow \mathcal R_2 \rightarrow \cdots } $$ 研究本身變成狀態演化。 --- # 5. Mathematical Research Runtime 本文將未來可能的平台核心稱為： $$ \boxed{ \textbf{Mathematical Research Runtime (MRR)} } $$ 其最小 pipeline 可以寫成： $$ \text{Ingest} \rightarrow \text{Normalize} \rightarrow \text{Triage} \rightarrow \text{Literature} \rightarrow \text{Formalize} \rightarrow \text{Search} \rightarrow \text{Verify} \rightarrow \text{Rank} \rightarrow \text{Persist}. $$ 但實際上它不是線性流程，而是具有 feedback 的循環： $$ \boxed{ \mathcal R_{t+1} = \Phi( \mathcal R_t, \mathcal E_t, \mathcal V_t, \mathcal L_t ) } $$ 其中： - $\mathcal E_t$ ：新證據； - $\mathcal V_t$ ：驗證結果； - $\mathcal L_t$ ：新文獻／新連接； - $\Phi$ ：研究狀態更新算子。 這與普通聊天介面的關鍵差異是： $$ \boxed{ \text{答案不是 terminal object；更新後的研究狀態才是。} } $$ --- # 6. 平台不應只問「能不能證」，而應先分類問題 對輸入研究狀態 $\mathcal R$ ，平台首先應執行： $$ \operatorname{Triage}(\mathcal R). $$ 候選類別包括： $$ \begin{aligned} &\text{Known Result},\\ &\text{Equivalent to Known Result},\\ &\text{False / Counterexample Found},\\ &\text{Ill-Posed},\\ &\text{Repairable Conjecture},\\ &\text{Novel but Trivial},\\ &\text{Novel and Potentially Interesting},\\ &\text{Open and Currently Unresolved},\\ &\text{Requires External Data / Experiment},\\ &\text{Requires Human Clarification}. \end{aligned} $$ 這點非常重要。 如果一個平台只會： > 收到問題 → 拼命證明， 它仍然不是研究平台。 成熟研究系統應該有權回答： > 這不是值得直接證明的問題，但其中第三個限制條件產生了一個新的可研究子問題。 --- # 7. 「亂搞」也可以成為可處理研究輸入 問題工業化的一個重要後果，是研究平台未必要像學術期刊一樣在入口處就要求使用者已經把問題整理成熟。 假設輸入： $$ \mathcal R_{\text{raw}} $$ 非常混亂，可能包含： - 錯誤猜想； - 已知定理； - 不一致定義； - 過度類比； - 不成熟直覺； - 無關敘述。 平台仍可以執行： $$ \boxed{ \operatorname{SSE} = \text{Salvageable Structure Extraction}. } $$ 輸出： $$ \operatorname{SSE}(\mathcal R_{\text{raw}}) = \text{可保留的研究結構集合}. $$ 例如： $$ \mathcal R_{\text{raw}} \rightarrow \begin{cases} Q_1:&\text{已知問題},\\ Q_2:&\text{錯誤，存在簡單反例},\\ Q_3:&\text{修改條件後成立},\\ Q_4:&\text{似乎形成未見文獻的新問題}. \end{cases} $$ 因此「低品質輸入」和「零研究價值」不再必然相同。 但這同時要求平台具有強力的去重、文獻查核與垃圾輸入管理能力，否則問題工業化也可能變成問題垃圾工業化。 --- # 8. 從 Proof Search 到 Research Routing 傳統自動證明器主要解決： $$ \text{Given }T, \quad \text{find proof of }T. $$ MRR 則更接近： $$ \boxed{ \text{Given }\mathcal R, \quad \text{decide what research operation should happen next.} } $$ 也就是： $$ \mathcal R \rightarrow \begin{cases} \text{Proof Search},\\ \text{Counterexample Search},\\ \text{Literature Retrieval},\\ \text{Definition Repair},\\ \text{Formalization},\\ \text{Computation},\\ \text{Conjecture Generation},\\ \text{Human Review},\\ \text{Archive / Reject}. \end{cases} $$ 因此成熟平台的核心能力之一可能不是 theorem proving，而是： $$ \boxed{ \textbf{Research Routing}. } $$ --- # 9. 自動化程度不應只有「AI 解了／沒解」二元分類 建議定義問題工業化的自主性等級。 ## Level 0：Answer Assistant 人類提出明確問題，AI 回答。 --- ## Level 1：Proof Assistant AI 能協助： - lemma； - formalization； - proof repair； - calculation。 研究控制流仍由人類維持。 --- ## Level 2：Research Task Agent AI 可以針對一個明確研究任務自主： $$ \text{Search} \rightarrow \text{Try} \rightarrow \text{Verify} \rightarrow \text{Revise}. $$ Aletheia 類系統已開始靠近此層。[1][2] --- ## Level 3：Persistent Research Runtime AI 保存 Research State，能跨多次執行： - 管理依賴； - 保存失敗路線； - 自動建立子任務； - 更新文獻； - 長期修復形式化。 LeanMarathon 類 blueprint 已經提供局部技術前兆。[4] --- ## Level 4：Research Portfolio Platform 平台同時管理： $$ \mathcal R^{(1)}, \mathcal R^{(2)}, \ldots, \mathcal R^{(N)}. $$ 自動配置： - compute； - prover； - formalizer； - literature agent； - human reviewers。 問題開始真正「工業化」。 --- ## Level 5：Open Mathematical Research Infrastructure 外部使用者可以上傳新的研究狀態，平台形成持續性的： $$ \boxed{ \text{Problem Marketplace / Research Infrastructure}. } $$ 此時研究不再主要以單篇 prompt 為單位，而以大量並行 research state 為單位。 RPIC 的強版本主要預測 Level 4–5 的出現。 --- # 10. 問題工業化的最小經濟條件 令： $$ C_p(t) $$ 表示把一個新研究狀態推進到「有價值的新狀態」的平均成本。 這個價值狀態可以是： - 找到反例； - 找到文獻等價； - 完成形式化； - 證明一個子引理； - 修正猜想； - 產生新連接； - 完成證明。 令： $$ R_p(t) $$ 表示平台每單位時間能可靠推進的研究狀態數量。 問題工業化需要至少出現： $$ \boxed{ C_p(t)\downarrow, \qquad R_p(t)\uparrow. } $$ 並且此改善不是只靠更多人類研究者手動控制每一條研究線。 也就是 autonomous fraction： $$ A_p(t) = \frac{ \text{AI 自主完成的有效研究操作} }{ \text{全部有效研究操作} } $$ 需要具有顯著增長。 --- # 11. 可測量的研究平台指標 為避免 RPIC 變成不可驗證的未來故事，本文提出下列候選指標。 ## 11.1 Research-State Throughput $$ R_p = \frac{ \text{被實質推進的 research states} }{ \text{time} }. $$ --- ## 11.2 Formalization Fidelity $$ F_f = \Pr( \text{formal target faithfully matches intended statement} ). $$ Lean code 能 compile 並不足夠；形式命題本身必須沒有漂移。 --- ## 11.3 Verified Progress Ratio $$ V_p = \frac{ \text{經獨立驗證的有效進展} }{ \text{平台宣稱的進展} }. $$ --- ## 11.4 Research Repair Rate $$ R_r = \frac{ \text{被成功修補成有意義問題的失敗／錯誤輸入} }{ \text{可修補輸入} }. $$ --- ## 11.5 Novelty Precision $$ P_n = \Pr( \text{標記為 novel 的結果經文獻審核後仍 novel} ). $$ --- ## 11.6 Human Intervention Density $$ H_d = \frac{ \text{human intervention operations} }{ \text{effective research progress} }. $$ 真正的問題工業化預期： $$ H_d\downarrow $$ 但不要求： $$ H_d=0. $$ --- ## 11.7 Time-to-Useful-State $$ T_u = \mathbb E[ \text{從問題上傳到第一次可驗證有效進展的時間} ]. $$ 如果平台成熟， $T_u$ 應顯著下降。 --- # 12. 問題工業化臨界條件 本文不要求存在一個單一精確臨界點，但提出一個候選組合條件。 若存在持續時間區間，使： $$ R_p\uparrow, $$ $$ C_p\downarrow, $$ $$ V_p\ge v_0, $$ $$ P_n\ge p_0, $$ 且： $$ H_d\downarrow, $$ 則可認為研究問題的處理開始從 artesanal / artisanal workflow 轉向 industrializable workflow。 因此強版 RPIC 的核心不是： $$ \text{AI solves everything}, $$ 而是： $$ \boxed{ \text{可靠研究進展的邊際成本下降且可並行擴張。} } $$ --- # 13. 平台真正稀缺的可能不是算力，而是研究價值判斷 當研究問題可以大量上傳後，立刻出現新瓶頸： $$ \boxed{ \text{Which problems deserve compute?} } $$ 假設一天收到： $$ 10^6 $$ 個研究狀態，平台不可能無差別分配相同資源。 因此需要： $$ \operatorname{Priority}(\mathcal R) $$ 候選因素： $$ \begin{aligned} I(\mathcal R)=f(&\text{Novelty}, \text{Difficulty}, \text{Generality}, \text{Connectivity},\\ &\text{Application}, \text{Verification Cost}, \text{Expected Information Gain}). \end{aligned} $$ 於是第一篇的「Mathematical Significance Engine」在第二篇變成平台核心 scheduler。 這代表： > 問題工業化不只會工業化「求解」，還會迫使數學建立新的研究資源分配制度。 --- # 14. 研究平台需要完整 provenance，而不是只輸出最後答案 每個 Research State 應保存： $$ \boxed{ \text{Provenance Graph}. } $$ 至少記錄： - 哪個模型提出哪個 lemma； - 哪個文獻提供哪個已知結果； - 哪次反例搜索推翻哪個版本； - 哪次 formalization 改寫了 statement； - 哪個 verifier 接受或拒絕哪個 proof； - 哪個 human reviewer 修改哪個關鍵步驟。 可表示為： $$ G_R=(V_R,E_R). $$ 其中節點為： - claim； - proof； - counterexample； - definition； - source； - experiment； - review decision。 邊表示依賴與修正關係。 如果未來數學大量 AI 化，這種 provenance 可能比傳統「一篇 PDF 的作者列表」更重要。 --- # 15. 問題工業化不等於問題價值民主化 一個容易誤判的樂觀版本是： > 人人都能把問題丟給 AI，所以任何人的數學想法都能獲得同等研究機會。 這未必成立。 因為平台仍然存在： $$ \text{Compute Scarcity}, $$ $$ \text{Verification Scarcity}, $$ $$ \text{Human Attention Scarcity}. $$ 因此未來可能反而出現： - priority algorithms； - reputation systems； - paid compute tiers； - public-interest queues； - open-problem bounties； - domain-specific research pools。 所以問題工業化是一個基礎設施命題，不等於所有問題會獲得相同待遇。 --- # 16. 最大風險之一：Research Spam 如果提交研究狀態的成本接近零： $$ C_{\text{submit}}\rightarrow 0, $$ 則可能產生： $$ R_{\text{spam}}\gg R_{\text{valuable}}. $$ 平台必須區分： - genuine exploratory weirdness； - duplicate conjectures； - automated nonsense； - adversarial workload； - citation laundering； - AI-generated theorem spam。 因此 RPIC 若成立，研究平台還需要： $$ \boxed{ \text{Research Input Governance}. } $$ 這是「問題工業化」和普通 chatbot 平台非常不同的地方。 --- # 17. 為什麼形式驗證仍不是完整終點 即使平台能生成 Lean proof： $$ \operatorname{KernelCheck}(P)=1, $$ 仍至少需要檢查： 1. statement fidelity； 2. assumptions； 3. imported axioms； 4. model correspondence； 5. novelty； 6. mathematical significance。 因此： $$ \boxed{ \text{Verified Proof} \neq \text{Completed Research Object}. } $$ LeanMarathon 將 target fidelity 放在長時程 autoformalization 的核心，就是因為局部證明成功不代表整體 formal target 沒有漂移。[4] First Proof 中錯誤候選解答的事例則提醒：自然語言長鏈研究輸出不能依賴模型自信直接驗收。[3] --- # 18. RPIC 的證偽條件 以下情況若長期成立，會削弱甚至否證強版 RPIC。 ## 18.1 長時程研究無法可靠維持 如果： $$ \text{context drift} + \text{dependency errors} + \text{state corruption} $$ 隨研究長度快速失控，Research State 無法穩定保存，則平台化會受限。 --- ## 18.2 驗證成本與生成成本同步爆炸 如果每新增一單位候選研究輸出，都需要更多人類專家時間： $$ C_{\text{verify}} \propto R_{\text{generate}}, $$ 則無法形成真正 industrial scaling。 --- ## 18.3 Novelty Search 無法可靠自動化 如果文獻分散、符號不一致、結果等價性難判斷，使 AI 長期無法可靠回答： > 這是不是已知結果？ 則平台會累積巨大重複研究。 --- ## 18.4 研究價值無法從局部訊號估計 若重要性高度依賴數十年後的歷史作用，任何即時 significance engine 都可能偏差巨大。 這不否定平台存在，但可能限制自動 priority allocation。 --- ## 18.5 人類仍必須細緻控制每一條研究線 若 $H_d$ 長期無法下降，系統只是更好的研究工具，而不是問題工業化平台。 --- # 19. 弱版、中版與強版命題 為了避免全有全無的預測，RPIC 可以拆成三個版本。 ## 19.1 弱版 RPIC 大量數學研究任務被標準化為 machine-processable research states。 這個版本目前已出現明顯前兆。 --- ## 19.2 中版 RPIC 研究平台可以在少量人類監督下，長時程維持並推進大量 research states。 目前尚未普遍實現，但 Aletheia、LeanMarathon 等方向已開始觸及其局部結構。[1][4] --- ## 19.3 強版 RPIC 公開平台可以接受大規模外部研究問題，並以低邊際成本自主完成： $$ \text{Triage} + \text{Research} + \text{Verification} + \text{Ranking} + \text{Persistence}. $$ 這仍然是明確的未來猜想。 --- # 20. 與第一篇「證明工業化命題」的關係 第一篇關心： $$ \boxed{ R_n>R_h } $$ 造成 proof abundance 與人類注意力瓶頸。 第二篇則問： > 如果證明與研究操作越來越廉價，誰來管理海量問題？ 因此： $$ \text{Proof Industrialization} \rightarrow \text{Problem Industrialization} $$ 並非邏輯必然，但具有清楚的制度性壓力。 證明能力越能批量配置，就越需要把： $$ \text{Research Problems} $$ 本身轉變為： $$ \boxed{ \text{Schedulable Research Objects}. } $$ --- # 21. 對第三篇的橋接：平台為何會開始「主動配送數學」 問題工業化之後，平台將累積： $$ \mathcal R^{(1)}, \mathcal R^{(2)}, \ldots, \mathcal R^{(N)}. $$ 它不只看到單一問題，還能看到不同問題之間反覆出現的： - state-transition structures； - symmetries； - optimization patterns； - topological invariants； - algebraic identities； - probabilistic structures； - graph motifs。 因此下一個自然問題變成： > 當平台同時處理足夠多領域的研究狀態，它是否會開始主動發現「這個領域不知道自己需要另一個領域的數學」？ 這導向第三篇： $$ \boxed{ \text{數學反向輻射命題} } $$ 即從： $$ \text{Science Pulls Mathematics} $$ 逐漸加入： $$ \boxed{ \text{Mathematics Pushes Science}. } $$ --- # 22. 結論 本文提出的「問題工業化命題」不是預測未來每個人都能按一下按鈕解決任意數學問題。 其較精確的主張是： $$ \boxed{ \text{數學問題會逐步變成可由持久 AI 研究基礎設施管理的計算物件。} } $$ 研究的基本單位可能從： $$ \text{Question} \rightarrow \text{Answer} $$ 轉為： $$ \boxed{ \text{Research State} \rightarrow \text{Research State}' \rightarrow \text{Research State}'' \rightarrow\cdots } $$ 而平台真正的工作也從： $$ \text{Solve this theorem} $$ 升級為： $$ \boxed{ \text{Decide what should happen next to this research state.} } $$ 這將使「問題提出、問題修補、問題分流、問題保存、問題排序」本身逐漸成為數學研究基礎設施的一部分。 若這種轉變發生，第一篇的證明工業化便不再只是「更多 AI 證明」；它將開始形成一個可以持續接收研究問題、分配計算資源、驗證結果並保存研究歷史的 Mathematical Research Runtime。 而一旦這個 runtime 同時觀察大量不同領域的研究結構，下一個相變就不再只是「解更多題」。 它可能開始主動問： $$ \boxed{ \text{這個數學結構，還能被送去哪裡？} } $$ 這正是下一篇「數學反向輻射命題」的起點。 --- # 參考資料 [1] Tony Feng et al., **Towards Autonomous Mathematics Research**, arXiv:2602.10177, 2026. https://arxiv.org/abs/2602.10177 [2] Google DeepMind, **Gemini Deep Think: Redefining the Future of Scientific Research / Accelerating mathematical and scientific discovery with Gemini Deep Think**, 2026. https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/ [3] OpenAI, **Our First Proof submissions**, 2026-02-20. https://openai.com/index/first-proof-submissions/ [4] Yuanhe Zhang et al., **LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization**, arXiv:2606.05400, 2026. https://arxiv.org/abs/2606.05400 [5] Chenyi Li, Wanli Ma, Zichen Wang, Zaiwen Wen, **SITA: A Framework for Structure-to-Instance Theorem Autoformalization**, AAAI 2026. https://ojs.aaai.org/index.php/AAAI/article/view/38997 [6] Po-Nien Kung et al., **LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks**, arXiv:2606.03303, 2026. https://arxiv.org/abs/2606.03303 --- ## 系列位置 1. **證明工業化命題**：當數學真理的生成速度超過人類理解速度。 2. **問題工業化命題**：從自動證明器到數學研究平台。 ← 本篇 3. **數學反向輻射命題**：從 Science Pulls Mathematics 到 Mathematics Pushes Science。 4. **需求驅動新數學命題**：當科學問題開始反向生成數學。 5. **後學科科學耦合命題**：AI 是否會重寫科學的領域邊界。