跨世代認知挑戰物：以動態不動點與開放形式理論為例

系列： 最後人類認知前沿（Last Human Cognitive Frontier, LHCF）
篇次： 11 / 12
作者： Neo.K
研究協作： Aletheia（GPT-5.6 Thinking）
版本： v0.1
日期： 2026-08-07

摘要

如果一套人類理論尚未完成、尚未形式化，甚至可能部分錯誤，它是否仍值得留給未來高階智慧？本文主張：可以，但前提不是把「未完成」浪漫化，而是把未完成部分轉換成可審核、可重建、可反駁、可形式化、可分叉與可取代的跨世代認知挑戰物（Cross-Generational Cognitive Challenge Object, CGCCO）。

本文以「動態不動點數學／開放形式理論」作為方法案例，而非已被證實的新數學體系。案例的核心動機可概括為：研究對象不只是一個固定形式系統，而是一族可隨時間演化的數學狀態

\mathfrak M_t,

以及其演化算子

\Phi_t: (\mathfrak M_t,\mathfrak C_t) \rightarrow \mathfrak M_{t+1},

其中 $\mathfrak C_t$ 表示語境、約束、證據、工具與歷史條件。本文不預設這套結構具有超越既有數學的獨立價值，而把它視為一個理想測試案例：未來 AI 應能判斷其哪些部分只是已知概念重命名、哪些部分可映射到既有範疇論／動力系統／重寫系統／形式語義／版本化邏輯，哪些部分不一致，哪些部分可以形成真正新問題。

本文提出 Open Theory Challenge Object（OTCO，開放理論挑戰物） 的十層結構：身份層、語義核心層、形式候選層、依賴層、證據層、失敗層、版本層、可執行層、開放義務層與繼承層。其核心原則為：

\boxed{ \text{Preserve the claim} + \text{preserve how it can fail} + \text{preserve how a successor may replace it}. }

本文進一步建立九級未來 AI 挑戰協議：語義重建、既有理論映射、最小形式化、一致性審計、反例搜索、機器驗證、非平凡結果生成、框架壓縮／重構、繼承或終止。完成挑戰不要求證明原理論為真；相反地，若未來 AI 證明它可完全壓縮為已知理論、發現核心矛盾、建立更簡潔的替代理論，皆屬成功。

2026 年 AI4Math 的實際進展使這種設計具有現實意義。Formal Conjectures 已將一千多個開放研究猜想形式化為 Lean 4 並建立持續演化的研究級 benchmark；AI 驅動的形式證明搜索已在數百個 Erdős／OEIS 問題上產生新解；另一方面，最新 benchmark audit 也提醒「Lean 能編譯」不代表自然語言意圖已被忠實形式化，形式陳述仍可能缺假設、變成 vacuous theorem 或偏離原問題。這意味著未來 challenge object 不能只保存一個 theorem ... := by 目標，而必須同時保存原語義、形式候選與兩者對齊證據。

本文最後把動態不動點案例整理成一個可由未來 AI 接手的最小研究接口：哪些概念是不可改寫的語義錨點、哪些數學結構只是候選實現、哪些命題尚未證明、哪些替代框架被允許、哪些實驗或形式結果會迫使原系統分裂或終止。這使「留給未來 AI」不再等於留下一篇神祕文本，而是留下一個有明確輸入、輸出、失敗條件與 successor protocol 的研究工程物件。

關鍵詞： 開放形式理論、動態不動點、跨世代知識、形式化、Lean、AI4Math、Research Object、認知挑戰物、理論繼承、LHCF

1. 為什麼需要「挑戰物」，而不只是未完成論文？

普通未完成論文常留下：

一些概念；
一些猜想；
幾段動機；
若干尚未證明的敘述。

未來讀者會遇到：

\boxed{ \text{作者到底想說什麼？} }

如果連這一步都無法穩定重建，後續：

\text{formalize} \rightarrow \text{verify} \rightarrow \text{extend}

全部失去意義。

因此「留給未來」不能只寫：

此問題留給後世解決。

而必須提供：

\boxed{ \text{challenge interface}. }

2. 一個跨世代挑戰物的最低條件

令挑戰物：

\mathcal O.

至少要回答：

你是什麼？
你聲稱什麼？
哪些地方還沒完成？
什麼證據會支持你？
什麼結果會推翻你？
哪些概念可以被替換？
哪些只是暫時記號？
未來智能應先做什麼？
如果原理論失敗，如何留下 successor？

因此：

