形式化不是吃苦藥，Axiom 對 AGI 路徑的反主流判斷

2025 年，成立僅七個月的 Axiom 在 Putnam 數學競賽解出全部 12 題（限時內完成 8 題），優於頂尖大學生的 110/120 分、DeepSeek 據報的 103/120 分。Putnam 歷屆中位數通常是 0 到 1 分，這份成績單並非不值一提。但與其把它讀成「AI 又破了一道難關」，不如把它當成 Axiom CEO Carina Hong 世界觀的入口。以下觀點來自 Latent Space 對她的深訪，代表創辦人立場。

快轉到 2026 年中，Claude Code 與 Codex 已成為工程師工作流的標配。Anthropic 在 2024 年的「all in code 與企業市場」當時像保守的利基押注，如今顯得極為精準：coding AI 確實把「超智能邊界」往外推了不少。

但 Hong 的判斷是：coding 能力是通往 AGI 的必要條件，不是充分條件。她認為現有 AI 在「非形式化（informal）」推理上存在讓人意外的缺口，而這個缺口才是接下來真正的瓶頸。

她把 verification（可驗證性）從「合規式約束」重新框架成截然不同的東西：驗證是在「scaling 與 compounding 卓越性」。這聽起來像行銷詞彙，直到 Ramanujan 的故事讓框架落地。

傳奇數學家 Ramanujan 憑直覺提出大量定理，但直覺無法被傳遞。G.H. Hardy 逼他把直覺轉化成形式證明後，兩件事同時發生：強迫明確化的過程讓 Ramanujan 自己開闢出新思路，形式化對自己產生 compounding，能力在更穩固的地基上繼續堆疊；同時，形式化的證明讓直覺變得可傳播、可驗證，任何人都能接棒沿用，這是 scaling。穩固的公理（Axioms）才是複利的前提，也是這家公司名字的來源。

對做推理或數學 AI 的團隊，這是一把具體的尺。很多模型的能力建在搖晃的地基上，某些 benchmark 亮眼，推理鏈一旦需要嚴格對接就破功。如果可驗證性只是「展示安全合規」的包裝，投資報酬率確實低。但若把它當成讓模型推理能自我 compound 的機制、以及讓結果能被更廣泛採信與沿用的基礎設施，它就不是在吃花椰菜，而是在賭複利。

當全行業把 coding 當成通往超智能的捷徑，Axiom 在問一個更難的問題：在 coding 之後，瓶頸長什麼樣？