中文版

math（GitHub：https://github.com/openai/math ，2026-10-06 创建，今晨抓取时已 17,245★）是 OpenAI 放出的数学手稿合集：一个未发布的内部模型在开放研究问题上的产出，附带证明材料与 Lean 形式化。

按 README 的说法，评估中模型被出了约 4,000 道问题，平均每个结果用了 3 小时 ChatGPT Pro 级别的思考算力；整理后形成 721 篇手稿、归入 373 个家族（一个家族可含主结果、伴随论证、推论或替代证明）。仓库里有 preprints/（PDF 与源码）、lean/（形式化证明库）、reasoning_traces/（推理摘要），顶线结果约 42% 已有形式化；推理摘要覆盖了 π 的无理性指数、对称 Mahler 猜想、Kaplansky 直接有限性猜想等题目。

为什么值得了解

• 这是“AI 能不能做前沿数学研究”最直接的实证材料：不是营销说法，而是 721 篇可下载、可核查的手稿，外加能用 Lean 机器验证的证明
• 对学形式化证明、Lean 的人尤其有用：同一批结果同时给了自然语言手稿和机器证明，可以对照着看“人类写法”与“机器可验证写法”的对应关系
• 但要按 README 的提醒来读：作者明说这些应视为原始研究数据而非打磨好的论文，未形式化的结果可能有问题，署名与优先权以数学界的判断为准

English Version

math (GitHub: https://github.com/openai/math , created 2026-10-06, 17,245 stars at this morning’s fetch) is OpenAI’s collection of mathematical manuscripts: the output of an unreleased internal model on open research problems, with proof artifacts and Lean formalizations.

Per the README, the model was posed roughly 4,000 problems during evaluation, using on average three hours of ChatGPT Pro-level thinking compute per result; the output was organised into 721 manuscripts in 373 families (a family can hold a principal result, companion arguments, consequences or alternative proofs). The repo contains preprints/ (PDFs and sources), lean/ (the formal proof library) and reasoning_traces/ (reasoning summaries), with about 42% of top-line results formalized; the reasoning summaries cover topics such as the irrationality exponent of π, the symmetric Mahler conjectures and Kaplansky’s direct-finiteness conjecture.

Why it’s worth knowing

• This is the most direct evidence available for “can AI do frontier mathematics research”: not marketing, but 721 downloadable, checkable manuscripts plus proofs a machine can verify in Lean
• Especially useful for anyone learning formal proofs or Lean: the same results come with both natural-language manuscripts and machine-checkable proofs, so you can compare the two styles side by side
• Read it with the README’s warning attached: the authors say these should be treated as raw research data, not polished papers — unformalized results may contain issues, and credit and precedence are for the mathematics community to judge