722 篇手稿怎么吃OpenAI 数学仓库的 GitHub 食用指南【免费下载链接】math项目地址: https://gitcode.com/gh_mirrors/math58/math2026 年 9 月底到 10 月初数学界被一条消息震动了OpenAI 一次性公开了数百篇由其内部模型产出的数学手稿媒体用数学大爆炸、数学的广岛时刻来形容这场冲击——准黎曼假设被证明、CM 阿贝尔簇上的有理 Hodge 猜想被攻克、Unique Games 猜想告破……更关键的是这些成果不是停留在 PDF 里而是连带一套 Lean 形式化工程一并放进了 GitHub。社区的情绪复杂兴奋于AI 一夜投下 722 篇手稿警惕于其中有多少能被逐行验证。这份仓库README.md就是那 722 篇发布后撤回 3 篇当前目录为 719 篇手稿的完整载体。但 719 篇、372 个结果家族的体量对任何人都是打开即迷路。本文不讨论 AI 数学的哲学争议只做一件事把这份仓库的目录结构拆开给出筛出名题、读懂形式化证据、把手稿转化成研究选题的可执行路径。仓库目录与文件组织速览先建立全局坐标。仓库根目录只有四个入口文件加上一个巨大的lean/目录路径作用README.md仓库总纲结果如何产生、如何导航、验证状态与版本承诺CONTENTS.md手稿地图719 篇手稿、372 个结果家族的一站式索引含摘要与 PDF 链接history.md版本历史撤回、修复、新增形式化的完整记录preprints/每篇手稿的 PDF、源码与 BibTeX 引用由 CONTENTS.md 逐篇链接lean/形式化证据OAI 库 Comparator 挑战集四个入口文件分工极其清晰README 回答这些东西怎么来的CONTENTS 回答里面有什么history 回答哪些不可信或已修订lean 回答哪些能机器验证。结果如何产生一个值得先读的数字段README.md 用一小段话交代了全部生产背景信息密度极高绝大多数结果由同一个未发布的内部 OpenAI 模型产出每项结果平均消耗3 小时 ChatGPT Pro thinking 算力整个评估周期内模型被提出了约4,000 道问题经聚合、分族、显著性筛选后沉淀为当前目录特别声明ζ 函数的零区域、CM 阿贝尔簇 Hodge 猜想的证明不在此固定流程内11/12 零区域的文稿还经过了人工编辑以保证可读性。这段话是整份仓库的免责声明也是使用说明它是模型产出物的精选集不是实验室论文汇编。因此 README 直白承认部分未形式化的结果可能存在瑕疵我们会尽快修复并提到正在探索社区托管这些材料的可能性。CONTENTS.md9142 行的手稿地图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.lean914 行 import 汇总文件是形式化库的总开关lean/OAI/3619 个.lean源文件按学科分四层——Algebra2081 个、AlgebraicGeometry975 个、Analysis518 个、AlgebraicTopology45 个再按结果家族细分子目录如lean/OAI/Algebra/OddKaplansky/单家族就拆出上百个文件lean/ComparatorChallenges/416 对.json.lean文件构成挑战—解法验证体系详见下文。README 给出关键量化指标顶层结果的形式化比例约 42%300/719且仍在持续补充。如何筛出名题级手稿719 篇不可能逐篇读。按照结果影响力 × 验证状态 × 可复现性三个维度可以从 CONTENTS.md 中筛出真正的名题级条目。下面这张表是按此逻辑挑出的第一批必读清单Lean 列标注了该家族在 CONTENTS.md 中是否挂载形式化文档标记编号名题一句话结论Lean 形式化003准黎曼假设所有 Dirichlet L-函数含 ζ(s)在 Re s 7/8 无零点另有 11/12 替代证明与 Landau–Siegel 零点统一排除✓032有理 Hodge 猜想对每个复 CM 阿贝尔簇、任意维数与余维成立并推出 Tate 猜想与 Hodge 标准猜想未标注001Milne 有理猜想好约化阿贝尔簇上 Hodge 类与互补除子乘积配对为有理数与上同调理论无关未标注002完整 BSD 公式低 Selmer corank0 或 1推出完整 Birch–Swinnerton-Dyer 首项公式及 Tate–Shafarevich 有限性未标注004Hilbert 第十问题ℚ不存在算法判定整系数多项式在 ℚ 上有无零点未标注005Catalan 常数G 是无理数✓007ordinary two-point ChowlaLiouville 相关和获得对数幂次节省二元修正 Elliott 猜想成立✓102Unique Games 猜想Khot 的 UGC 成立并给出 Max-Cut 等问题的最优近似阈值NP-困难性✓103去随机化L RL BPL未标注107矩阵乘法复域上 ω ≤ 9/4✓109整数乘法确定性最坏情形 O(n(log n)^{1-κ})κ 2⁻¹⁸²低于 n log n未标注073Falconer 距离猜想所有维数 d ≥ 2 成立✓074Kakeya三维 Kakeya 极大猜想、四维 Hausdorff 维数猜想未标注078Bochner–Riesz三维严格范围解决未标注196反例Kaplansky 零因子猜想构造有限生成无挠群 G其 ₂[G] 有非零零因子Comparator 挑战 ✓197反例Kaplansky 直接有限性特征 2 下无挠群代数非直接有限Comparator 挑战 ✓三条筛选线索线索一标题即信号。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句式。例如 032Hodge 猜想与 001Milne 有理猜想互相成就合起来意味着每个特殊化 Hodge 类在所有素到 p 与晶体实现中同时由单个有理代数闭链表示。002BSD与 006Goldfeld 猜想合并后对所有 ℚ 上椭圆曲线的二次扭给出密度为一的完整 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.mdlake 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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考