OpenAI开源内部模型数学解题成果及Lean证明
openai/math
展示未发布模型在前沿数学领域的硬核推理能力，附带可复现的算力消耗数据与形式化验证进度，对评估模型极限极具参考价值。
GitHub repository created 2026-10-06 · 14768 stars in 7.7 days (about 1914 a day) · Lean
GitHub 仓库创建于 2026-10-06 · 7.7 天内获得 14768 颗星（平均每天约 1914 颗）· Lean
Readme
自述文件
This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.
该仓库包含由 OpenAI 内部模型生成的数学手稿及辅助证明工件。
As part of model development, we evaluate our models on open research problems. We expanded these evaluations after performance on our existing mathematical evaluations saturated. Some outputs build upon earlier results produced by the models.
作为模型开发的一部分，我们在开放研究问题上对我们的模型进行评估。在现有数学评估的性能饱和后，我们扩展了这些评估。部分输出建立在模型先前产生的结果之上。
This collection includes results at different stages of verification. Not all have accompanying Lean formalizations. We will continue to update this repository with Lean formalizations as we obtain them.
本合集包含处于不同验证阶段的结果。并非所有结果都附有 Lean 形式化证明。随着我们获取到 Lean 形式化证明，我们将继续更新此仓库。
Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly. We are also exploring community-hosted repositories for these materials.
部分未形式化的结果可能存在缺陷。我们将努力尽快修复此类问题。 我们也在探索社区托管的存储库来存放这些材料。
Navigating the collection
浏览合集
The current catalogue contains 719 manuscripts organized into 372 families. A family groups related papers, which may include a principal result, companion arguments, consequences, or alternative proofs. Each family is classified by mathematical discipline.
当前目录包含 719 份手稿，分为 372 个家族。一个家族将相关的论文分组，可能包括主要结果、配套论证、推论或替代证明。每个家族均按数学学科进行分类。
- Start with the overview for descriptions of the families. - Use the manuscript map to find individual papers and their supporting materials. - The `preprints/` directory contains PDFs, source files, and manuscript-specific citation and build instructions. - The Lean library and formalization catalogue describe the available formal proofs, their associated papers, and verification configurations. See the Comparator instructions for additional checking instructions. The repository has ~42% top-line results formalized. - Updates to the repo are described in the history.
- 从概述开始了解各家族的描述。 - 使用手稿地图查找单个论文及其支持材料。 - `preprints/` 目录包含 PDF、源文件以及特定于手稿的引用和构建说明。 - Lean 库和形式化目录描述了可用的形式化证明、其关联的论文以及验证配置。请参阅 Comparator 说明以获取更多检查指令。该仓库约有 42% 的主要结果已实现形式化。 - 仓库的更新情况详见历史记录。
Reasoning summaries
推理摘要
We are also releasing abridged summaries of the model's reasoning, covering the following results:
我们还发布了模型推理的简化摘要，涵盖以下结果：
| Family | Subject | ||
|---|---|---|---|
| 007 | Ordinary two-point correlations of multiplicative functions | ||
| 017 | The irrationality exponent of π | ||
| 087 | Symmetric and general Mahler conjectures | ||
| 102 | Ordinary NP-hardness at the basic semidefinite threshold | ||
| 159 | Quasipolynomial bounds for arithmetic progressions | ||
| 197 | Kaplansky's direct-finiteness conjecture in characteristic two | ||
| 221 | The Mézard–Parisi formula for diluted spin glasses | ||
| 271 | Spontaneous magnetization in the quantum Heisenberg ferromagnet | ||
| 287 | Isomorphism of free group factors | ||
| 362 | The three-dimensional relativistic Vlasov–Maxwell system |
| 家族 | 主题 | ||
|---|---|---|---|
| 007 | 乘性函数的普通两点相关性 | ||
| 017 | π 的无理性指数 | ||
| 087 | 对称及一般 Mahler 猜想 | ||
| 102 | 基本半定阈值处的普通 NP 困难性 | ||
| 159 | 算术级数的拟多项式界 | ||
| 197 | 特征二域中 Kaplansky 的直接有限性猜想 | ||
| 221 | 稀释自旋玻璃的 Mézard–Parisi 公式 | ||
| 271 | 量子海森堡铁磁体中的自发磁化 | ||
| 287 | 自由群因子的同构 | ||
| 362 | 三维相对论性 Vlasov–Maxwell 系统 |
How the results were produced
结果的生成方式
The vast majority of results were obtained with the same procedure using an unreleased internal OpenAI model. On average, each result used three hours of ChatGPT Pro thinking compute with that model. Over the course of the evaluation, the model was posed approximately 4,000 problems. Aggregating the output into result families and manuscripts and requiring an appropriate level of significance led to the catalog outlined above.
绝大多数结果均使用相同的流程，基于一个未公开的 OpenAI 内部模型获得。平均而言，每个结果都使用了该模型三小时的 ChatGPT Pro 推理计算资源。在整个评估过程中，该模型共解决了约 4,000 个问题。将输出汇总为结果家族和手稿，并要求达到适当的显著性水平，从而得出了上述目录。
Exceptions to this fixed procedure include work on a zero-free region for the Riemann zeta function and proof of the Hodge Conjecture for CM abelian varieties. Additionally, the writeup for the Re(s) > 11/12 zero-free region for the Riemann zeta function was human edited for readability.
此固定流程的例外包括对黎曼ζ函数零自由区域的工作，以及对复乘阿贝尔簇霍奇猜想的证明。此外，关于黎曼ζ函数 Re(s) > 11/12 零自由区域的撰写内容经过了人工编辑以提高可读性。
Versions and citations
版本与引用
We will preserve the public release history of this collection. Corrections and revisions will be recorded as new versions, with previously released versions remaining accessible.
我们将保留本合集的公开发布历史。更正和修订将记录为新版本，先前发布的版本仍将可访问。
To cite the individual manuscript, use the BibTeX block in its directory.
要引用单篇手稿，请使用其目录中的 BibTeX 代码块。
更进一步：量化金融体系
看懂新闻只是起点——沿量化金融路径，把它变成能交付的工程能力