openai/math

722 篇 AI 数学手稿 + Lean 形式化证明，前沿实验室第一次把”机器数学”完整摊在阳光下

项目速览

项目 内容
仓库 openai/math
语言 Lean（形式化证明）+ LaTeX（手稿源码）
Stars 约 1.52 万（2026-10-19 GitHub API 口径），Forks 1,770
协议 Apache-2.0
状态 2026-10-06 创建并发布，10 月中旬仍在更新 Lean 形式化
热度 发布即登上 GitHub Trending 与全球科技媒体头条；配套 IAS 顾问组发布协议与 Simons 基金会 500 万美元资助计划

它想解决什么问题

前沿 AI 实验室用未发布的内部模型在开放数学问题上”刷”出了成果，但数学界既审不过来，也无法验证真伪——这是 2026 年数学界与 AI 实验室之间最大的信任危机。OpenAI 的应对是把整个成果库完整开源：一个内部前沿模型在约 4,000 道开放研究问题上的产出，收敛为 722 篇手稿、372 个结果族（family，即围绕一个主结果的相关论文、推论与替代证明的集合），连同 Lean 形式化证明、推理摘要、算力消耗估算一起放进 GitHub。

这不是一篇论文，而是一个可检索、可引用、可机器校验的”机器数学”档案库——数学界第一次能逐条检查 AI 到底证明了什么、没证明什么。

核心机制拆解

1. 结果族（family）组织法。 722 篇手稿按 372 个结果族归类，每个族包含主结果、伴随论证、推论或替代证明，并按数学学科分类。导航从 overview 总览开始，经 CONTENTS.md 手稿地图定位到单篇——把”AI 一口气吐了七百篇论文”这个审稿噩梦，拆成了可逐族消化的结构。

2. Lean 形式化是硬通货。 约 42% 的主结果已附 Lean 形式化（372 个族中 235 个附 Lean 链接，formalization.yaml 列出 162 篇主结果已形式化），可用 leanprover/comparator 逐行机器校验。README 明确警告：未形式化的结果可能有问题，OpenAI 承诺持续补形式化并快速修复。这种”分级信任”设计——形式化的算已验证，未形式化的算待审——正是 IAS 顾问组建议的核心。

3. 生产过程全透明。 绝大多数结果由同一未发布内部模型、同一固定流程产出，平均每个结果消耗约 3 小时 ChatGPT Pro 思考算力；模型共被投放约 4,000 道问题。两个例外被单独点名：黎曼 ζ 函数 Re(s) > 11/12 无零区域的写作经过人工编辑润色，CM 阿贝尔簇上 Hodge 猜想的证明走了不同流程。10 份推理摘要公开，覆盖 π 的无理性指数、Mahler 猜想、自由群因子同构、三维相对论 Vlasov–Maxwell 系统等结果。

4. 版本与引用协议。 仓库保留完整发布历史，修订记录为新版本、旧版本持续可访问；每篇手稿目录自带 BibTeX 引用块。这套协议直接回应了 IAS 数学与 AI 顾问组 9 月 29 日的公开建议（收到 600+ 数学界回复）：结果应存入不受 AI 实验室控制的学术仓储、带持久可引用标识、公开模型名与提示词与推理链、证明尽量形式化。

5. 生态配套。 OpenAI 另向 Simons 基金会新倡议资助 500 万美元，支持数学家研讨、理解并发展 AI 产出的结果，并向受资助研究者开放模型与算力。

安装与上手

这不是软件，是档案库。典型用法：

1
2
3
4
5
git clone https://github.com/openai/math
# 1. 读 overview.pdf / overview.tex 了解 372 个结果族
# 2. 用 CONTENTS.md 手稿地图定位感兴趣的结果
# 3. preprints/ 下取 PDF、源码与单篇引用说明
# 4. lean/ 目录取形式化证明，按 Comparator 说明校验

对数学研究者，真正的入口是 lean/formalization.yaml——它告诉你哪些主结果已经机器验证、验证配置是什么。

点评

亮点是透明度设计本身：算力估算、推理摘要、失败与例外、修订协议、分级信任（形式化 vs 未形式化），每一条都踩在顾问组建议的点上。在”AI 数学冲击波”（《纽约时报》报道其震动数学界，《科学美国人》称”数百个新结果砸向一个已经震惊的领域”）的背景下，这是目前唯一一个把机器数学成果放到公共、可校验、可引用基础设施上的大规模发布。Apache-2.0 与 BibTeX 块意味着这些结果可以立即进入正常的学术引用流。

局限同样醒目：全部结果未经同行评审；约 58% 的主结果尚无 Lean 形式化，README 自承”部分未形式化结果可能有误”；生成模型本身未开放，外部无法复现”3 小时 Pro 算力”的产出过程；顾问组明确”不认可在专有模型上测试高级数学问题”的做法，社区对”发布即营销”的质疑并未消散。验证负担现在压在数学家肩上——这正是 Simons 资助要缓解的问题。

适合人群：关注 AI for Math 的研究者、Lean/形式化验证社区、想跟踪”机器能证什么”边界的量化与数学工作者，以及所有关心 AI 科学成果该如何负责任发布的人。