OpenAI 发布了一个由内部模型生成的数学手稿及证明材料仓库。作为模型开发评估的一部分，团队在现有数学评估性能饱和后扩展了评估范围，部分输出基于模型此前产生的成果。

该合集包含处于不同验证阶段的结果，并非所有结果均附有 Lean 形式化证明。随着新证明的获得，仓库将持续更新。针对部分未形式化结果可能存在的瑕疵，团队正努力修复，并探索建立社区托管存储库。

数据集概览

当前目录收录 722 份手稿，划分为 372 个“家族”（families）。每个家族按数学学科分类，聚合了主要结果、辅助论证、推论或替代证明等相关论文。用户可通过概述了解各家族描述，利用手稿地图查找单篇论文及支持材料。

preprints/ 目录提供 PDF 文件、源文件及特定引用和构建说明。Lean 库和形式化证明目录则描述了可用的形式化证明、关联论文及验证配置。许多（非全部）手稿已完成形式化，额外检查指令可参阅 Comparator 说明。

重点成果摘要

发布的模型推理精简摘要涵盖以下代表性成果：

  • 家族 007：乘性函数的普通两点相关性
  • 家族 017：π 的无理性指数
  • 家族 087：对称及一般 Mahler 猜想
  • 家族 102：基本半定阈值处的普通 NP 困难性
  • 家族 159：算术级数的拟多项式界
  • 家族 197：特征二域中的 Kaplansky 直接有限性猜想
  • 家族 221：稀释自旋玻璃的 Mézard–Parisi 公式
  • 家族 271：量子海森堡铁磁体中的自发磁化
  • 家族 287：自由群因子的同构
  • 家族 362：三维相对论性 Vlasov–Maxwell 系统

生成机制与例外

绝大多数成果通过同一流程，由一个未发布的 OpenAI 内部模型生成。平均而言，每项成果消耗该模型三小时的 ChatGPT Pro 推理算力。在评估过程中，模型处理了约 4,000 个问题，输出经聚合并按重要性筛选形成上述目录。

该固定流程存在例外：黎曼 zeta 函数零自由区域的工作，以及复乘法阿贝尔簇霍奇猜想的证明。其中，关于黎曼 zeta 函数 Re(s) > 11/12 零自由区域的内容经过人工编辑，以提升可读性。

版本管理与引用

OpenAI 将保留本合集的公开发布历史，更正和修订将以新版本记录，旧版本仍可访问。如需引用单份手稿，请使用其目录中提供的 BibTeX 块。