OpenAI于2026年10月6日发文，介绍内部前沿模型在数学开放问题上的新结果，并把Lean形式化证明与研究细节放到GitHub。对开发者来说，关键不在口号，而在交付物：把证明做成可被定理证明助手检查的脚本。必须立刻划清边界——给定材料没有题名、没有模型名称、没有任何成绩数字，因此不能把「有进展」读成「已解决某著名猜想」，也不能读成某项评测分数。
公开了什么、没公开什么
已确认的事实只有三条。第一，工作对象是数学中的开放问题，而不是教材习题或封闭基准。第二，结果来自内部前沿模型，材料未称其对外提供。第三，Lean形式化证明和研究细节被放到GitHub，供外部查看。
Lean的作用是把证明从自然语言主张，转成机器可检查的对象。仓库存在，意味着至少可以核验这些证明是否被Lean接受。材料没有承诺模型权重、接口、训练数据或完整推理轨迹一并开放，所以「分享数学进展」不等于「开源该模型」。把二者混为一谈，会高估可复现性。
该怎么读这条进展
形式化社区可以去仓库里看证明结构、引理依赖，以及形式化是否引入了额外假设。能力评测视角则应克制：目前只知道内部模型被用于冲击开放问题，且部分结果被形式化后公开。稳定复现、人工介入深度、失败比例，材料均未涉及，不宜外推。
开发者也不宜把GitHub仓库直接当产品组件。它被描述为证明与研究细节的存放处，不是推理服务，也不是新的数学基准测试包。在文件清单未核对前，不宜假设可训练、可评测或可接入智能体工作流。
我的判断
价值主要在公开纪律：用可机检的Lean产物，部分约束「模型会做数学」的宣传。对科研和形式化交叉方向，这比纯通告更有用。适用边界是研究归档与核验，不是通用解题产品，更不是职业数学家的替代声明。局限很硬：材料过粗，缺题单、数字、失败案例和人机分工。在读完仓库与技术说明前，只把它记作一条可核验方向的动态，不上升为能力结论。