OpenAI公布了一批由其内部前沿模型产生的数学结果，并在公开仓库中提供论文、引用与修订规则，以及部分证明的Lean形式化版本。Lean是一种可由计算机检查证明步骤的编程语言。对机器辅助数学研究而言，这个发布方式比只展示结论多了一层可检验性：研究者可以检查形式化证明是否通过，也能追踪仓库中的文本修订。
公司还分享了十份模型推理摘要、尝试题目数量的统计，以及每项结果所用计算量的估算。OpenAI称平均结果耗费的算力大致相当于ChatGPT Pro进行约三小时的思考。这个换算帮助读者把模型研究和资源成本联系起来，但它仍是公司提供的估计，不能简单当成数学家实际工作的等时比较。
形式化检查是有力工具，不是价值判断的替代品
Lean可以验证某些形式系统内的证明步骤是否符合规则，却不能单独回答一个结果是否重要、问题是否值得研究、定义是否贴合数学家关心的对象。论文的表达、背景文献、推理脉络与对领域的贡献，仍需要同行理解和审阅。OpenAI也表示，正在参考数学与人工智能独立顾问组提出的规范，并计划资助围绕AI数学成果的讨论活动。
这次发布值得留意的部分，是研究组织开始说明如何分享模型生成的科学结论：公开仓库、证明形式化、推理摘要和计算统计，都能让后续评议更具体。但开放并不意味着已获同行认可。读者还应查看每个结果是否能被独立复现，形式化版本覆盖了结论的哪些部分，以及摘要能否支持从假设到论证的完整追踪。
对数学研究者而言，模型可能擅长搜索长推理路径或生成候选证明，形式化工具则提供机器核验的接口。两者结合能否稳定地产生新知识，取决于错误发现、反例搜索、独立复核和清晰表达是否跟得上。最值得期待的不是模型“替代数学家”，而是它让更多猜想与证明能够被提出、检查和讨论。