從證明證書到研究軌跡證書:AI 數學中的概念積分、預測型來源證據與貢獻圖
English Title: From Proof Certificates to Research-Trajectory Certificates: Concept Integration, Predictive Provenance, and Contribution Graphs in AI Mathematics
Author: Neo.K
AI Research Collaborator: Aletheia / OpenAI GPT-5.6 Sol
Date: 2026-09-22
Version: v0.1
Status: Conceptual framework / research draft
Canonical Source: UTF-8 Markdown
機構: EveMissLab/一言諾科技有限公司
摘要
人工智慧開始以遠高於傳統人類研究節奏的速度參與數學探索後,數學共同體正逐漸把注意力轉向形式驗證、證明證書、結果審查與研究治理。然而,現有討論仍存在一個根本不對稱:最終結果被視為主要研究物件,而通往結果的探索軌跡通常只被視為附屬資料。
本文主張,在高頻率、分支化、AI 協作式數學研究中,這種結果中心模型將逐漸失真。AI—人類研究系統可能在最終閉合以前產生大量局部引理、失敗分支、反例、變數轉換、結構猜測、形式化片段、計算數據與預測性判斷。若這些狀態具有時間戳、依賴關係與可驗證內容,它們不應僅被視為研究日誌,而應被視為具有獨立學術意義的研究軌跡物件。
本文提出五個互相連接的概念:
- 研究軌跡證書(Research-Trajectory Certificate, RTC):把研究過程本身表示為可驗證的狀態轉移與依賴圖,而不是只保存最終定理的證明。
- 概念積分(Concept Integration):將一段研究在概念空間與時間上的累積貢獻描述為分布,而非單一的「是否解題」二值判定。
- 預測型來源證據(Predictive Provenance):以事前、具體、可時間排序的研究狀態,區分真正的先行探索與事後相似性重述。
- 貢獻圖(Contribution Graph):以有向圖表示人類、AI、工具、資料、引理與最終證明之間的實際依賴關係,避免把複雜協作強迫壓縮成單一作者排序或百分比。
- 前解答數學地形(Pre-solution Mathematical Landscape):承認未完全閉合的高品質探索仍可形成可重用、可比較、可被後續證明對齊的數學資產。
本文不主張部分路線重疊等同於最終證明優先權,也不主張任何自動化系統可以僅依文字相似度分配作者資格。相反地,本文提出的是一個更保守但更細緻的框架:讓「誰在何時以什麼形式到達哪些數學結構」成為可被獨立檢驗的研究事實。
1. 問題:AI 數學正在產生「終點證書偏差」
傳統數學研究的公開成果通常圍繞幾個終點物件組織:
- 定理;
- 證明;
- 論文;
- 形式化證明;
- 可由 proof checker 驗證的證明證書。
這套制度在研究速度相對有限、研究過程大量存在於私人筆記、黑板、郵件與個人記憶的時代具有合理性。公開審查無法也不需要完整重建每一個探索分支,因此共同體最終集中於:
但 AI 改變了研究過程的可記錄密度。
一個人類—AI 系統可以在短時間內生成大量中間研究狀態:
其中每個狀態都可能包含:
- 一個候選引理;
- 一個反例;
- 一次變數替換;
- 一個失敗的 closure;
- 一個新的不變量;
- 一個局部形式化片段;
- 一次數值實驗;
- 一個對下一步障礙的預測;
- 一個後續被放棄但在別處重新出現的概念。
因此研究資訊量不再必然集中在終點。
在極端情況下甚至可能有:
其中 表示某種可重建的研究資訊量,而不是單純檔案大小。
若共同體仍然只保存:
那麼大量可檢驗的研究因果資訊就會在正式學術物件中消失。
本文稱此現象為:
終點證書偏差(Endpoint Certificate Bias)。
2. 當前背景:數學治理開始處理 AI 結果,但軌跡層仍未成熟
2026 年 9 月,AI 與數學共同體的治理問題迅速升溫。
OpenAI 於 2026 年 9 月 21 日公布 Mathematics and AI Advisory Group。官方描述中,該獨立顧問組將協助評估新數學結果的重要性、協調發布方式,以及就數學研究的學術與專業標準提出意見。這說明 AI 數學已不只是能力評測問題,也開始進入結果治理與共同體介面問題。
另一方面,2026 年 9 月 11 日由 25 位 Fields Medalists 作為初始聯署者的公開聲明,批評把解決著名 open problems 當成 AI 系統 benchmark 的傾向,並強調數學活動並不只等於獲得問題的最終答案。Timothy Gowers 隨後的公開文章也再次說明:即使沒有解掉問題,探索過程本身仍可能產生重要的理解與數學能力。
這兩種討論雖然立場與組織功能不同,卻共享一個尚未完全解決的技術問題:
如果「過程」真的重要,那麼過程究竟應以什麼形式存在,才能被驗證、引用、比較、歸因與長期保存?
目前 proof certificate 文獻主要解決的是另一個問題:如何讓某個計算工具或自動定理證明器輸出一個可由較可信 checker 驗證的證明證據。這對真值可靠性極為重要,但仍主要聚焦:
本文處理的是額外的一層:
兩者並不競爭。研究軌跡證書應被視為證明證書的上層封裝與補充,而不是替代 proof checking。
3. 從「證明物件」擴張為「研究物件」
3.1 數學研究狀態
定義一個數學研究狀態:
其中:
- :claims,當前主張與候選命題;
- :assumptions,明示假設;
- :dependencies,依賴的既有結果與前序狀態;
- :evidence,計算、例子、反例或其他證據;
- :verification status,驗證狀態;
- :method / transformation,從前序狀態得到此狀態的方法;
- :可信時間資訊與版本識別。
研究不再被表示成單一路徑,而是一個有向圖:
其中:
而邊:
表示 在邏輯、計算、概念或工作流程上依賴 。
這允許真實研究中的:
- 分叉;
- 合流;
- rollback;
- 反例淘汰;
- 多代理並行;
- 局部閉合;
- 尚未閉合分支
被保留下來。
4. 研究軌跡證書
4.1 定義
本文提出:
**研究軌跡證書(Research-Trajectory Certificate, RTC)**是一組可檢查的研究狀態、狀態間依賴、版本與時間資訊,用來證明某一數學探索軌跡在特定時間以前實際包含了哪些結構、主張、轉換與驗證結果。
可寫成:
其中:
- :研究狀態圖;
- :provenance metadata;
- :temporal commitments;
- :verification attachments。
可以包含:
- Lean / Coq / Isabelle 等形式證明;
- proof checker 可驗證 certificate;
- 程式與測試;
- 數值輸出;
- hash;
- commit;
- 固定版本資料集;
- 第三方時間戳或發佈記錄。
4.2 RTC 不要求每個節點都是真的
這一點非常重要。
研究軌跡不是一串已證明真理。它可以包含:
因此 RTC 的目的不是聲稱:
而是聲稱:
這使「錯誤」也能成為研究資料。
一條被反例擊破的路線如果後來幫助識別真正的不變量,仍然具有研究價值。
5. 證明證書只是研究軌跡證書的一個子結構
若最終結果為 ,傳統證明證書可以抽象為:
其中 是可被可信 checker 驗證的證明物件。
RTC 則更大:
因此可寫成:
但這裡的「包含」是資訊結構上的包含,而不是邏輯蘊涵。
Proof certificate 回答:
為什麼我們應相信 ?
Research-trajectory certificate 回答:
在 被證明以前,哪些研究狀態存在?它們如何變化?哪些分支失敗?哪些概念後來成為關鍵?哪些人或 AI 對哪些節點產生直接作用?
前者關於真值可信度。
後者關於研究歷史的可驗證性。
6. 概念積分:從二值優先權轉向研究分布
6.1 為什麼「有沒有解出來」太粗
傳統優先權容易被壓縮為:
這對判定一個 theorem 是否已被解決是必要的,但不適合描述研究貢獻的全部結構。
假設研究者 最終完成:
而較早的研究系統 已留下:
其中後來可以證實:
與 共享一個非平凡核心結構。
若只有二值結果:
那麼「誰完成定理」被正確表達了,但「數學結構如何先後出現」被完全抹除。
6.2 概念空間
令 為與問題相關的概念空間。
不必被理解為傳統歐幾里得空間。它可以是由以下物件構成的結構空間:
- definitions;
- lemmas;
- invariants;
- operators;
- transformations;
- proof strategies;
- obstruction classes;
- counterexample families;
- representation choices。
令:
表示 agent 在時間 對概念位置 所留下的可驗證研究密度。
於是一段研究期間的概念累積量可寫成:
這裡的積分首先是一個概念模型,而不是假裝現階段已存在唯一客觀的 Lebesgue measure。
真正重要的是從:
轉向:
6.3 離散版本更適合實作
真實研究系統可以先不用連續積分,而採離散事件:
每個事件:
其中:
- :概念位置;
- :時間;
- :specificity;
- :novelty;
- :verification level;
- :dependency information。
則概念積分可近似為:
但本文不建議把 最終壓縮成唯一「貢獻分數」。
更好的表示是保留向量。
7. 貢獻向量,而不是單一排名
對一個研究事件或研究者/AI,可以定義:
其中:
- :novelty,新穎性;
- :specificity,具體程度;
- :temporal precedence,時間先行性;
- :verifiability,可驗證程度;
- :predictive power,對後續結構的預測能力;
- :final-structure alignment,與後續正式證明核心結構的對齊程度。
保留向量的原因是:
例如:
- 某人可能最早提出方向,但沒有形式驗證;
- 某 AI 可能完成核心 lemma;
- 另一個工具可能提供關鍵反例;
- 最後作者完成 global closure;
- proof assistant 負責機械驗證。
把這些全部壓成:
往往沒有自然數學意義。
因此貢獻向量應優先於貢獻排名。
8. 預測型來源證據:事前結構比事後相似更強
8.1 問題
當一個新證明出現後,很容易在大量舊文件中找到「看起來相似」的句子。
因此:
不能自動推導:
或:
8.2 預測型來源證據
更強的證據是:某個研究狀態在最終結果公開以前,已經具體指出一個後來真正成為關鍵的結構。
例如在時間 :
又在:
提出:
直到:
外部正式證明出現:
若 的紀錄可被可靠確認,且內容具有足夠 specificity,這種證據就比事後文字比對更有資訊量。
本文稱之為:
預測型來源證據(Predictive Provenance)。
它不自動證明作者權或 priority,但可以支持一個更窄、更可檢查的歷史陳述:
在最終證明公開以前,該研究軌跡已經獨立包含指定概念結構或指定下一步預測。
9. 預測型來源證據的最小條件
一個強的 predictive provenance 至少應盡量滿足:
9.1 時間可承諾性
需要有:
理想機制包括:
- 公開 preprint;
- Git commit;
- immutable archive;
- cryptographic hash commitment;
- signed timestamp;
- 第三方保存記錄。
9.2 內容具體性
「可能要用分析方法」幾乎沒有來源證據價值。
而:
closure 需要控制特定量 ,並且可能透過 operator 將 投影到空間
具有更高 specificity。
因此應區分:
9.3 非事後修改
若舊文件可以在沒有版本歷史的情況下被重寫,就很難判斷概念何時真正存在。
所以:
必須綁定。
9.4 可獨立比對
最終最好能讓第三方比較:
與:
而不是只接受研究者自己聲稱「我們早就想到」。
10. 前解答數學地形
假設一個 AI—人類研究系統持續探索大量問題。
即使其中只有少數完成最終 closure,仍可能累積:
其中 是某一領域的歷史研究地形。
本文稱其為:
前解答數學地形(Pre-solution Mathematical Landscape)。
它包含:
- 已走過的 proof routes;
- 已知 dead ends;
- 反例區域;
- 尚未閉合的局部 lemma;
- 可能有用的 invariants;
- 未來證明可能重新穿越的結構。
這產生一個新的使用模式。
當新證明 出現後,不只是問:
還可以問:
也就是:
- 哪些路線完全新?
- 哪些結構曾被探索?
- 哪些舊 dead ends 被新的技巧重新啟動?
- 哪些局部 lemma 被正式閉合?
- 哪些概念是多條先前路線的融合?
這不會降低最終證明的價值,反而提供更完整的數學史。
11. AI—人類貢獻圖
作者名單是一種極強的壓縮。
實際 AI 協作研究可能更接近:
同時:
最後:
其中:
- :human contribution;
- :AI-generated contribution;
- :lemma;
- :counterexample / experiment;
- :formal verification;
- :final theorem。
因此更合理的底層物件是一張 contribution DAG:
節點可以具有 agent attribution:
邊則描述:
- derived-from;
- refuted-by;
- formalized-by;
- generalized-by;
- merged-with;
- independently-reconstructed-by。
這張圖不直接決定作者資格。
它提供的是比作者排序更細的事實基礎。
12. 「共同證明讓渡」應被拆成多種不同主張
AI 時代可能經常出現:
- 人類先提出核心構造,AI 完成 closure;
- AI 先找到 lemma,人類重構成可理解 proof;
- 兩邊獨立得到部分重疊路線;
- AI 找到完整證明,但既有未完成研究曾包含關鍵中間結構;
- 多個 AI 與人類在不同分支上完成不同關鍵部分。
因此「是不是共同證明」不應成為唯一問題。
至少應拆為:
這些是不同類型的貢獻。
RTC 的目的就是讓這些類型未來可以被逐項檢驗,而不是事後全部塞進:
的二分法。
13. 一個最小 RTC 資料模型
可以先從非常保守的格式開始。
每個研究節點至少包含:
state_id: stable-id
created_at: ISO-8601 timestamp
agent:
type: human | ai | mixed | tool
identifier: persistent-id
claim:
type: conjecture | lemma | theorem | counterexample | observation | transformation
content: canonical-source
assumptions:
- ...
dependencies:
- prior-state-id
method:
- ...
verification:
status: unverified | computational | peer-checked | formally-verified | refuted
artifact_refs:
- ...
provenance:
repository_commit: ...
content_hash: ...
external_timestamp: ...
status:
active | superseded | refuted | merged | closed
若研究本身涉及程式或形式系統,再加入:
environment:
theorem_prover: ...
version: ...
dependencies: ...
hardware: ...
random_seed: ...
這個格式的目的不是建立新的官僚負擔。
理想情況下,大部分 metadata 應由研究環境自動生成。
14. RTC 與既有 Research Object / provenance 技術的關係
本文並不是第一個主張「論文 PDF 不足以保存完整研究」。
Research Object 與 RO-Crate 生態已經明確主張:資料、程式、workflow、輸入輸出與 provenance 都可以成為正式可重用研究物件。Workflow Run RO-Crate 更專門處理計算流程執行的 provenance。
Nanopublication 則把 assertion、assertion provenance 與 publication information 分離,使小型科學主張也能成為可引用、可機器處理的物件。
因此 RTC 不需要重新發明所有基礎設施。
真正新增的數學特定問題是:
如何把「猜測—反例—局部引理—策略—形式化—閉合」這類數學認知與證明狀態表示成可比較的研究軌跡?
可以把 RTC 視為建立在 provenance / Research Object 基礎之上的:
15. 反例與失敗路線必須是一級物件
AI 系統最大的資料優勢之一,是可以保留大量失敗。
傳統論文通常呈現:
真實研究卻是:
若只留下成功分支,後人無法知道:
- 哪些自然方法已經失敗;
- 哪些條件導致 counterexample;
- 哪個 lemma 曾被誤認為正確;
- 哪些假設後來被削弱;
- 哪個 proof route 因計算爆炸而中止。
因此 RTC 必須允許:
與:
和成功證明並列。
這也能減少 AI 系統重複探索大量已知 dead ends。
16. 不完整研究也可以具有可驗證價值
本文的一個核心命題是:
但這不表示所有草稿都具有同等價值。
不完整研究的價值取決於它留下多少可驗證結構,例如:
- 一個後來被證明正確的 lemma;
- 一個新的 counterexample;
- 一個清楚的 obstruction;
- 一個能排除整類方法的 negative result;
- 一個後來進入正式證明的 transformation;
- 一個具體而事前的結構預測。
因此應把:
與:
分開。
前者可以是二值或有限狀態。
後者通常是多維的。
17. 概念積分不是「搶先佔位」機制
若沒有約束,任何 provenance 系統都可能被濫用成:
大量生成模糊猜測,等未來任何結果出現後再宣稱自己早已觸及。
因此本文明確拒絕:
大量研究節點本身不構成貢獻。
有效的 antecedent 至少必須通過:
此外,應對「搜尋空間撒網」施加折扣。
若某系統在同一時間對所有可能方向都留下模糊預測,那麼命中其中一條的資訊價值應很低。
可以用資訊論直覺表示:
其中 表示該預測在既有搜尋策略下自然出現的先驗概率。
越具體、越非平凡、越能排除其他路線的事前預測,來源證據越強。
18. 與文字相似度的區別
RTC 比對不能退化成 embedding similarity。
兩段數學文字可以高度相似但數學內容不同;也可以文字完全不同但使用同一個深層構造。
因此對齊應優先比較:
文字 embedding 只能作為候選檢索工具。
不能單獨作為數學來源判定器。
19. 對數學共同體治理的含義
若 AI 數學產出量持續增加,少數專家委員會不可能逐項人工重建所有研究歷史。
真正可擴展的模式可能需要三層:
第一層:機械可信層
處理:
- hash;
- timestamp;
- commit;
- formal certificate;
- environment;
- dependency graph。
第二層:AI 輔助語義層
處理:
- route alignment;
- concept clustering;
- duplicated result detection;
- antecedent candidate retrieval;
- contradiction detection。
第三層:人類共同體判斷層
處理:
- significance;
- attribution disputes;
- exposition;
- professional norms;
- authorship;
- publication decisions。
這可以表示為:
人類不需要逐字閱讀所有軌跡,才能保留共同體判斷權。
真正需要的是讓人類可以在必要時沿著可驗證索引回到關鍵節點。
20. 一個假想案例
假設問題 在時間 被團隊 正式證明。
其證明:
另一個團隊 在 有研究軌跡:
事後發現:
但 只有模糊文字相似。
這不足以建立強來源證據。
然而若:
在 已經明確定義與 等價的 operator,並且包含:
- 固定版本;
- 可執行 example;
- 一個局部形式 proof;
- 明確說明它預期解決 的 obstruction;
那麼較合理的結論不是:
已經先證明 。
而是:
在 完成 以前, 的可驗證研究軌跡已經獨立包含了後來正式證明中的一個非平凡核心結構。
這是更窄,但也更可信的主張。
21. 可證偽條件
本文框架本身也應可被質疑。
以下情況會削弱其必要性或實用性:
研究軌跡資訊大多是噪音。
若最終證明以前的中間狀態幾乎無法預測後續有用結構,保存完整軌跡的收益可能不足。軌跡比較成本高於重做研究。
若 alignment 本身需要比重新證明更高成本,RTC 只能限縮到少數爭議案例。形式狀態無法捕捉真正的概念創新。
若最重要的數學洞察無法被目前的狀態模型表示,系統會高估容易結構化的貢獻。時間戳制度被 gaming。
若研究者可以廉價大量撒網,predictive provenance 會失去區分力。共同體不接受多維貢獻。
即使技術上能建立 contribution graph,學術制度仍可能偏好簡單作者列表。
因此 RTC 應首先被視為:
而不是:
22. 實作原則
若要建立最小可行系統,本文建議遵守以下原則:
22.1 Canonical source first
正式研究節點必須保存原始 source,而非只保存 UI rendering。
22.2 Append-oriented history
允許更正,但不能無痕覆寫舊狀態。
22.3 Stable identifiers
每個 lemma、claim、counterexample、experiment 與 proof object 都應有穩定 ID。
22.4 Explicit status
每個節點必須標記:
等狀態,而不能把 brainstorming 與 theorem 混在一起。
22.5 Machine-readable dependencies
依賴關係必須可以由機器追蹤。
22.6 Human-readable crystallization
大量軌跡之上仍需生成可供人類理解的摘要、論文與概念地圖。
22.7 Independent verification
來源主張與數學正確性必須盡可能由不同檢查機制處理。
23. 對 AI 原生數學研究的更一般結論
AI 原生數學不只是:
真正的變化可能是研究本身開始從「文件」轉向「持續演化的可驗證圖」。
傳統結構:
AI 原生結構可能是:
因此 paper 變成研究圖的一種 human-readable projection,而不再是唯一 source of truth。
這使得:
- 未完成研究;
- 失敗研究;
- 多代理研究;
- 長時間研究;
- AI 自主探索
第一次有機會被保留成結構化、一致且可追溯的科學物件。
24. 核心命題
本文最終提出三個核心命題。
命題一:證明證書不足以表示 AI 原生數學研究
它證明結果的可靠性,但不保證研究歷史的可重建性。
命題二:研究軌跡本身可以成為可驗證物件
前提是狀態、依賴、時間、版本與驗證資料被保留下來。
命題三:部分路線重疊不等於完整證明優先權,但也不應被壓縮為零
同時:
真正需要的是比二值 attribution 更細的語言。
25. 結論
AI 數學的下一個制度問題,可能不是「AI 能不能提出更多證明」,而是:
當研究速度高到人類無法逐步旁觀時,我們要保存什麼,才能在事後仍知道數學是怎麼被發現的?
如果共同體只要求最終 proof certificate,那麼我們可以知道:
是對的。
但我們仍可能不知道:
- 誰先看到核心 obstruction;
- 哪一條失敗路線排除了錯誤空間;
- 哪個 AI 找到局部 lemma;
- 哪個人類重新定義問題;
- 哪些概念早已存在但尚未閉合;
- 最終證明究竟是全新路線,還是先前數學地形的重新組合。
因此 AI 時代需要的證書不應只回答:
「為什麼這個答案可信?」
還應能回答:
「這個答案在概念空間中是怎麼被走到的?」
本文用一句式總結:
而概念積分、預測型來源證據與貢獻圖,則提供三個互補座標:
讓未來數學共同體不必在「只看最後結果」與「人工重讀全部研究過程」之間二選一。
真正需要建立的是:
參考資料
OpenAI. “Advisory Group on Mathematics and Artificial Intelligence.” 2026-09-21.
https://openai.com/index/advisory-group-on-mathematics-and-ai/Tao, Terence. “A Severe Misalignment of AI in Mathematics.” What’s New, 2026-09-11.
https://terrytao.wordpress.com/2026/09/11/a-severe-misalignment-of-ai-in-mathematics/Gowers, Timothy. “Why I Didn’t Sign the Fields Medallists’ Letter.” Cross-posted on Terence Tao’s What’s New, 2026-09-17.
https://terrytao.wordpress.com/2026/09/17/why-i-didnt-sign-the-fields-medallists-letter/Heath, Quentin, and Dale Miller. “A Framework for Proof Certificates in Finite State Exploration.” arXiv:1507.08716, 2015.
https://arxiv.org/abs/1507.08716Sternagel, Christian, and Sarah Winkler. “Certified Ordered Completion.” arXiv:1805.10090, 2018.
https://arxiv.org/abs/1805.10090Research Object Community. “Research Object / RO-Crate.”
https://www.researchobject.org/Workflow Run RO-Crate Working Group. “Workflow Run RO-Crate: Profiles to Capture the Provenance of Workflow Runs.”
https://www.researchobject.org/workflow-run-crate/Nanopublications Community. “Nanopublications: FAIR Data Containers for Scientific Results.”
https://nanopub.net/
附錄 A:本文術語對照
| 中文 | English | 縮寫 |
|---|---|---|
| 研究軌跡證書 | Research-Trajectory Certificate | RTC |
| 終點證書偏差 | Endpoint Certificate Bias | ECB |
| 預測型來源證據 | Predictive Provenance | PP |
| 概念積分 | Concept Integration | CI |
| 貢獻圖 | Contribution Graph | CG |
| 前解答數學地形 | Pre-solution Mathematical Landscape | PML |
| 數學研究狀態 | Mathematical Research State | MRS |
附錄 B:最小主張層級
為避免把來源證據誤用成 priority 宣告,可以把可支持的結論分層:
L0:存在性
L1:概念存在性
L2:結構先行性
在外部結果以前已經以足夠具體的形式存在。
L3:局部數學結果先行性
某個可獨立驗證的 lemma / counterexample / construction 已經成立。
L4:方法先行性
不只得到局部結果,而且使用了與後來證明實質等價的關鍵方法。
L5:完整證明優先權
存在完整、正確、足以支持最終 theorem 的 proof。
因此:
而:
這種分層可以避免「沾到一點就宣稱先證明」與「沒完整閉合就一律視為零」兩個極端。
附錄 C:一句話版本
AI 時代的數學證書,不應只證明答案是對的,也應能證明一條研究路徑在什麼時間以前已經真正走到過哪些數學結構。