AI 用一個「可愛的證明」推翻了 80 年沒人動搖的數學猜想——然後三家公司同一週都做到了

5 月 21 日，OpenAI 宣布它的內部推理模型構造出一個反例，推翻了 Erdős 在 1946 年提出的單位距離猜想——伴隨 九位外部數學家的驗證論文。5 月 25 日，Google DeepMind 發表 AlphaProof Nexus 論文，用 Lean 形式驗證解了九道 Erdős 開放問題。5 月 26 日，Anthropic 工程師 Sholto Douglas 在 X 上寫：Claude Mythos 也解了同一道猜想，用的是一個「cute, simple proof」。

五天之內，三家公司、三種方法、同一類問題。

我不是數學家，以下不是數學論文導讀。我想搞清楚的是：這件事對用 AI 寫程式的人來說，到底暗示了什麼。

先搞懂這個問題到底在問什麼

Erdős 單位距離猜想說起來很直覺：在一張紙上放 n 個點，最多能有多少對點之間的距離剛好是 1？

1946 年 Erdős 猜測，一種稍微歪斜的正方形網格排列已經接近最優解——也就是說，配對數的成長速度只比點的數量稍微快一點。

這個問題 80 年來沒人動搖過。1984 年 Spencer、Szemerédi 和 Trotter 建立的上界，40 年來也沒被改進。數學家 Thomas Bloom 在 2026 年 4 月的 erdosproblems.com 部落格 把它列入「Erdős 十大最難問題」，理由是：它「已經抵抗了數十年的嘗試」。

一個月後 OpenAI 的模型就構造出了反例。Bloom 後來寫道：「我沒有預期這會在僅僅一個月後發生。」

要說清楚的是：這不是「完全解決」這個問題。OpenAI 找到了一個比經典排列更好的構造，推翻了猜想本身，但 1984 年建立的理論上界依然存在。也就是說，最優排列的真正上限還沒被碰到。

OpenAI 怎麼解的：用了數學家不會去碰的工具

OpenAI 的模型找到一種新的點排列方式，能產生比經典正方形網格更多的單位距離配對。普林斯頓數學家 Will Sawin 估計增益大約是每翻倍一次點數，多出 1% 的配對。

1% 聽起來微不足道。但 Erdős 的猜想說的是根本不可能有任何增益。所以即使只多 1%，猜想就倒了。

更有意思的是解法用的工具。不是幾何——是代數數論。模型用了複數系統的內部對稱性來構造特別密集的點分佈。這些工具在數論裡是標準的，但把它們搬去解平面幾何問題，在場的數學家都覺得匪夷所思。

Thomas Bloom 分析了為什麼人類漏掉了這個方向：你得花大量時間在這個問題上、得願意賭 Erdős 的猜想是錯的、得想到把原始構造翻譯到數域的世界、還得夠熟悉相當專門的類域論。四個條件同時滿足的人類數學家，幾乎不存在。

Fields 獎得主 Tim Gowers 說，如果一個人類把這篇論文投到《Annals of Mathematics》，他「會毫不猶豫地推薦接受」。沒有任何先前的 AI 證明接近過這個水準。

Claude Mythos 的不同路線

Anthropic 的做法是用一組隔離的 Claude Code 實例，每個都有 Mythos 模型的存取權限。它們各自獨立嘗試解題，然後一個實例匯整所有方案並分發給其他實例繼續推進。

數學家 Daniel Litt 評價 Mythos 的結果「比 OpenAI 的稍弱」——但 Mythos 也獨立找到了跟 OpenAI 相同的構造方法。Anthropic 發佈了一份由 Opus 4.7 整理的正式證明版本 PDF。

要注意的是：這裡的「也解了」跟 OpenAI 的「首次發現」性質不同。OpenAI 是先行者，Mythos 是在已知方向上驗證並找到替代路徑。Douglas 用「serious overhang」來形容這件事——他的重點不在誰先做到，而在「一家做到了，其他家立刻也做到」本身就說明這個能力不是偶發的。

DeepMind 用另一套方法也做到了

