722 篇手稿怎么吃？OpenAI 数学仓库的 GitHub 食用指南

【免费下载链接】math项目地址: https://gitcode.com/gh_mirrors/math58/math

2026 年 9 月底到 10 月初，数学界被一条消息震动了：OpenAI 一次性公开了数百篇由其内部模型产出的数学手稿，媒体用"数学大爆炸"、"数学的广岛时刻"来形容这场冲击——准黎曼假设被证明、CM 阿贝尔簇上的有理 Hodge 猜想被攻克、Unique Games 猜想告破……更关键的是，这些成果不是停留在 PDF 里，而是连带一套 Lean 形式化工程一并放进了 GitHub。社区的情绪复杂：兴奋于"AI 一夜投下 722 篇手稿"，警惕于"其中有多少能被逐行验证"。

这份仓库（README.md）就是那 722 篇（发布后撤回 3 篇，当前目录为 719 篇）手稿的完整载体。但 719 篇、372 个结果家族的体量，对任何人都是"打开即迷路"。本文不讨论 AI 数学的哲学争议，只做一件事：把这份仓库的目录结构拆开，给出筛出名题、读懂形式化证据、把手稿转化成研究选题的可执行路径。

仓库目录与文件组织速览

先建立全局坐标。仓库根目录只有四个入口文件，加上一个巨大的lean/目录：

四个入口文件分工极其清晰：README 回答"这些东西怎么来的"，CONTENTS 回答"里面有什么"，history 回答"哪些不可信或已修订"，lean 回答"哪些能机器验证"。

结果如何产生：一个值得先读的数字段

README.md 用一小段话交代了全部生产背景，信息密度极高：

• 绝大多数结果由同一个未发布的内部 OpenAI 模型产出；
• 每项结果平均消耗3 小时 ChatGPT Pro thinking 算力；
• 整个评估周期内模型被提出了约4,000 道问题，经聚合、分族、显著性筛选后沉淀为当前目录；
• 特别声明：ζ 函数的零区域、CM 阿贝尔簇 Hodge 猜想的证明不在此固定流程内，11/12 零区域的文稿还经过了人工编辑以保证可读性。

这段话是整份仓库的"免责声明"也是"使用说明"：它是模型产出物的精选集，不是实验室论文汇编。因此 README 直白承认"部分未形式化的结果可能存在瑕疵，我们会尽快修复"，并提到正在探索社区托管这些材料的可能性。

CONTENTS.md：9142 行的手稿地图

CONTENTS.md 是核心导航工具。每个结果家族以**NNN. 标题**开头，紧跟一句话结论，其下挂载组成该家族的各篇手稿及其摘要。家族的定义值得注意：README 明确说明一个 family 可能包含主结果、伴生论证、推论或替代证明——这意味着同一编号下常常不止一篇论文。例如 003（准黎曼假设）一族就包含 7/8 零区域主证明、11/12 替代证明、Landau–Siegel 零点统一排除三篇手稿。

被媒体广泛报道的"722 篇"，恰好等于当前目录 719 篇加上 history.md 记录的 10 月 7 日撤回的 3 篇（Weil classes 相关签名错误引发的连锁撤回）——数字完全对得上，也说明版本管理是这套仓库的硬设计：README 承诺"已发布版本保持可访问，修订以新版本记录"。

lean/：3619 个形式化文件与 416 个 Comparator 挑战

lean/是整个仓库最有工程价值的部分，Apache 2.0 许可，结构如下：

• lean/OAI.lean：914 行 import 汇总文件，是形式化库的"总开关"；
• lean/OAI/：3619 个.lean源文件，按学科分四层——Algebra（2081 个）、AlgebraicGeometry（975 个）、Analysis（518 个）、AlgebraicTopology（45 个），再按结果家族细分子目录（如lean/OAI/Algebra/OddKaplansky/单家族就拆出上百个文件）；
• lean/ComparatorChallenges/：416 对.json+.lean文件，构成"挑战—解法"验证体系（详见下文）。

