openai/math（OpenAI 模型数学手稿库）

OpenAI 公开的数学手稿与证明材料库：内容由一个未发布的内部模型在开放研究问题评测中产出，部分附 Lean 形式化证明。 星数 15690（+141 / 24h） **理由** - 官方称目前收录 721 篇手稿、分 373 个结果族，约 42% 的主结果已有 Lean 形式化，另附 10 个结果的模型推理摘要 - 10 月 26 日更新新增两篇带 Lean 形式化的手稿，其中一篇宣称给出确定性亚指数时间算法、推翻指数时间假设（ETH）；官方称由 Impagliazzo、Paturi、Williams 牵头的独立小组将审查该证明 - 官方称多数结果按同一流程产出：共向模型提出约 4000 个问题，每个结果平均用 3 小时 ChatGPT Pro 思考算力 - 官方定位是“原始研究数据”而非正式论文，撤稿和修订都记录在 history.md，旧版本保留可查 **用法** - 先读 overview.pdf（各结果族简介），再用 CONTENTS.md 找具体手稿；PDF 与源文件在 preprints/ - 形式化证明看 lean/README.md 和 lean/formalization.yaml，按 lean/ComparatorChallenges/README.md 自行复核 - 引用单篇手稿用其目录里的 BibTeX；许可证为 Apache-2.0（仓库 LICENSE） **风险** - 官方承认未形式化的结果可能有错；10 月 7 日已因符号错误撤回 3 篇相互依赖的手稿 - ETH 相关结论尚在独立审查，结论未经学界确认 - 产出模型未发布，无法用同一模型复现；这是论文与证明数据，不是可运行的工具 [打开](https://github.com/openai/math)