\boxed{ \text{Open Theory} \neq \text{Unspecified Theory}. }

3. 案例定位：動態不動點不是本文要證明的定理

本文使用「動態不動點數學」作案例時，採取以下立場：

\boxed{ \text{Case Study} \neq \text{Validation}. }

我們不在本文證明：

它是新的數學基礎；
它比既有範疇論更強；
它形成一致形式系統；
它有不可還原的新定理。

這些恰好是 challenge object 留給未來 AI／數學家的工作。

因此案例價值在於：

它是否能被整理成一個未來可以嚴格判定成敗的開放研究物件？

4. 語義母錨點

案例最核心的自然語言錨點可寫成：

\boxed{ \text{變又不變，不變又變。} }

這句話本身不是數學定義。

它只是表達一個研究動機：

在形式系統、概念、語言與驗證規則可能演化時，什麼意義上的結構／身份仍可以被視為持續？

因此真正需要形式化的是：

\boxed{ \text{change} + \text{identity} + \text{equivalence} + \text{history}. }

5. 狀態化數學物件

一個候選形式可令：

\mathfrak M_t = ( L_t, A_t, R_t, K_t, E_t, V_t, H_t, D_t ),

其中：

$L_t$ ：language，語言／符號；
$A_t$ ：axioms，當前公理／假設；
$R_t$ ：rules，推理與重寫規則；
$K_t$ ：knowledge，已接受結果；
$E_t$ ：equivalence，當前等價判準；
$V_t$ ：verification，驗證制度；
$H_t$ ：history，版本／證明／失敗歷史；
$D_t$ ：debt，未解義務與形式債務。

這不是唯一形式化。

未來智能可以提出更好的：

\mathfrak M_t'.

6. 演化算子

定義候選演化：

\boxed{ \Phi_t: (\mathfrak M_t,\mathfrak C_t) \rightarrow \mathfrak M_{t+1} }

其中：

\mathfrak C_t

可以包含：

新證明；
反例；
新資料；
新工具；
新語言；
新 verifier；
外部理論映射；
資源限制。

核心問題因此不是：

x=f(x)

的普通固定點問題。

而是：

當描述固定點的系統本身改變時，什麼條件允許我們仍說「它是同一個理論／同一個結構」？

7. 動態等價問題

令：

x_t\in\mathfrak M_t,

x_{t+1}\in\mathfrak M_{t+1}.

需要定義：

x_t \sim_{t,t+1} x_{t+1}.

但：

\sim

本身可能也演化。

所以真正困難是：

\boxed{ \text{equivalence under changing equivalence criteria}. }

這可能映射到既有：

bisimulation；
equivalence of categories；
model equivalence；
program refinement；
versioned semantics；
homotopy／path-based identity；
institution morphisms；

等概念。

未來挑戰的第一部分，就是找出最佳 prior-art mapping。

8. 第一條挑戰原則：先壓縮，不准先發明

未來 AI 接手時，不應第一步就替這套理論增加新術語。

第一步應是：

\boxed{ \operatorname{CompressAgainstPriorArt}(T). }

也就是：

哪些概念已有標準名稱？
哪些公式等價於已知結構？
哪些只是哲學敘述？
哪些部分真的沒有直接對應？

如果：

T \subseteq \operatorname{Closure}(K_{\mathrm{known}}),

最好的結果可能是：

全部可壓縮成既有理論。

這是成功，不是失敗。

9. 第二條原則：作者不是形式真理來源

對理論原作者：

h.

未來 AI 可詢問：

\operatorname{Intent}(h).

但：

\boxed{ \operatorname{Intent}(h) \neq \operatorname{Truth}(T). }

若：

原文；
後續版本；
作者口頭解釋；
形式化結果；

彼此衝突，應保留衝突。

不能事後把所有矛盾解釋成：

作者原本就是這個意思。

10. 作者只擁有「語義證詞權」，不擁有「結果否決權」

作者可以說：

我當時想表達 $X$ 。

這對：

G_S

Semantic Reconstruction 有幫助。

但如果形式化後：

X \Rightarrow \bot,

作者不能用：

那我其實不是那個意思。

直接消除舊版本失敗。

正確處理是：

T_0 \xrightarrow{\text{refuted}} T_1.

版本必須保存。

11. OTCO：開放理論挑戰物

本文定義：

\boxed{ \mathcal O_T = ( I, S, F, D, E, X, V, R, O, H ) }

十層：

