OpenAI 研究員 Dan Roberts 於 2026 年 10 月 8 日在 X（原 Twitter）上宣布，OpenAI 已更新其 GitHub 數學倉庫（openai/math）。此次更新包含 6 項新的 Lean 形式化證明、19 項修改以及 3 項結果的撤回。Roberts 指出，該倉庫目前已有約 42% 的頂層結果（top-line results）完成形式化，並承諾將持續更新倉庫，納入新的形式化證明及發現的任何勘誤。
事件背景
OpenAI 的數學倉庫（openai/math）是一個公開的 GitHub 儲存庫，用於記錄與數學研究相關的結果。根據推文連結指向的 history.md 檔案，該倉庫追蹤了結果的形式化狀態與修改歷史。Lean 是一種互動式定理證明器，用於將數學證明轉化為機器可驗證的形式化代碼。
社群觀察
社群討論聚焦於 AI 生成證明的可靠性與驗證機制。用戶 qoez 認為，若沒有活躍的數學社群指出錯誤，這些問題將持續存在，並引用陶哲軒（Terence Tao）的觀點指出自動數學領域的社群面臨風險。用戶 amadeuspagel 將此情況類比為 AlphaGo 從獲勝到失敗的轉變過程。用戶 chubot 質疑被撤回的三項證明是否為未經 Lean 驗證的證明，並詢問為何混合了經 Lean 驗證與自然語言的證明，同時引用 Scott Aaronson 的部落格指出，雖然部分結果有 Lean 證書，但似乎沒有人類真正理解這些證明。用戶 ijustlovemath 認為，許多完全由 AI 生成的證明在仔細檢查後可能會崩潰，因為即使在 Lean 中，也可能編譯通過但語義與預期不符，且由於證明數量龐大，發現問題可能需要數年時間。用戶 ThePhysicist 對宣稱突破整數乘法 O(n log n) 複雜度的論文表示懷疑，認為這聽起來好得不真實，可能存在細微缺陷。
