AI 數學與形式驗證
OEIS Open 用 Lean 驗證 492 個未解猜想，但交叉檢查把通過數由 147 修正為 144
OEIS Open 讓通用語言模型在固定成本內證明或否證 492 個整數序列猜想，初始 SafeVerify 評分為 147 題通過。另一套 Lean 驗證器重查後確認 144 題，凸顯形式化基準仍會受到規格與檢查器差異影響。
Epoch AI 研究者提出 [OEIS Open](https://arxiv.org/abs/2608.11941)，把 492 個源自《線上整數數列百科》的未解猜想改造成可重複執行的模型評測。每一題已用 Lean 表述，模型必須提交猜想或其否定命題的形式證明；驗收依賴 Lean 核心，而不是比對已知答案或交給另一個模型判分。這使基準能測試目前尚無公開解答的問題，也降低答案直接出現在訓練語料中的可能性。
作者讓 Claude Opus 4.8、GPT-5.5 與 Gemini 3.5 Flash 等模型使用基本 shell、檔案編輯及 Lean 編譯工具。完整集每題預算為 50 美元，所有模型的成功證明聯集涵蓋 147 題，即 30%；隨機抽取 100 題的 Lite 版本把單題預算提高至 200 美元後，最佳模型取得 44%。值得注意的是，額外提供 47.6 萬篇 arXiv 數學論文，或改用更複雜的 DeepAgent 迴圈，都沒有改善 Lite 成績，顯示當前瓶頸未必只是缺少檢索內容或規劃步驟。
為防止代理竄改定理、加入不允許的公理或污染工具鏈，每次嘗試被拆到無網路的代理、乾淨編譯及驗證容器。SafeVerify 會從頭重播編譯產物，核對目標宣告的名稱、型別與可用公理；公開結果庫亦保留每題的 Lean 檔案、token 成本及失敗階段，方便第三方稽核。
不過，驗證器本身仍不是完全無爭議。作者再以 Lean 團隊的 Comparator 交叉檢查 Claude Opus 4.8 結果時，發現五題的原始形式化帶有異常，另有兩題只是 SafeVerify 耗盡資源；依 Comparator 計算，成績應由 147／492 修正為 144／492。這些猜想多半關注度低，數學重要性也未確定，而且分數同時衡量數學推理與 Lean 工程能力。後續應追蹤規格人工稽核、統一驗證器，以及模型能否在較低成本下重現通過證明。