$I$ ：Identity；
$S$ ：Semantic Core；
$F$ ：Formal Candidates；
$D$ ：Dependencies；
$E$ ：Evidence；
$X$ ：Failure / Counterexample；
$V$ ：Version Graph；
$R$ ：Runnable Artifacts；
$O$ ：Open Obligations；
$H$ ：Handoff / Inheritance。

12. Identity Layer

至少保存：

I= ( \text{ID}, \text{title}, \text{author}, \text{date}, \text{version}, \text{hash} ).

如果未來有：

T_0,T_1,T_2,

必須知道哪個才是：

active；
superseded；
refuted；
historical。

13. Semantic Core Layer

定義：

S= ( \mathcal D, \mathcal C, \mathcal Q, \mathcal B ).

其中：

$\mathcal D$ ：核心定義；
$\mathcal C$ ：不可隨意漂移的核心主張；
$\mathcal Q$ ：核心問題；
$\mathcal B$ ：適用邊界。

對動態不動點案例，核心問題之一可表達為：

\boxed{ \text{如何形式化會演化的形式系統之跨時身份？} }

14. Semantic Core 不等於固定數學實現

例如：

\mathfrak M_t

用 tuple 表示只是一個 implementation candidate。

未來可以換成：

category；
graph；
transition system；
dependent type；
rewriting system。

只要仍忠實處理：

\text{change / identity / equivalence / history}.

所以：

\boxed{ \text{semantic invariants} \neq \text{notation invariants}. }

15. Formal Candidate Layer

保存多個候選：

F= \{ F_1,F_2,\ldots,F_n \}.

例如：

$F_1$

狀態轉移系統。

$F_2$

範疇／函子演化。

$F_3$

帶版本的 dependent type theory。

$F_4$

重寫系統＋等價關係演化。

禁止假裝已知道哪一個是最終形式。

16. Formalization Fidelity

2026 年形式化研究再次提醒：

\boxed{ \text{Lean compiles} \neq \text{meaning preserved}. }

一個形式 statement 可以：

漏假設；
改 domain；
變成 vacuous theorem；
形式上可證但完全不是原問題。

因此每個：

F_i

都需要：

\operatorname{Fidelity}(S,F_i).

17. 三向對齊

至少需要：

\boxed{ \text{Natural Language} \leftrightarrow \text{Formal Statement} \leftrightarrow \text{Executable / Test Behavior}. }

三者互相驗證。

不能只靠：

\text{NL}\rightarrow\text{Lean}.

18. Dependency Layer

建立：

G_D=(V,E).

節點包含：

定義；
公理；
定理；
假說；
實驗；
外部理論。

若命題：

C_7

依賴：

A_2,C_3,C_5,

必須明確表示。

這樣未來反駁：

A_2

時，可以自動傳播：

\operatorname{Invalidate}(C_7).

19. Evidence Layer

不是所有開放形式理論都有 empirical evidence。

因此：

E

可以包含：

formal proof；
computational experiment；
model example；
theorem mapping；
empirical observation；
simulation；
literature support。

每個 claim 應標：

\operatorname{EvidenceType}(C_i).

20. Failure Layer

這是 challenge object 最重要的部分之一。

保存：

X= ( \text{counterexamples}, \text{failed proofs}, \text{broken definitions}, \text{negative results}, \text{dead branches} ).

因為未來智能真正需要知道：

哪些路已經走過而且為什麼不行？

21. 失敗不是垃圾資料

若一個 proof attempt：

P

失敗，

其價值可能是：

I(P;\Omega)

——它排除了多少搜索空間。

所以 failure ledger 可以降低未來：

C_{\mathrm{search}}^*.

這直接接第 9 篇 TARG。

22. Version Graph

不只線性：

T_0\rightarrow T_1\rightarrow T_2.

還允許：

T_1 \rightarrow \begin{cases} T_{2a}\\ T_{2b}\\ T_{2c} \end{cases}

不同 successor 可以競爭。

這是：

\boxed{ \text{theory branching}. }

23. 理論可以死亡

Open Theory 不應有「永遠可修補」特權。

定義終止條件：

\operatorname{Terminate}(T)

若例如：

核心語義無法穩定重建；
所有合理形式化都矛盾；
完全被更簡潔既有理論吸收；
沒有獨立生成力；
後續修補已改變原核心。

此時最好的 successor 可以是：

\boxed{ \text{archive as historical object}. }

24. Open Obligations Layer

對動態不動點案例，至少可以列出：

O1：動態等價

是否可定義：

