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.部分未形式化的结果可能存在问题。我们将尽力尽快修复此类问题。 我们也在探索将这些资料托管至社区仓库的可能性。
The current catalogue contains 722 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.目前的目录包含 722 份手稿，分为 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.preprints/ 目录包含 PDF、源文件以及特定于手稿的引用和构建说明。 - 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. Many, but not all, of the manuscripts have been formalized.Lean 库和形式化目录描述了现有的形式化证明、其关联论文以及验证配置。有关额外的检查说明，请参阅 Comparator 说明。许多（但并非全部）手稿已经过形式化处理。
We are also releasing abridged summaries of the model's reasoning, covering the following results:我们还发布了模型推理的删节摘要，涵盖以下结果：
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.此固定程序的例外情况包括关于黎曼ζ函数零点无零区域的研究，以及关于 CM 阿贝尔簇的霍奇猜想（Hodge Conjecture）证明。此外，关于黎曼ζ函数 Re(s) > 11/12 零点无零区域的文稿经过人工编辑，以提高可读性。
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 代码块。