OpenAI 公开一批数学文稿，附带可检查的证明文件 OpenAI published a batch of math papers, with proof files you can check

详细介绍Details

OpenAI 发了一篇《Sharing AI progress in mathematics》，并在 GitHub 仓库 openai/math 放出一批由内部模型写出的数学文稿。仓库说明写，当前目录有 722 篇文稿，分成 372 个结果族。一篇族可以把主结果、伴随论证和另一种证法放在一起。仓库同时放了 Lean 证明。Lean 是一种可以用电脑检查证明对不对的语言。说明写，不是每一篇都有 Lean，没有形式化的结果里可能有问题，他们会尽快改。博文还写，这次附了 10 份推理过程的缩写，以及按 ChatGPT Pro 思考时长估算的计算量：平均每个结果大约相当于 3 小时。模型本身还没有放出。本库没有读这些论文，也没有跑过 Lean。 OpenAI published “Sharing AI progress in mathematics” and put a batch of math papers from an internal model in the GitHub repo openai/math. The repo says the catalogue has 722 manuscripts in 372 families. A family can hold a main result, companion arguments, and another proof. The repo also includes Lean proofs. Lean is a language a computer can use to check whether a proof holds. The readme says not every paper has Lean, that some results without it could have issues, and that they will try to fix those quickly. The post also says this release includes 10 shortened reasoning summaries and a compute estimate in ChatGPT Pro thinking time: about three hours for the average result. The model itself is not released. This library did not read the papers and did not run Lean.

它是什么What it is

这是一次数学结果的公开，不是一个你能在聊天框里调用的新模型。OpenAI 说这些文稿来自他们内部还没发布的模型。公开的位置是 GitHub 仓库 openai/math，许可 Apache-2.0。仓库自己的目录写着 722 篇文稿、372 个结果族。一个族是一组相关论文，可以包括主结果、配套论证或另一种证法。旁边有 Lean 证明，电脑可以检查这些证明是否成立。仓库写得很直：不是每篇都有 Lean，没做形式化的结果里可能有错，发现了会改。博文另外说，这次放了 10 份推理过程的缩写，并说平均每个结果用掉的计算量大约等于 ChatGPT Pro 思考 3 小时。这句话是官方的估算，本库没有重算。 This is a release of math results, not a new model you can call from a chat box. OpenAI says the papers come from an internal model that is not released yet. The public place is the GitHub repo openai/math, under Apache-2.0. The repo’s own catalogue says 722 manuscripts and 372 families. A family is a group of related papers: a main result, companion arguments, or another proof. Lean proofs sit beside them. A computer can check whether those proofs hold. The repo is direct: not every paper has Lean, results without that check could be wrong, and they intend to fix problems they find. The post also says this release includes 10 shortened reasoning write-ups, and that the average result used about three hours of ChatGPT Pro thinking. That is the vendor’s estimate. This library did not recompute it.

为什么推荐Why we recommend it 可读文本来自 r.jina.ai 对同一 URL 的抓取，标题 Sharing AI progress in mathematics。博文写：结果来自一个内部前沿模型；与普林斯顿高等研究院的数学与人工智能顾问组商量过发布方式；材料放在 GitHub，含修订和引用约定；许多证明有 Lean 形式化，以后继续补；另有 10 份推理摘要、按 ChatGPT Pro 用量估算的计算量，以及尝试过多少问题的统计。博文给出的计算量原句是 The average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking。博文说会资助研讨会，细节以后再说；模型还在准备负责任地发布，本条不把它写成已上线的模型。README 与 CONTENTS.md 都写 722 manuscripts、372 families。README 写并非都有 Lean，未形式化的结果可能有问题。本库没有逐篇打开 PDF，没有运行 Lean，没有核对“大约三小时”的换算，也没有打开博文里指向的 Navier-Stokes 模型页。 The readable text is a fetch of that same URL through r.jina.ai, title Sharing AI progress in mathematics. The post says the results come from an internal frontier model, that release practice was discussed with the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, that the materials are on GitHub with revision and citation protocols, that many proofs have Lean formalizations and more will be added, and that the release includes 10 reasoning summaries, a compute estimate in ChatGPT Pro usage, and statistics on how many problems were attempted. The compute sentence is: The average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking. The post says workshops will be funded later, without details. It says the model is still being prepared for a responsible release, so this note does not treat it as a model you can call. Both the README and CONTENTS.md say 722 manuscripts and 372 families. The README says not every paper has Lean and that some unformalized results could have issues. This library did not open the PDFs one by one, did not run Lean, did not check the “about three hours” conversion, and did not open the Navier-Stokes model page linked from the post.

对照Contrast

左列是公告和仓库写明的事实。右列是本站口径：为什么放在 Cases 的资讯里，而不是模型板。 Left: what the post and the repo state. Right: why this sits in Cases as news, not on the model board.

怎么试Try it

1. 先看公告在承诺什么 Read what the announcement commits to

   公告页在有些网络环境下会先出浏览器校验。打得开的话，看它怎么讲内部模型、Lean，以及大约 3 小时 Pro 思考这个估算。HN 讨论在 item 49984923。 The announcement URL shows a browser check on some networks. If it opens, read how it describes the internal model, Lean, and the estimate of about three hours of Pro thinking. The HN thread is item 49984923.

   OpenAI 公告 OpenAI announcement HN 讨论 HN thread

2. 用仓库核对数量和许可 Check the count and the license in the repo

   README 和 CONTENTS.md 都写 722 篇、372 个族。许可是 Apache-2.0。先看总览 PDF 和目录，再决定要不要读某一族。 The README and CONTENTS.md both say 722 manuscripts and 372 families. The license is Apache-2.0. Start with the overview PDF and the catalogue, then decide whether to read one family.

   GitHub 仓库 GitHub repo 文稿目录 Manuscript map

3. 把 Lean 当成检查工具，而不是已经全部通过 Treat Lean as the checker, not as a stamp on every paper

   仓库的 lean 目录说明哪些证明可以让电脑检查。没有 Lean 的那部分，仓库自己说可能有问题。本库没有在本地跑过检查。 The lean directory says which proofs a computer can check. For the papers without Lean, the repo itself says there could be issues. This library did not run the check locally.

   仓库里的 Lean 说明 Lean notes in the repo

边界Boundaries

• 本库没有读完论文，没有运行 Lean，没有重算“大约 3 小时 ChatGPT Pro”这个官方估算。 This library did not finish the papers, did not run Lean, and did not recompute the vendor estimate of about three hours of ChatGPT Pro thinking.
• 722 与 372 来自仓库 README 和 CONTENTS.md。公告正文的可读副本没有再写这两个数。 722 and 372 come from the repo README and CONTENTS.md. The readable copy of the announcement did not restate those two numbers.
• 做出这些结果的模型还没有发布。这条不是模型卡，也不能当成你已经可以调用的接口。 The model that produced the results is not released. This is not a model card, and it is not an API you can call.
• 公告页在本环境直接请求返回 403。正文通过阅读代理核对，HN 外链指向同一 URL。 A direct request to the announcement returned 403 in this environment. The body was checked through a reader proxy, and the HN link points at the same URL.