README 给出关键量化指标：顶层结果的形式化比例约 42%（300/719），且仍在持续补充。

如何筛出名题级手稿

719 篇不可能逐篇读。按照"结果影响力 × 验证状态 × 可复现性"三个维度，可以从 CONTENTS.md 中筛出真正的名题级条目。下面这张表是按此逻辑挑出的第一批必读清单（Lean 列标注了该家族在 CONTENTS.md 中是否挂载形式化文档标记）：

三条筛选线索

线索一：标题即信号。CONTENTS.md 中conjecture、conjectures、resolves、disproves是最高频的显著性标记。媒体的头条几乎都集中在"解决型"条目（准黎曼、Hodge、Falconer、UGC），但研究价值上"反例型"条目同样重磅：196、197 推翻了 Kaplansky 猜想，199 给出 Auslander–Reiten 猜想的反例族，198 推翻有限性维数有限性。反例通常意味着某个长期假设的结构判断错误，是后续理论的锚点。

线索二：看依赖关系，不看单篇。CONTENTS.md 大量使用"Together with result NNN"、"A companion gives"句式。例如 032（Hodge 猜想）与 001（Milne 有理猜想）互相成就：合起来意味着每个特殊化 Hodge 类在所有素到 p 与晶体实现中同时由单个有理代数闭链表示。002（BSD）与 006（Goldfeld 猜想）合并后，对所有 ℚ 上椭圆曲线的二次扭给出密度为一的完整 BSD。名题的伴生结果往往比主结果更适合做后续工作。

线索三：用[Lean]标记做第一层过滤。CONTENTS.md 中约 242 个家族带(Lean)标记，是"结果可机器核验"的硬信号。未标注不等于错误（README 明言形式化在持续补入），但标注了的是研究起点最稳的候选。

从手稿到研究选题的转化路径

对研究者而言，这份仓库最大的价值不是"答案"，而是它把验证缺口、依赖网络、撤回记录全部摊开了——这本身就是一座问题矿藏。以下是四条可执行的转化路径。

路径一：把未形式化结果形式化

README 明确"约 42% 顶层结果已形式化"，意味着近六成结果等待 Lean 形式化——而 Comparator 挑战机制已经把这项工作变成了可验收的工程任务。

以准黎曼假设为例，lean/ComparatorChallenges/QuasiRiemannHypothesis.lean定义了待证目标：

