AI4Math ChronicleAI4Math 大事记

OpenAI 发布 722 篇 AI 生成数学手稿，覆盖 372 个成果族

公开仓库包含总览、手稿索引、PDF 与源码、Lean 库与形式化目录、十个精选 reasoning summaries，以及保存公开版本历史的承诺。OpenAI 明确提醒部分未形式化结果可能存在问题， 并表示后续修订将保留历史版本。

发生了什么？

2026 年 10 月 6 日，OpenAI 公开发布由未公开内部模型产生的数学手稿与证明产物集合。 仓库记录共有 722 篇手稿、372 个成果族，来源于约 4,000 个被提出的研究问题。 OpenAI 表示绝大多数结果使用统一流程产生，平均每项结果消耗约三小时 ChatGPT Pro thinking compute。集合覆盖数学与理论计算机科学多个方向中的开放问题解决或推进， 其中许多但并非全部手稿配有 Lean 形式化。

公开仓库包含总览、手稿索引、PDF 与源码、Lean 库与形式化目录、十个精选 reasoning summaries，以及保存公开版本历史的承诺。OpenAI 明确提醒部分未形式化结果可能存在问题， 并表示后续修订将保留历史版本。此次发布此前与独立的 Advisory Group on Mathematics and Artificial Intelligence 进行了沟通；AGMAI 随后公开声明，其建议不构成对数学结果 或 OpenAI 流程的背书，并把本次发布视为更广泛人类理解与共同体评估的开始。

为什么重要？

本事件改变了前沿 AI 生成数学进入公共研究生态的规模，把批量研究生成、形式验证基础设施、 provenance 披露、引用与修订机制以及治理咨询集中到一次发布中。它同时带来新的编辑问题： 整体事件可以具有很高历史重要性，但其中各个结果的验证状态可能差异巨大，仍需分别接受 专业审查。

重要性说明：该发布被列为 Historical Milestone，因为它把 AI 生成研究数学从少量旗舰成果推进到 前所未有规模的公开成果库。OpenAI 一次性公开 722 篇手稿、372 个成果族，并配套 大规模 Lean 形式化计划、推理摘要、算力与流程披露、持久化公开产物及版本修订承诺。 其历史意义来自发布规模和面向学术共同体的公开接口，而不是把库内每一项数学主张都 视为已经正确验证。

历史脉络

更早进展
后续进展

—

相关里程碑

主要证据

证据与状态一览

重要性
H1 · 历史里程碑
验证状态
核验中
证据等级
E3 · 可检查工件
AI 角色
尚不明确
形式保障
有形式化工件

如何理解这些标签？ →

贡献与验证

数学新颖性
新结果
接口
非形式化, 形式化, 符号, 混合
AI 贡献
OpenAI 将未公开内部模型描述为该成果集的主要产生者，并表示绝大多数结果来自统一评测流程。 但 372 个成果族中的人类贡献、编辑、检查与形式化流程并不完全一致，因此 Chronicle 只在整体层面记录强 AI 生成属性，不为每项结果统一指定同一套模型—人类分工。
人类贡献
人类负责选择和提出研究问题、把结果整理成成果族和手稿、准备发布基础设施、进行不同程度 的编辑与验证，并协调形式化和外部咨询。公开仓库也明确标记了少数偏离统一生成流程的例外。
验证状态
核验中 · E3 · 可检查工件 · 有形式化工件
最后审阅
2026-10-07

技术细节

系统
openai-internal-math-model, lean, comparator
机构
openai, advisory-group-on-mathematics-and-artificial-intelligence
数学问题
—
方法
large-scale-mathematical-discovery, research-problem-evaluation, formal-verification, provenance-disclosure, responsible-release

全部来源与工件

验证历史

  • 2026-10-06 · 核验中 · E3 · 可检查工件

    OpenAI 公开发布手稿、源码以及大规模形式化库。仓库明确说明不同成果处于不同验证阶段， 并非全部手稿都有 Lean 形式化，而且部分未形式化结果可能存在问题。

  • 2026-10-06 · 核验中 · E3 · 可检查工件

    AGMAI 独立确认了其咨询角色以及公开审查的重要性，同时明确不对数学主张背书，也不认证 OpenAI 已完全遵守其建议。因此 Chronicle 将整体发布的历史意义与逐项数学验证严格分离。

更正

当前没有记录的更正。