Google DeepMind 的 AlphaProof Nexus 在同一週解了九道 Erdős 問題，其中兩道已經懸了 56 年。整個推理成本只有幾百美元。

它的方法跟 OpenAI 和 Anthropic 不一樣。Nexus 用的是 Lean 形式語言——模型產生證明步驟，Lean 編譯器逐步檢查，錯誤訊息回饋到下一次嘗試。這是一個有符號驗證安全網的系統，不需要 LLM 自己扛整條邏輯鏈。

有意思的是：研究團隊事後分析發現，最簡單的 Agent（只有 LLM + 編譯器回饋）也能解完全部九道題，只是最難的那幾道花費更高。他們把這歸因於「底層語言模型的快速進步」和「編譯器回饋在接地 LLM 推理上的效果」。

研究者的結論：這反映了一個更大的趨勢——從專門訓練的系統轉向簡單的 agentic loop，隨著 LLM 變得更強大。

三種方法的比較

三家用了不同策略，解的題目也不完全相同（OpenAI 和 Mythos 解的是單位距離猜想，Nexus 解的是另外九道問題）。但重疊的部分——同一道猜想被 OpenAI 和 Mythos 分別用不同路徑解開——確實說明這不是某個特定系統的偶然成功。

先釐清各家結果的可信度

這些結果目前的公開程度和驗證狀態差異很大，不能混在一起當「AI 已經解了」：

OpenAI 的結果有最完整的學術驗證。DeepMind 的優勢是形式驗證——Lean 編譯器通過就是通過，不需要相信人類的判斷。Anthropic 的公開證據目前最薄——主要是員工的 X 發文和一份 AI 整理的 PDF，還沒有經過同等級的外部審查。

這對寫程式的人意味著什麼

數學證明和寫程式碼顯然是不同的事。但這一週的事件裡有幾個模式，如果你每天在用 AI Agent 工具，會覺得很眼熟。

LLM + 驗證器回饋循環已經是通用解題架構了。 DeepMind 發現最簡單的 Agent（LLM 生成 + Lean 編譯器檢查 + 錯誤回饋）就能解九道問題。Anthropic 用多個 Claude Code 實例獨立探索再匯總。如果你有用 CI/CD 裡的 type checker 或 test runner 來回饋 Agent 的修正迴圈——你已經在用同一個架構了。

跨領域搬運是 AI 目前最被低估的能力。 OpenAI 的模型把代數數論的工具搬去解平面幾何，人類數學家不會嘗試這個方向（你得同時精通兩個領域）。在軟體工程裡，「把 A 領域的已知解法搬到 B 領域」也是最容易被忽略的創新路徑。

不能過度推論的地方。 數學反例構造、形式化證明、漏洞掃描、日常軟體開發——這些不是同一種能力。Erdős 問題有非常明確的正確/錯誤判定標準（你的構造要嘛比原來的好，要嘛不是），這讓 AI 的嘗試-驗證-修正循環特別有效。多數軟體工程問題沒有這麼乾淨的判定標準。

附帶一提，解數學的同一個 Mythos 模型，在 Anthropic 的 Project Glasswing 裡也用於安全掃描——一個月內幫 50 家合作夥伴找到超過一萬個高風險漏洞（90.6% 驗證為真正的安全問題）。能做數學推理的模型同時也能更好地理解程式碼的邏輯結構，這不意外。

老實說，我不確定該怎麼消化「五天內三家公司用不同方法解同一類問題」這件事。它可能代表 AI 數學推理到了某個臨界點，也可能是 Erdős 組合幾何問題剛好適合現階段 LLM 的能力特性——明確的判定標準、可搜尋的構造空間、跨領域工具的遷移收益。

我比較確定的是：DeepMind 那個「最簡單的 Agent 也能解全部九道題」的發現，暗示了 LLM + 驗證器的回饋循環比我們以為的更強大。這跟我每天用 Agent 跑 type check 循環的體驗是一致的。

原文來源：

• The Decoder: Claude Mythos solves Erdős problem
• The Decoder: OpenAI disproves unit distance conjecture
• The Decoder: AlphaProof Nexus solves 9 Erdős problems
• Anthropic: Project Glasswing update