我们的 GitHub 数学仓库已更新，新增了 6 项 Lean 形式化、19 项修改和 3 项撤回。目前仓库中约 42% 的核心结果已完成形式化。我们将持续更新仓库，加入新的形式化成果，并修正发现的勘误。

https://t.co/HI6otY2NTO

openai/math

来源：https://github.com/openai/math

说明

本仓库包含由 OpenAI 内部模型生成的数学手稿及配套证明产物。

作为模型开发的一部分，我们在开放研究问题上对模型进行了评测。在现有的数学评测基准性能趋于饱和后，我们扩大了评测范围。部分输出是在模型早期成果的基础上进一步发展而来的。

本合集收录了处于不同验证阶段的结果。并非所有结果都附有对应的 Lean 形式化证明。随着新的形式化成果的获得，我们会持续更新本仓库。

部分尚未形式化的结果可能存在一些问题。我们将努力尽快修复这类问题。 我们也在探索将这些材料托管在社区仓库中。

如何浏览本合集

当前目录共收录 719 篇手稿，归为 372 个“族“（family）。一个族包含相关联的论文，可能包括一个主要结果、配套论证、推论或替代证明。每个族按数学学科分类。

• 从 概览 开始，了解各族的介绍。
• 使用 手稿地图 查找各篇论文及其配套材料。
• preprints/ 目录包含 PDF、源文件以及各手稿的引用和构建说明。
• Lean 库 和 形式化目录 描述了可用的形式化证明、对应的论文及验证配置。关于额外的检查说明，请参阅 Comparator 使用指南。仓库中约 42% 的核心结果已完成形式化。
• 仓库的更新记录见 历史。

推理摘要

我们同时发布了模型推理过程的精简摘要，涵盖以下结果：

结果是如何产出的

绝大多数结果都是使用同一套流程，通过一个尚未发布的 OpenAI 内部模型获得的。平均而言，每个结果使用了约三小时的 ChatGPT Pro 思考算力。在整个评测过程中，模型共被提出了约 4,000 个问题。我们将输出聚合为结果族和手稿，并要求达到相应的显著性水平，最终形成了上述目录。

这一固定流程的例外包括关于 Riemann zeta 函数零点无区域的工作，以及关于 CM 阿贝尔簇 Hodge 猜想的证明。此外，Riemann zeta 函数 Re(s) > 11/12 零点无区域的文稿经过了人工编辑以提高可读性。

版本与引用

我们将保留本合集的公开发布历史。更正和修订将以新版本的形式记录，已发布的旧版本将保持可访问。

引用单篇手稿时，请使用其目录中的 BibTeX 块。