import Mathlib namespace OAI theorem riemannZeta_ne_zero_of_seven_eighths_lt_re {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by sorry end OAI

对应的 QuasiRiemannHypothesis.json 指明解法模块与允许的公理：

{ "challenge_module": "ComparatorChallenges.QuasiRiemannHypothesis", "solution_module": "OAI.NumberTheory.DirichletL.Nonvanishing", "theorem_names": [ "OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re" ], "permitted_axioms": [ "propext", "Quot.sound", "Classical.choice" ], "enable_nanoda": false }

验证命令只有三条（见 lean/ComparatorChallenges/README.md）：

lake update lake exe cache get lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

机制要点：挑战文件把定理名、解法模块、允许公理固定下来——permitted_axioms只放propext、Quot.sound、Classical.choice三个无伤大雅的公理，意味着解法不得依赖任何额外假设。此外还有 5 个"支持性结果"挑战（如CharacterVarietiesAllSeamsSupport、SurfaceConeCandidateSupport），验证的是主定理所需支撑命题而非主定理本身——这是比"主定理形式化"更细颗粒度的可参与空间。

路径二：从"主定理"走向"反例工程"

反例类结果的 Lean 化是最有教学价值的深水区。看 lean/OAI/Algebra/GroupRing/Basic.lean 中零因子反例的完整命题形态：

def MainTheorem : Prop := ∃ (G : Type) (inst : Group G), letI : Group G := inst Group.IsFinitelyPresented G ∧ TorsionFree G ∧ HasFiniteTwoDimensionalClassifyingSpace G ∧ ∃ α β : MonoidAlgebra (ZMod 2) G, α ≠ 0 ∧ β ≠ 0 ∧ α * β = 0

这串定义把 196 的结论压缩成四件事：有限表现、无挠、存在有限二维 CW K(G,1)、以及 𝔽₂[G] 中一对非零零因子。其中HasFiniteTwoDimensionalClassifyingSpace的定义（连通有限 Hausdorff 二维 CW 复形、万有覆盖、基本群同构）本身就是一个完整的拓扑学小课。而 Main.lean 给出了构造性证明的骨架：

theorem main : MainTheorem := by obtain ⟨rep,r,x,y,hr,hL,hd,ha,hx,hy,hz⟩ := SampleGraph.exists_nonzero_factors exact ⟨ConcreteGroup.G rep r, inferInstance, inferInstance, ...⟩

有意思的是证明结构：它把问题归约到一个**采样图（SampleGraph）**的显式数据上，再逐层装配出具体的群。同家族的lean/OAI/Algebra/OddKaplansky/（对应 197）更夸张，拆出了上百个文件，从GreedyColumns、WreathRepresentation到Fourier、SectorGluing，活脱脱是一套"反例构造方法论"。想研究 AI 生成的证明长什么样、如何把组合构造翻译成可验证代码，这里是第一手标本。

路径三：以"撤回与修复"为教材做审稿式研究

history.md 记录了一次教科书级的撤回案例：在 "Algebraicity of Weil classes on split abelian eightfolds" 中发现符号错误，导致一个稳定化-迹消去论证失效，并连锁拖垮了两篇依赖论文——三篇一并撤回，且撤回论文的 README 会说明缺口并链接存档版本。同日还修复了 14 篇（跨界面证明、Kähler MMP、锥等式等），新增 6 项形式化，将形式化比例从之前推进到 300/719。

这条记录的价值在于：它是"AI 数学如何被纠错"的稀有公开数据。对任何想进入这个领域的人，逐个对照"撤回原因 → 缺口位置 → 依赖传播"就是最真实的审稿训练。也可以从"找下一个符号错误"切入——README 自己承认未形式化结果可能有瑕疵，对错误敏感的读者，这份 58% 未形式化的手稿池就是一片尚未开垦的核查矿。

路径四：把"结果清单"转成"问题清单"

最后，也是最容易被忽略的一点：这个仓库的真正用法，是把它当作问题库的索引而非答案库。每篇手稿的摘要里藏着大量"新的 open problem"——Nagata 猜想的严格非齐次形式（039）、Seshadri 常数的正特征版本、Talagrand 期望阈值与图分解（175）、第二 Kahn–Kalai 猜想（176）、cycle–clique Ramsey 精确值（189）、Brennan 猜想的积分均值谱（072）……这些结果在推进某个猜想的同时，几乎都留下了下一层问题：更强的界、更弱的假设、更干净的证明、更多维数的推广。

配合 CONTENTS.md 的检索技巧（grep -n 'conjecture' CONTENTS.md找猜想、grep -n 'counterexample' CONTENTS.md找反例、grep -n 'Lean' CONTENTS.md找已形式化条目），你能在两小时内产出一份个性化的"待办研究清单"——这比任何论文速读都高效。

结语：先把地图画对，再谈吃法

722 篇（现 719 篇）手稿不是一个需要"读完"的东西，而是一套需要"用好"的系统：CONTENTS.md 是目录，preprints/是正文，lean/OAI/是机器可读的证据链，lean/ComparatorChallenges/是验证入口，history.md是纠错日志。42% 的形式化比例、416 个 Comparator 挑战、5 个支持性挑战、以及仍在持续补充的形式化承诺，共同构成了一个罕见的开放式研究场：别人已经证明了定理，但把证明"讲清楚"、"修正确"、"推广开"的活儿，还远远没有做完。对研究者来说，这份仓库最好的吃法不是仰视它，而是走进它的缺口里。

【免费下载链接】math项目地址: https://gitcode.com/gh_mirrors/math58/math