OpenAI 說解掉三道 Erdős 難題，資料庫卻標 OPEN (LEAN)：「解決」有兩種意思
OpenAI 在 2026 年 8 月 1 日發表十項數學與理論電腦科學結果，其中三項寫明解掉 Erdős 問題 183、146、180，並附可重跑的 Lean 形式證明。8 月 4 日的 erdosproblems.com 把這三題標成 OPEN (LEAN)：形式證明存在、機器驗得過，但資料庫仍保留未解的非形式狀態，表示尚未依它的標準被人類專家消化與接受。截至當天，全庫只有四題掛著這個標籤。
This article is also available in English: OpenAI Says It Solved Three Erdős Problems. The Database Says OPEN (LEAN).
三道題的編號是 183、146、180。
2026 年 8 月 1 日，OpenAI 發表〈Ten advances in mathematics and theoretical computer science〉，說一個未公開的內部模型做出十項結果，其中三項寫明解掉了這三道 Erdős 問題。8 月 4 日打開 erdosproblems.com，這三題的狀態欄寫著 OPEN (LEAN)，三個頁面同時顯示「0 claimed proofs for this problem」。
所以「解決」到底算不算數？這要先分清楚兩個問題：證明能不能被機器驗過，和這個資料庫是否依自己的標準記錄為已被人類消化與接受。
對照組就在同一個站上。2026 年 5 月的 unit distance 反例，題號 #90，狀態欄寫的是 DISPROVED (LEAN)，後面還跟著一句站方說明：這題已被否定地解決，證明也在 Lean 裡驗過。#183、#146、#180 的同一個位置寫的是「No explanation available」。
差別不在證明的真偽，在一個七月底才被造出來的狀態格。open (Lean) 的意思是：這題有一份形式證明，機器驗得過，但還沒被人類專家消化到資料庫可以接受的程度。按這個資料庫的規則，題目的非形式狀態還開著。
這個狀態格是陶哲軒 7 月 26 日設的，首例是第 1112 題
erdosproblems.com 背後的資料庫放在 GitHub 上，由陶哲軒（Terence Tao，加州大學洛杉磯分校數學教授）維護。2026 年 8 月 4 日的 README 記錄的是 210 題「有一份在 Lean 裡形式化的解」，規則寫得很白：這一批不必是已解決題目的子集合。一份還沒被人類讀者消化的形式化解，會保留它的非形式狀態，所以可以出現 open (Lean) 這種標法。
這條規則不是一直都在。
2026 年 7 月 26 日 19:12 UTC，陶哲軒在 Mathstodon 上說明了設計理由。他寫的原因是：AI 生成、已經在 Lean 裡形式化、但還沒被人類專家消化到可以接受的證明，已經是個會持續下去的現象，資料庫因此把形式狀態與非形式狀態脫鉤。他舉的首例是第 1112 題：這題有一份可驗證的形式解，但還沒有人類消化過它，所以在非形式的意義上仍然開著。
到 2026 年 8 月 4 日，本文查閱的 #146、#180、#183 頁面，也已顯示這個狀態。當日資料庫全表標為 open (Lean) 的四題是 #1112、#146、#180、#183。
機器能檢查的那一層
官方 formalization.yaml 登記 12 條主結果，列出定理宣告、所在檔案、sorry_count 與公理。sorry 是 Lean 的佔位符，表示該處證明尚未補完。
這份登記把 12 條主結果的 sorry_count 都列為 0，公理則列 propext、Classical.choice、Quot.sound。這些是官方 manifest 登記的數值。
有一格要單獨標出來。formalization.yaml 的 review 欄位寫的是 status: "agent-reviewed"：審查是 agent 做的，而且這是官方自己標的。官方在 blog 裡對分工也講得很直接：他們協助把論證整理成手稿、把證明形式化進 Lean，並為正確性負責，而數學論證本身由他們的系統產生。
Lean 驗過的，和它交還給人的
Lean 驗過一份證明，保證的是一件很具體的事：在這份檔案寫下的這組定義之下，這個敘述可以被證明。它不保證那組定義忠實對應數學文獻裡的那個概念。
這不是外人的挑剔，是 Lean 官方語言參考手冊〈Validating Proofs〉自己做的區分：要分開「這個定理有沒有有效的證明」和「這個定理敘述是什麼意思」。
判斷：兩種「解決」
我認為這次真正新的不是十個證明，而是那個狀態格。
open (Lean) 這五個字承認了一件過去不需要承認的事：一道題可以同時「有一份機器驗得過的證明」和「還沒被依資料庫的標準接受為解決」。在 2026 年 7 月 26 日之前，資料庫裡沒有格子能同時裝下這兩件事。
那三個證明對不對，本文不作獨立裁決。官方 manifest 記錄了零 sorry_count 與三個標準公理；8 月 4 日的資料庫頁面，則仍把三題的非形式狀態標為 open。這是兩種記錄，不能互相取代。
所以「OpenAI 解掉三題」和「資料庫標還沒解決」並不矛盾，它們回答的是兩個問題。前者對應官方公開的 Lean 形式證明；後者是這個資料庫記錄的人類消化狀態，8 月 4 日當天仍維持非形式未解。
來源
- OpenAI, Ten advances in mathematics and theoretical computer science: https://openai.com/index/ten-advances-in-mathematics/
- Official manifest and toolchain: https://github.com/openai/ten-proofs
- Erdős problem pages: https://www.erdosproblems.com/183 , https://www.erdosproblems.com/146 , https://www.erdosproblems.com/180 , https://www.erdosproblems.com/90
- Database README: https://github.com/teorth/erdosproblems
- Terence Tao, 26 July 2026: https://mathstodon.xyz/@tao/116987866420438091
- Lean, Validating Proofs: https://lean-lang.org/doc/reference/latest/ValidatingProofs/
常見問題
OpenAI 真的解出了那三道 Erdős 問題嗎？
OpenAI 官方頁面寫明這十項結果中包含解掉 Erdős 問題 183、146、180，並且提供了可下載、可重跑的 Lean 形式證明。但截至 2026 年 8 月 4 日，erdosproblems.com 上這三題的狀態是 OPEN (LEAN)，頁面同時顯示「0 claimed proofs for this problem」，那是網站欄位的顯示，不等於沒有人主張有證明。這個狀態不代表有人主張證明是錯的：本文不由資料庫狀態判定證明真偽。它代表的是：形式證明存在、機器驗得過，但尚未依這個資料庫的標準被人類專家消化並接受，所以題目的非形式狀態仍然開著。
open (Lean) 這個狀態是什麼意思？
這是 erdosproblems.com 背後資料庫在 2026 年 7 月 26 日新增的狀態，由維護者陶哲軒說明設計理由：為了回應「AI 生成、已在 Lean 形式化、但尚未被人類專家消化」的證明，資料庫把形式狀態與非形式狀態脫鉤。README 寫得很直接：一份還沒被人類讀者消化的形式化解，會保留它的非形式狀態，因此可以出現 open (Lean) 這種標法。首例是第 1112 題。到 2026 年 8 月 4 日，這三題的頁面也顯示該狀態。
Lean 驗過的證明還會出錯嗎？
會，但出錯的方式跟一般人想的不一樣。Lean 官方文件把兩個問題明確分開：「這個定理有沒有有效的證明」和「這個定理敘述是什麼意思」。機器保證的是前者，而且是在該檔案寫下的那組定義之下；那組定義是否忠於數學文獻上的概念，要人類判斷。