上学的时候你大概也经历过：一道证明题，答案看懂了，自己写就漏洞百出。数学证明这种东西，对就是对、错就是错，糊弄不过去的。现在有一批 AI 写的数学证明，正在接受同样的检验——而且检验结果公开可查。
这个仓库是 OpenAI 十天前（2026 年 10 月 6 日）建的，名字就叫 openai/math。建仓才 10 天，截至榜单抓取那天已经攒了 1.5 万颗星，排 GitHub 近 30 天新建仓库总星榜第 5 名。它里面装的是什么？据项目 GitHub 页介绍：OpenAI 内部模型在开放数学研究问题上产出的手稿合集——719 篇手稿，归成 372 个族（一族就是一组相关的论文，可能包含一个主要结果、配套论证和不同证法），按数学学科分类。
它跟网上那些"AI 生成的文章"有本质区别：这个仓库里约 42% 的顶层结果已经完成了 Lean 形式化。Lean 是一种数学证明语言，用人话说，就是把证明写成计算机能逐行校验的代码——计算机验过的证明，不存在"看起来对"这种事，对了就是对了。官方还同时公开了部分结果的推理摘要，你能看到模型是怎么一步步想的。
它解决的是个老争论："AI 到底是真会数学，还是嘴上功夫。"以前的答案是看刷题分数——官方自己在 README 里说，既有数学评测上的表现已经饱和（就是题目都考不出差距了），所以他们换了个方式：拿真正开放的研究问题去考模型。绝大多数结果用同一套流程产出，平均每个结果要烧掉这个内部模型三个小时的算力，一共问了大约 4000 个问题。这套玩法对普通人的意义在于：以后"让 AI 干需要严谨性的活"这件事，多了一个可核验的样本——结果不是 AI 自己说对，是机器验过。
有几句官方自己写的实话要转达：并非所有结果都附有 Lean 形式化，部分未经形式化的结果可能存在问题，官方说会尽快修。仓库体积很大，约 811MB，想下载的话留够硬盘。另外它正在探索把材料转给社区托管，也就是说这个 GitHub 地址以后可能会搬家。
怎么用 AI 读它？它不是一个你要安装的软件，更像一座公开的图书馆。打开仓库里的概览和手稿映射，挑你感兴趣的题目——里面有从 π 的无理性指数到量子磁化这种各种口味的——把对应的页面内容复制给 AI 助手（豆包、Kimi、DeepSeek 都行），让它用人话给你讲解这篇手稿在证明什么、难在哪。官方文档没有提供 AI 集成或安装器，它本来就不是拿来"装"的。
AI 做的数学，敢公开、敢让机器验、错了敢认——这种开放方式比分数榜好看。我先看明白了，你跟上。