定理經濟的衰落：AI 與數學理解危機

證明與理解的脫鉤

數學的主要價值在於提升人類世界觀的認知，而非僅僅產出定理。 雖然學術界的「定理經濟」獎勵新結果的發現，但該領域的真正智力進步是透過概念構建與直覺發展——這些過程與機械式的定理證明是不同的。

數十年來，這兩個面向共生共存：解決一個困難的猜想被視為密碼式的證明，表明數學家已經產生了真正的概念創新。然而，大型語言模型（LLM）與自動形式化工具的出現正打破這層連結。AI 現在可以產生正確的形式化證明，卻不提供人類理解所必需的概念框架。

「Mathslop」問題與典範化危機

AI 生成的證明可能形成一層「Mathslop」——正確卻難以理解的形式推導，無法為人類數學語料庫作出貢獻。

在人類數學中，證明必須可理解才能有用；它們是其他數學家學習並擴展自身直覺的載體。相較之下，AI 系統可以產生龐大、充滿「氛圍編碼」的形式代碼（例如 Lean 中的程式），雖在技術上正確，卻缺乏可理解的介面。

這導致了「典範化」危機——將一次性形式化轉變為一般、可重用且連貫的函式庫數學的過程。正如 Mathlib 社群的研究者所指出，當 AI 公司搶先完成重大定理（例如 Maryna Viazovska 的球體堆積工作）的形式化，卻不進行繁瑣的典範化工作時，他們留下的將是一片「放射性荒原」，對人類理解毫無實際益處。

「Overhang」與發現的自動化

許多被視為數學創造力的事實，其實是對「Overhang」的收割——透過在龐大且碎片化的語料庫中連結既有點而發掘的潛在價值。

因為 LLM 可以在整個數學文獻上進行訓練，它們能獨特地捕捉語法類比與對應，這是人類數學家一生可能只閱讀數百篇論文所無法做到的。這使得 AI 能「先於」人類研究者，發現問題的解答已經存在於另一個看似無關的數學分支中。

此能力暗示 AI 可能在取得概念構建的充分性之前，就已經在問題解決上取得優勢。危險在於公眾與學術界可能會把解決技術性引理的能力誤認為是高層次數學綜合的能力。

對數學職業的生存威脅

如果定理證明仍是唯一官方的數學貨幣，該職業將面臨系統性的去貨幣化。

傳統指標，如「First Proof」計畫，關注 AI 能否解決研究層級的問題。雖然這對技術評估有用，卻加深了數學是「封閉系統」如棋或圍棋的敘事。此框架忽視了學科以人為本的目標：清晰、理解，以及改變我們思考方式的能力。

此轉變帶來即時的實務後果：

• 學術絕望： 初期研究者面臨未來大部分傳統工作將被自動化的局面，質疑研究數學作為職業的長久性。
• 教學崩潰： AI 在教育中的使用讓學生能產出正確答案，卻未經歷實際數學能力所需的神經可塑性變化，可能導致一代畢業生缺乏真正技能。

為數學打造新敘事

為了在 AI 轉型中存活，數學社群必須將其價值主張從「解題」轉向「提升人類理解」。

緩解損害的建議方案包括：

• 數學智慧等級尺度： 類似自駕車的自主等級，一個尺度可以區分「暴力」問題解決（等級 1‑3）與更高層次的概念綜合與典範化（等級 8‑10）。
• 撤銷「榮譽守則」： 數學家必須停止將直覺與闡述視為次要或「二等」工作，應將其置於領域的主要產出。

正如 Terry Tao 所預測的，雖然 AI 可能很快處理掉目前出現在數學論文中的大部分工作，但這將顯示那些任務並非數學家真正最重要的工作。該領域的未來可能在於「直覺最大化者」——利用 AI 處理形式化繁重工作，同時專注於探索新概念大陸的研究者。

---

摘要： David Bessis 主張，AI 解決定理的能力威脅到「定理經濟」，因為它使形式證明與人類理解脫鉤，可能使傳統的學術獎勵制度變得過時。

標題： 定理經濟的衰落：AI 與數學理解危機