外部精选
Sharing AI progress in mathematics
本文来自外部来源,不是黄奕彬的原创文章。本站提供原文入口,并在采集端生成 AI 结构化摘要、解读与中文翻译(如有),一切以原文为准。
阅读原文(openai.com)结构化摘要 AI 生成
背景与问题
OpenAI 宣布发布由其内部前沿模型(internal frontier model)产生的一批新数学成果。文章面对的背景问题是:如何以符合数学界规范、可被社区接受的方式发布 AI 生成的数学结果。
为此 OpenAI 咨询了设于 Institute for Advanced Study 的独立“数学与人工智能咨询小组”,依据其建议与公开推荐来确定发布方式。
方法或内容
本次通过 GitHub 仓库发布这些数学结果,并附论文修订与引用协议;同时分享许多证明的 Lean 形式化(Lean 被原文描述为允许计算机检查数学证明的编程语言),并承诺随获取进展持续更新仓库。
为促进透明与开放,还公开取得结果的补充细节:10 份模型推理摘要、以 ChatGPT Pro 用量折算的计算开销估计、以及尝试问题数量的统计。此外宣布将资助围绕理解 AI 重大成果的系列研讨会、会议与专项计划,并正致力于负责任地发布产出这些结果的模型。
关键发现 / 结果
具体数据点:平均每个结果消耗约相当于 3 小时 ChatGPT Pro thinking 的计算量;仓库包含 10 份模型推理摘要、计算开销估计与尝试问题数统计;许多证明提供 Lean 形式化。具体数学定理/结论的名称与内容:原文未说明(正文可能被截断)。资助金额、研讨会细节、模型名称与发布时间:原文未说明。另提及正在探索符合该咨询小组指引的其他社区托管发布渠道。
结论与意义
作者期望这些进展推动人类知识前沿并促进数学进步;将继续在数学与其他科学上评估内部前沿模型,以加速开发推进这些领域的工具;将继续采纳社区反馈并更新未来重大科学进展披露的标准。适用边界:文中结论多为意向与承诺(如资助计划、负责任地发布模型、改进论文质量),未给出时间表或验证结果。
AI 解读 AI 生成
方法:按「时空变量」分析(时间 / 空间 / 变量,严格区分包含、相关与因果),对象包括原文作者、署名人员与关键技术及其实际原理;结论用「元反空」(元思考、反思考、空思考、综合)整理。
时间:何时发生,现在是否仍成立
来源日期为 2026-10-06。GitHub 仓库发布、Lean 形式化、10 份推理摘要与计算统计是当时已发生的动作;“继续更新仓库”“资助研讨会/会议/专项计划”“负责任地发布模型”均为无时间表的前瞻承诺。现在是否仍成立无法从原文判断:仓库内容可能已更新,承诺事项状态原文未说明。
空间:谁的环境 / 场景
适用场景为面向数学研究社区的成果披露,载体是 GitHub 仓库(并探索符合 IAS 咨询小组指引的其他社区托管渠道)。产出结果的模型是 OpenAI 内部前沿模型,原文未给出模型名称、版本或部署形态;计算量以 ChatGPT Pro 用量折算,仅为度量单位,不表示产品功能变化。Lean 形式化面向可用计算机检查证明的环境。
变量:实际改变了什么
相对此前实际改变:发布渠道改为带论文修订与引用协议的 GitHub 仓库;新增透明度材料——10 份模型推理摘要、按 ChatGPT Pro 折算的计算开销估计、尝试问题数统计;新增许多证明的 Lean 形式化并承诺持续补充;承诺未来通过引用、数学表述与结果呈现改进论文质量,并资助相关研讨活动。价格或产品结构变化:原文未说明。
区分:包含 ≠ 相关 ≠ 因果
包含/相关:Lean 形式化、推理摘要、计算统计均属于 GitHub 仓库发布内容的一部分;与 IAS 咨询小组的咨询属于相关且被用作参考。有明确表述的因果:咨询小组的建议与公开推荐被用来指导本次发布方式(原文自述)。
无因果证据的部分:“推动人类知识前沿”“赋能科学家”“加速开发工具”均为目标或动机表述;“平均约 3 小时 ChatGPT Pro 计算量”是描述性统计,不构成计算量与成果质量之间的因果证明。
对象:作者/署名与关键技术原理
作者/署名:结构化作者字段为空,原文未标注。涉及的关键技术:
- OpenAI 内部前沿模型,产出这批数学结果,其名称、版本、训练与推理原理原文均未说明。
- Lean——原文描述为“一种允许数学证明被计算机检查的编程语言”,用于将许多证明形式化以便机器验证。
- 计算度量以 ChatGPT Pro 使用量(Pro usage / thinking)折算。
10 份模型推理摘要与尝试问题统计是了解结果取得过程的补充材料,其具体内容原文未展示。
元反空综合结论
元:这篇内容本质在解决“AI 生成的数学成果如何可信、合规地向数学界披露”的流程与规范问题,而非证明某个数学定理本身。
反:最可能失效或有边界的部分是全部无时间表的前瞻承诺(持续更新仓库、资助研讨会、负责任发布模型、改进论文质量),以及“平均约 3 小时 ChatGPT Pro 计算”这类依赖具体模型与配置的统计;成果本身的数学正确性在本文中未展示,需依赖 Lean 机器验证与社区审阅,二者均不在本文范围内。
空:去掉宣传叙事后剩下的必要事实为——发布了一个含数学结果的 GitHub 仓库,附修订与引用协议;提供许多证明的 Lean 形式化;公开 10 份模型推理摘要、计算开销估计(平均约 3 小时 ChatGPT Pro thinking)与尝试问题统计;发布方式参考了 IAS 数学与 AI 咨询小组的建议。
综合结论:这是一份确立披露实践与承诺的公告,其可信度锚点在 Lean 可机器检查与透明度材料,但具体数学贡献与后续承诺的落实情况均需以仓库与未来披露为准,原文未提供可独立核验的定理内容。
中文译文 AI 生成
我们正在发布由一个内部前沿模型产生的一系列广泛的数学新成果。
在我们寻求改进如何与数学界分享成果的过程中,我们一直在与 Institute for Advanced Study 独立的 Advisory Group on Mathematics and Artificial Intelligence 进行咨询,以制定最佳实践,并且我们参考了他们的建议和公开建议(在新窗口中打开)来指导我们如何发布这些成果。
在本次发布中,我们将成果发布在一个 GitHub 仓库中,并附有论文修订与引用的规范。我们还在继续探索符合该委员会准则的其他由社区托管的发布替代方案,用于本次发布。对于未来的发布,我们承诺通过引用、数学阐述以及成果的呈现方式进一步提升论文质量,以便于更好地理解。
作为 GitHub 仓库的一部分,我们正在分享许多证明在 Lean 中的形式化,Lean 是一种允许用计算机检验数学证明的编程语言。随着我们获得更多形式化成果,我们将持续更新该仓库。为促进科学透明与开放,我们还在仓库中发布了关于我们如何获得这些成果的更多细节。
这些细节包括 10 份关于模型推理的总结、以 ChatGPT 上 Pro 使用量计算的算力消耗估算,以及关于尝试问题数量的统计数据。平均每项成果使用了大约相当于三小时 ChatGPT Pro 思考的算力。我们希望这一进展能推动人类知识的前沿,并促成数学的进一步发展。
我们将资助一系列围绕理解 AI 产生的重大成果的研讨会、会议和特别项目——我们将在近期分享更多相关信息。我们希望以最先进的能力直接赋能科学家,并正在努力负责任地发布产生这些成果的模型。这正是为什么在数学和其他科学领域继续评估我们的内部前沿模型十分重要的原因,这样我们才能加快开发推动这些领域发展的工具。
我们将继续根据社区反馈采取行动,并更新我们未来披露重大科学进展的标准。
展开原文提取正文(采集端自动提取,可能有缺失)
We’re releasing a broad range of new mathematical results produced by an internal frontier model.As we look to improve how we share results with the math community, we’ve been consulting with the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study(opens in a new window) to develop best practices, and we have drawn on their advice and public recommendations(opens in a new window) to inform how we release these results. For this release, we’re publishing the results in a GitHub repository, with protocols for paper revisions and citations. We’re continuing to explore other community-hosted alternatives for this release which meet the committee’s guidelines. For future releases, we are committed to further improving the quality of the papers via the citations, mathematical exposition, and presentation of the results for better understanding.As part of our GitHub repository, we are sharing formalizations of many of the proofs in Lean, a programming language that allows mathematical proofs to be checked by a computer. We will update the repository with more formalizations as we obtain them. To promote scientific transparency and openness, we are also publishing additional details about how we obtained the results in the repository. These include 10 summaries of the model’s reasoning, estimations of compute spent in terms of Pro usage on ChatGPT, and statistics about the number of attempted problems. The average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking.We want this progress to push the frontier of human knowledge and enable further progress in mathematics. We will be funding a series of workshops, conferences, and special programs around the understanding of major results produced by AI—we will share more on this in the near future. We want to directly empower scientists with state-of-the-art capabilities and are working to responsibly release the model that produced these results. This is why it is important to continue to evaluate our internal frontier models on mathematics and other sciences, so we can accelerate developing the tools to advance those fields. We will continue to act on feedback from the community and update our standards for future disclosures of major scientific advancements.
原文入口
阅读原文(openai.com)原文将在新窗口打开。收录时间不是内容更新时间;正文、译文与解读的版权归原作者/来源所有,本站仅作个人阅读辅助并保留原文入口;页面时间均为北京时间。
了解来源批准与收录规则