\sim_{t,t'}

並保持可組合性？

O2：跨框架身份

若：

L_t\neq L_{t+1},

「同一命題」如何映射？

O3：演化一致性

\Phi_t

是否可能造成任意 trivialization？

O4：可重開性

一個曾被關閉的命題，什麼條件下可重新變成 open？

O5：長鏈穩定性

\Phi_n\circ\cdots\circ\Phi_1

是否存在可控制 invariant？

O6：自我修改

如果 verification rule：

V_t

本身被改寫，如何防止自我合法化？

25. 自我合法化問題

最危險的動態理論是：

我可以改自己的規則，所以任何反例都能透過改規則解決。

這等於：

\boxed{ \text{unfalsifiable by self-modification}. }

因此必須定義：

\operatorname{LegalUpdate} ( \mathfrak M_t, \mathfrak M_{t+1} ).

更新規則本身也需要外部約束。

26. Meta-Verification Constraint

一個候選條件：

V_{t+1}

不能單獨決定：

V_t

曾經錯不存在。

必須保留：

H_t.

所以：

\boxed{ \text{future validity} \neq \text{retroactive erasure}. }

27. Runnable Layer

即使是抽象數學，也可建立最小 executable semantics。

例如定義：

\mathfrak M_t

的有限 toy model，

測：

version transition；
equivalence update；
contradiction propagation；
branch／merge；
invariant tracking。

未來 AI 可以先驗證：

\text{conceptual consistency in finite models}.

28. Toy Model 不等於證明

如果有限程式：

P

成功運行：

\operatorname{Run}(P)=1,

只表示：

至少有一個實例可執行。

不能推出：

\text{general theorem}.

因此 runnable artifact 與 proof obligation 必須分開。

29. Inheritance Layer

最重要的不是：

請未來 AI 把這套理論做完。

而是：

\boxed{ \text{允許未來 AI 拒絕它。} }

Handoff protocol 必須明確允許五種結論：

Validate
Partially Validate
Compress into Known Theory
Refute
Replace

30. 五種結果都算成功

令 future evaluator：

A_f.

挑戰成功定義：

\operatorname{Success}(A_f,\mathcal O_T)=1

如果它能給出：

\boxed{ \text{auditable disposition} }

而不是只有：

我覺得這理論很有趣。

所以真正成功的是：

\text{clarification}.

31. 第 0 級挑戰：Corpus Audit

先判斷：

哪個版本是 canonical？
是否有 duplicate？
哪些文件缺失？
哪些定義互相衝突？

輸出：

A_0.

沒有這一步，不准開始形式化。

32. 第 1 級：Semantic Reconstruction

AI 必須從原 corpus 重建：

\hat S.

再與：

作者說明；
文件； -版本歷史；

比對。

測：

R_A.

33. 第 2 級：Prior-Art Compression

建立映射：

\Psi: T \rightarrow \mathcal K_{\mathrm{math}}.

輸出：

exact equivalence；
partial analogy；
misleading analogy；
candidate novelty。

如果 90% 可壓縮，應直接說 90%。

34. 第 3 級：Minimal Formalization

不是一次形式化所有文章。

先找：

\mathcal C_{\min}

最小核心命題集。

例如：

\{ \mathfrak M_t, \Phi_t, \sim_{t,t'}, \operatorname{LegalUpdate} \}.

建立 Lean／Coq／Isabelle／其他形式候選。

35. 第 4 級：Consistency Audit

測：

\operatorname{Consistent}(F_i)?

包括：

triviality；
circular definitions；
hidden axioms；
contradictory update rules。

若：

F_i\vdash\bot,

記錄最小矛盾核心：

\operatorname{MUS}(F_i).

36. 第 5 級：Counterexample Search

對每個非定義性核心 claim：

C_i,

建立：

\operatorname{CounterexampleSearch}(C_i).

包括：

finite models；
property-based testing；
SAT/SMT；
model checking；
symbolic search。

37. 第 6 級：Verified Result Generation

如果理論仍存活，

要求產生至少一個：

C^*

滿足：

非 trivial；
可機器驗證；
不是直接重述定義；
相對 prior art 有明確位置。

這是從概念框架跨向數學結果的最低門檻。

38. 第 7 級：External Transfer

測：

\Delta_A(T)

或：

\Delta_{\mathrm{transfer}}.

也就是：

吸收此框架後，AI 是否能在外部問題做得更好？

例如：

版本化形式系統；
自修改 agent verification；
theorem evolution；
dynamic semantics。

若完全沒有外部遷移，

其價值可能主要是歷史／哲學。

39. 第 8 級：Successor Generation

要求未來 AI 提出：

T'

並說明：

T' \succ T

在哪些維度更好：

simpler；
more rigorous；
more general；
more testable；
lower resource cost。

40. 第 9 級：Termination / Inheritance Decision

最後不是：

這套理論永遠值得研究。

而是：

\boxed{ \operatorname{Disposition} \in \{ \text{continue}, \text{branch}, \text{merge}, \text{archive}, \text{terminate} \}. }

這使 challenge object 有真正生命週期。

41. 與 2026 Formal Conjectures 的關係

Formal Conjectures 已把：

2615

個研究級數學問題形式化為 Lean 4，其中包含：

1029

個 open research conjectures。

它的特別價值不是只有題量。

而是建立：

\boxed{ \text{open} + \text{formal} + \text{evolving} + \text{community-audited} }

的研究接口。

這正是 OTCO 可以借鑑的模式。

42. AI 已開始真正處理開放數學問題

2026 年大規模形式證明搜索已報告：

解決部分 open Erdős problems；
證明部分 OEIS conjectures；
使用 Lean 做 machine verification。

這說明：

\boxed{ \text{future challenge object} }

不必假設 AI 只能閱讀。

它可以被設計成：

\text{machine-actionable open research}.

43. 但「formal」仍然不等於「faithful」

2026 年對 Lean benchmark 的審計發現：

counterexample；
vacuous theorem；
unsound axiom；
benchmark harness defect。

因此：

\boxed{ \text{kernel checked} \neq \text{research intent checked}. }

這對 OTCO 是硬性警告。

44. 雙重 verifier

因此至少需要：

Formal Verifier

檢查：

F\vdash C.

Semantic Fidelity Verifier

檢查：

F \approx S.

兩者缺一不可。

45. Challenge Object 的評分向量

定義：

\mathbf Z(\mathcal O_T) = ( Z_S, Z_F, Z_A, Z_X, Z_V, Z_R, Z_O, Z_H ).

其中：

$Z_S$ ：semantic stability；
$Z_F$ ：formalizability；
$Z_A$ ：auditability；
$Z_X$ ：counterexample accessibility；
$Z_V$ ：version integrity；
$Z_R$ ：runnability；
$Z_O$ ：open-obligation quality；
$Z_H$ ：handoff quality。

46. 成熟度階梯

Level 0：Narrative Artifact

只有文章。

Level 1：Versioned Artifact

有版本／hash。

Level 2：Auditable Artifact

定義、證據、failure ledger。

Level 3：Formalizable Artifact

有最小形式化接口。

Level 4：Executable Challenge

有 verifier、tests、formal targets。

Level 5：Cross-Generational Cognitive Challenge Object

有完整 successor／termination protocol。

本文案例目標是：

\boxed{ L_5. }

47. 動態不動點案例的最小 P5 包

最少應包含：

A. Canonical Manifesto

只說研究動機與邊界。

B. Core Semantics

定義：

\mathfrak M_t,\Phi_t,\sim_{t,t'}.

C. Prior-Art Map

列出可能對應：

category theory；
rewriting；
dynamic logic；
type theory；
versioned semantics。

D. Formal Sandbox

Lean／Coq toy formalization。

E. Failure Ledger

所有已知問題。

F. Open Obligations

O1–O6。

G. Benchmark Tasks

從 semantic reconstruction 到 successor generation。

H. Disposition Protocol

允許 archive／terminate。

48. 什麼東西絕對不能放進不可修改核心？

不應把：

某個符號；
某套命名；
某篇文章；
作者原始措辭；
「這一定是全新數學」；

設為不可修改核心。

真正核心應盡量小：

\boxed{ \text{研究問題，而不是預設答案。} }

49. 最好的跨世代錨點是問題，不是理論名稱

因此案例最穩定的 anchor 可能不是：

Dynamic Fixed-Point Mathematics.

而是：

\boxed{ Q^*= \text{如何形式化形式系統在自我演化下的身份、等價與可驗證性？} }

只要：

Q^*

仍有意義，

即使：

T

被完全取代，

挑戰仍然成功傳遞。

50. 跨世代認知物的真正不可替代性

一個 challenge object 最有價值的不是：

後人一定要使用它。

而是：

後人不必重新猜我們當時到底卡在哪裡。

因此它降低：

\boxed{ C^*_{\mathrm{reconstruction}}. }

同時保留：

\boxed{ O_V }

Future Option Value。

51. 可反駁預測

預測一

完整 OTCO 包會顯著降低未來 AI 的 semantic reconstruction error。

預測二

保存 failure ledger 會降低搜索成本：

C_{\mathrm{sea}}^*.

預測三

雙 verifier 比單純 Lean compilation 更能避免「證明錯問題」。

預測四

大部分開放人類理論經 prior-art compression 後會大幅縮小，而不是全部保留原始術語。

預測五

真正高品質的 challenge object 即使原理論最終被 refute，也仍具有正重建價值。

52. 如何反駁本文？

如果未來實證發現：

只留原始 prose 已足以無損重建；
failure ledger 對未來搜索沒有幫助；
semantic fidelity 可以由形式編譯自動保證；
successor protocol 不影響研究繼承效率；
open-theory object 與普通 archive 的效果沒有差異；

則 OTCO 架構應被簡化。

53. 與 LHCF 前十篇的整合

前十篇回答：

\text{什麼是前沿？}

\text{什麼對 AI 難？}

\text{誰仍能產生前沿？}

\text{要花多少資源？}

\text{什麼值得完整重建？}

本文加入：

\boxed{ \text{如何把一套未完成理論真正做成可被未來智能接手的研究物件？} }

54. 結論：最好的「留給未來 AI」，不是把答案藏起來，而是把問題做乾淨

一個真正的跨世代認知挑戰物不應要求未來 AI：

證明我們是對的。

而應要求它：

\boxed{ \text{理解我們說了什麼， 判斷哪些已知， 找出哪些錯誤， 形式化哪些可形式化， 完成哪些未完成， 並在必要時把整套理論換掉。} }

動態不動點案例之所以適合作為本文示範，不是因為本文已證明它是一套成立的新數學。

恰恰相反。

它仍有：

形式語義缺口；
prior-art 映射問題；
動態等價問題；
自我修改驗證問題；
長鏈穩定性問題；
非平凡定理缺口。

所以它可以被整理成：

\boxed{ \text{open, auditable, falsifiable, inheritable}. }

最終理想的未來結果甚至可能是：

\boxed{ T \xrightarrow{\text{ASI reconstruction}} T' }

其中：

T'

已經不再叫「動態不動點數學」。

只要：

原問題被更清楚表達；
錯誤被保留為歷史；
有價值結構被吸收；
新理論更強、更簡潔、更可驗證；

那就是成功。

因此跨世代知識傳承真正應保存的不是：

\boxed{ \text{理論名稱的永生} }

而是：

\boxed{ \text{問題、證據、失敗與可繼承的認知結構。} }

下一篇也是整個系列最後一篇：

《認知對手的終結：從最後人類前沿到 AI 原生認知主導》

第 12 篇將把所有集合、能力、配置、吸收成本與跨世代 challenge object 收斂成一個終局模型，正式定義：

\boxed{ \text{在什麼條件下， 我們才可以說「最後人類認知前沿」真正結束？} }

參考文獻

[1] Jiang, E. et al. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier. arXiv:2607.07779, 2026.

[2] Tsoukalas, G. et al. Advancing Mathematics Research with AI-Driven Formal Proof Search. arXiv:2605.22763, 2026.

[3] Firsching, M. et al. Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics. arXiv:2605.13171, 2026.

[4] Long, W. et al. CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean. arXiv:2605.17255, 2026.

[5] Pham, Q. V. et al. TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics. arXiv:2606.09450, 2026.

[6] Ammanamanchi, P. S., Bhat, S., & Biderman, S. Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving. arXiv:2606.29493, 2026.

[7] Zhang, K. et al. Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization. arXiv:2606.31002, 2026.

[8] Soltani Moakhar, A. et al. Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics. arXiv:2606.31134, 2026.

[9] Neo.K / Aletheia. 最後人類理論：哪些知識作品值得高階智慧完整重建. LHCF 10, 2026.

版本註記

v0.1 建立 OTCO（Open Theory Challenge Object）、十層開放理論物件、九級未來 AI 挑戰協議、作者語義證詞權／非結果否決權、雙 verifier、理論分叉／終止協議與 P5 級跨世代挑戰物最小包。本文使用「動態不動點」僅作 challenge-object 工程案例，不構成對其數學新穎性、正確性或完整性的驗證。

11_跨世代認知挑戰物_以動態不動點與開放形式理論為例_v0.1