Sharing AI progress in mathematics — OpenAI 用内部前沿模型攻数学开放问题，并公开 Lean 形式化证明

• OpenAI 发布了一批针对数学开放问题的新结果，来源是内部的前沿模型，而非公开可用的模型版本。对 agent 开发者而言，这意味着能力上限与可调用工具之间存在落差，评估时需区分内部与对外模型。
• 配套的 Lean 证明形式化被一并公开，说明自然语言结论之外还提供了可机器校验的产物。对工具链的含义是：形式化验证正成为 AI 数学输出的可信度锚点，值得纳入 agent 的产出校验环节。
• 研究细节同步发布在 GitHub 上，供外部查看与复用。对开发者的含义是，这类发布把模型能力展示与可复现材料绑定，便于在自有流程中对照和借鉴。

原文：Sharing AI progress in mathematics · 作者 OpenAI