OpenAI在其官方博客发布消息，介绍了内部前沿模型在数学开放问题上取得的新进展，并将Lean证明形式化及相关研究细节上传至GitHub。

发生了什么

根据OpenAI博客，此次公布的内容包含内部前沿模型针对数学开放问题的求解结果。

同时，该机构在GitHub上分享了Lean证明形式化文件以及对应的研究细节，供外界查阅。

OpenAI将这一动作描述为对外分享其在数学领域的AI进展。

为什么重要

数学开放问题长期被视为检验人工智能推理能力的试金石。将模型结果与Lean形式化证明一同公开，有助于研究者验证结论的正确性与可复现性。

形式化证明的公开，也使相关结果能够被社区直接检查、引用与进一步拓展，降低了对非形式化描述的依赖。

来源：Sharing AI progress in mathematics（发布于 2026-10-06）