PSI 用非公開 Anthropic 模型攻克阿倫森-安拜尼斯猜想：量子計算 18 年懸案告破
PSI 團隊藉助非公開的 Anthropic 模型與 Lean 驗證器，僅用 3 天便完整證明了懸而未決 18 年的阿倫森-安拜尼斯猜想。該定理正式確認量子計算機處理無規律隨機資料時無法實現指數級加速，徹底為量子計算劃定了嚴格的數學邊界。
Lean
OpenAI 公佈內部模型數學成果：生成 722 篇論文，捐資 500 萬支援驗證
OpenAI 公開內部前沿模型生成的 722 篇數學論文，涵蓋 372 個研究成果，並在 GitHub 提供 Lean 形式化證明。平均每個成果消耗約 3 小時 ChatGPT Pro 算力。10 月 15 日，OpenAI 還向西蒙斯基金會資助 500 萬美元，協助數學界驗證這些 AI 成果。