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、哪些仍是研究草稿，以及计算成本如何影响可复现性。
