OpenAI 於 2026 年 10 月 6 日公開一批由內部 frontier model 產生的數學結果，並把論文、Lean formalizations 及額外研究細節放到 GitHub repository。這次發布的重點不只是「模型解到甚麼」，也包括如何讓數學社群閱讀、引用、修改和以電腦檢查這些結果。
Lean 是一種可由電腦檢查數學證明的程式語言。OpenAI 表示，repository 會分享許多證明的 formalization，並在取得更多結果後持續更新。形式化可以把某些證明的邏輯交給 proof checker 驗證，但它不會自動判斷問題是否重要、方法是否有洞察力，亦不取代數學家對敘述和背景的審閱。
為改善發布透明度，OpenAI 表示會提供 10 份 model reasoning summaries、以 ChatGPT Pro 使用量等值估算的 compute，以及模型嘗試過多少問題的統計。文章給出的平均結果約使用相當於三小時 ChatGPT Pro thinking 的計算量。OpenAI 亦表示曾向 Institute for Advanced Study 的 Advisory Group on Mathematics and Artificial Intelligence 徵詢發布做法，並以其建議及公開 recommendations 作為參考。
OpenAI 同時在 repository 放入 paper revision 和 citation protocols，並表示會繼續尋找符合委員會指引的社群託管方案。這種做法把 frontier model 的數學工作由封閉示範轉成一個可追蹤的研究資產：外部讀者可以看到版本、來源、形式化程度和計算成本，而不是只接收一段沒有上下文的結論。
但公開結果仍需要獨立專家核查。形式化的 proof 可能只涵蓋其中一部分，模型的 reasoning summary 亦不是完整可重播的思考紀錄；嘗試題目數和平均計算量也不能直接轉換成研究效率或學術影響。比較可靠的閱讀方式，是把 Lean 檢查、論文敘述、引用、結果重現和專家評議分開看。
對 AI research workflow 而言，今次發布示範一個值得延伸的模式：模型負責探索和產生候選證明，人類及工具負責定義問題、檢查形式化、整理引用和判斷結果。它提高可驗證性，但仍然需要持續披露限制，尤其是哪些結果已完整 formalize、哪些仍是研究草稿，以及計算成本如何影響可重現性。
