10 月 6 日白天先是传闻：有人说 OpenAI 要放大约 400 份 AI 写的数学证明，不走论文，直接上 GitHub。晚上，传闻变成了一个仓库。

下面是那一天，按世界时（UTC）排：

这篇文章读的是仓库本身。我读了能当文本读的部分：说明、目录、概览、Lean 的清单、两份挑战声明，还有一份推理摘要的源码。没有编译 Lean，也没有读那 722 份 PDF。所以哪一条是真的，我没法说，今天也没人能说。能说的是：它给了什么，没给什么，该怎么读。

先放一张背景。三个月里，OpenAI 放出的东西一次比一次多：

9 月 21 日那次，只有一个数字，没有清单。15 天后，清单到了。

按 README 的说法，这是开发模型时评测的一部分：原有的数学评测饱和了，评测就扩到了开放问题上。模型被问了约 4000 个题，每个结果平均用掉相当于约三小时 ChatGPT Pro 思考的算力，再按重要程度筛成现在这份清单。绝大多数结果走同一套流程，用的是一个没发布的内部模型。README 点了名的例外有两个：黎曼 ζ 函数的零点自由区域，以及 CM 阿贝尔簇上的 Hodge 猜想。另外，Re s > 11/12 那份零点区域的文字，经人编辑过，让它好读些。

“结果族”是把相关论文归在一起：一个主结果，配上辅助论证、推论或另一种证明。722 篇分在 372 族里，205 族只有一篇，最大的一族有 14 篇。Lean 目录登记的作者只有 OpenAI，提交记录的作者栏是 Anonymous。

再说两个小细节。目录编号排到 377，只有 372 条：045、061、070、123、163 这五个号空着，README 没有解释。每份手稿的目录名里带着日期，最早 9 月 10 日，最晚 10 月 6 日；能读出日期的 720 篇里，有 563 篇落在 9 月 23 日到 27 日这五天。那更像是整理定稿的日子，不是产出的速度，仓库没有说。

清单里有大量听过名字的问题。下面挑 14 条，照着它的摘要转述，不加评价。它们的状态都一样：OpenAI 称已证明，没有同行评审。卡片右上角带青色圆点的，有 Lean 说明页。

没有圆点的五条是：BSD、Hodge、ℚ 上的希尔伯特第十问题、L = RL = BPL、整数乘法。两个千禧年难题的相关结果，BSD 的低余秩情形和 Hodge 的 CM 情形，都在这一组里。

反例也不少。标题里写 counterexample 的有 44 条，写 conjecture 的有 130 条。比如 Borsuk 猜想在 9 维不成立，Hadwiger 猜想也有反例。

Navier-Stokes 也在里面，但不是 9 月 8 日那件事。376 号构造了带光滑外力的黏性流：给一台图灵机，编译出一个外力，让某个粒子到达固定区域，当且仅当这台机器停机。也就是说，这类流能做通用计算。

722 篇论文，谁来验？仓库给的办法是 Lean。有 Lean 的结果，你不用去读那份证明，只要读一份很短的“挑战声明”，再让一个叫 Comparator 的工具去核对。按它的说明，核对通过就保证三件事：证明里的定理和挑战文件陈述的是同一个命题，只用了允许的公理，并且被 Lean 内核接受。前提是 Mathlib 和内核本身可信。

下面是拟黎曼假设那一份。整个文件 9 行，声明本身 2 行：

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

"permitted_axioms": [
  "propext", "Quot.sound", "Classical.choice"
]

翻成人话：只要复数 s 的实部大于 7/8，黎曼 ζ 函数在 s 处就不为零。要人核对的只有三处：ζ 用的是不是 Mathlib 里那个 riemannZeta，不等号的方向和严格性对不对，允许的公理是不是只有 propext、Quot.sound、Classical.choice 这三条。读完这几行，你就知道 Lean 如果通过，到底证明了什么。

如果这两行成立，意味着什么？先说什么是拟黎曼假设。黎曼假设说，ζ 的所有非平凡零点实部都是 1/2。拟黎曼假设弱得多：只要有一个固定的 θ < 1，让 Re s > θ 的区域里没有零点。OpenAI 称 θ = 7/8 可以，而且对所有 Dirichlet L 函数一致成立。

弱，不等于小。零点区域和素数定理的误差项，是一件事的两面：

对照一下现状。此前无条件的最好结果，是 Vinogradov 和 Korobov 在 1958 年前后给出的零点区域，它贴着 Re s = 1，随高度变窄；对应的素数定理误差，是 x 乘上一个 exp(−c(log x)^3/5) 量级的缩小因子（忽略 loglog 因子）。7/8 如果成立，误差就变成 x 的 7/8 次方量级。这个问题此前一直没有人证出来，OpenAI 的概览把它写成“解决了拟黎曼假设”。

声明只有两行，证明在哪里？在仓库的 Lean 库里。lean/OAI 目录下有 121,734 个 .lean 文件，约 1.57 GB 源码；要人去读的挑战声明有 405 个文件，约 4.4 MB。把两者画成面积：

机器去查左边那个大方块，人去读右边那个小红点。形式（form）可以大到没人读得完，功能（function）所依赖的那一小块，仍然得有人去读。

这批 Lean 是怎么来的？lean/formalization.yaml 里有三行自述：范围是 Partial progress，自动化方式是 agent，审核状态是 unchecked。大意是：主要由智能体做，还没有审。把三层验证各自缺什么，列成一张表：

挑战声明不总是这么短。对数 Brunn-Minkowski 那份，全文 41 行：先要定义六样东西，欧氏空间、凸体、原点对称、支撑函数、Wulff 形体、对数组合，占 12 行；然后才是一个 5 行的定理。每个定义都可能藏着一处写偏的地方，读的人得先把它们读完。

仓库还附了 10 份推理摘要。我读了其中一份，关于稀释自旋玻璃（diluted spin glass）的 Mézard-Parisi 公式。开头是提示词节选，大意是：即使题目标着“开放”，意图也是让你解决它；可以给完整严格的证明，也可以给严格的反驳；不鼓励暴力枚举和计算机辅助。后面是三段按阶段写的推理，夹着模型的原话，其中一句是：

读起来像一个人在草稿纸上自言自语。摘要的最后一句只是说，最终回答“声称”下界与插值上界相符。真假，还是要人去判。

前面说，235 个结果族有 Lean 页，占 63%。按学科拆开，差别很大：

数理逻辑 6 个全有，泛函分析 11 个里有 10 个，组合 37 个里有 33 个。代数几何 36 个里只有 7 个，拓扑 18 个里只有 3 个。我的猜测是，这和 Mathlib 里各个领域现成的基础有关：组合和逻辑家底厚，概形、同伦论这类要从头搭很多地基的领域家底薄。这是猜测，仓库没写。

它有一个后果。Hodge 所在的代数几何，覆盖率倒数第二，36 个里有 7 个；BSD 所在的数论，约一半，31 个里有 16 个。这两条自己都没有 Lean 页，只能靠人读。

9 月 29 日，设在普林斯顿高等研究院的“数学与人工智能咨询组”（AGMAI）发了一份《负责任地发布 AI 生成的数学》。成员九位，包括 Gowers、Hairer、Vakil、Witten。他们向数学界征求意见，收到 600 多份回复，给实验室列了一套做法。OpenAI 这次的帖子说，放出这批结果时参考了他们的建议。逐条对照一遍：

形式上的东西，OpenAI 做得相当到位：挑战声明、formalization.yaml、状态说明，都是咨询组点名要的社区标准。没做的在另一头：失败的尝试，选题的办法，每个结果的提示词、用时和成本，一个不归实验室管的存放处。

咨询组在建议的开头就写明：不赞成实验室在外人用不了的模型上测试高难度数学题，并要求他们停止。这批结果，恰恰来自一个没发布的内部模型。OpenAI 的发言人对《科学美国人》说，团队认真对待这些建议，尽量遵守，但不受其约束。他还说，放出的结果里有很多，连他们自己的数学家也还没读懂。

前面有个先例。8 月 1 日那批十个问题，有两位作者做过一次人工核查（arXiv:2608.14673）：没发现主结果里确认的实质错误，但承认审读深度不一，有些依赖只查了一部分。这是对十个问题的核查，不是对 372 个。

先看 Tao。他在仓库出现前近四个小时发了四条帖。他说，传统数学（Math 1.0）里，一个大猜想的证明会引出一连串后续：报告，工作坊，新合作，新人入行，证明在这个过程里被消化、简化，最后写进教材。现在的情形是，问题被 AI 批量解掉，提示它的人对这个领域没有兴趣，也答不出关于结果的问题。被解掉的问题不能变回没解的，连“有解”这个消息本身，也会污染后来人去找别的路、看到更多东西的努力。他的结论是，Math 2.0 要把重心从单纯解题挪开：多看讲解，多看社群，多开新方向。

OpenAI 的发言人对《科学美国人》说，这批结果几乎都是一个智能体、一次提示的产物（有些可能试了不止一次）。MIT 的 Andrew Sutherland 的回应是：在模型发布、别人能复现之前，凡是“单个智能体一次提示就解出”的说法，都该当作没验证过，要向 OpenAI 要凭据。多伦多的 Daniel Litt 说法相反：如果大家想知道这些问题的答案，就没有理由让公司替我们保密，他认为这对数学是好事。

Hacker News 上，我读了前三十条一级评论。有人说这是进步，没有闹剧；有人说实验室是被公开点名才肯来和数学界打交道的；有人说 Lean 只证明你写下的命题，命题写对没有，得有人看；有人问，博士读到一半，手上的课题被写进了清单怎么办；也有人批评 AGMAI 的“停止测试”，说这像是为了让数学家保住饭碗。

以上都是别人的反应。我自己的看法，落在怎么读上。读之前，先问三件事。

1976 年，IBM 的计算机跑了上千个小时，才证明了四色定理，系里的邮戳改成了“四色足矣”。这次，OpenAI 说平均每个结果三小时。两个数字没法比：一个是检查用的机器时间，一个是折算出来的思考算力。有一样东西没变：读懂它们要花的，还是人的时间。

“清单可以一夜写完，
读懂得一条一条来。

During the day on October 6 there were only rumors: OpenAI, people said, was about to release some 400 AI-written math proofs, not as papers but straight onto GitHub. By evening the rumor had become a repository.

Here is how the day went, in Coordinated Universal Time (UTC):

This article reads the repository itself. I read the parts that can be read as text: the README, the contents, the overview, the Lean manifest, two challenge statements, and the source of one reasoning summary. I did not compile the Lean, and I did not read the 722 PDFs. So I cannot tell you which results are true, and as of today nobody can. What I can tell you is what it provides, what it does not, and how to read it.

First, some background. Over three months, each of OpenAI's releases was bigger than the last:

On September 21 there was only a number, no list. Fifteen days later, the list arrived.

According to the README, this was part of the evaluation done while developing the model: the existing math benchmarks had saturated, so the evaluation was extended to open problems. The model was given about 4,000 problems; each result used, on average, the equivalent of about three hours of ChatGPT Pro thinking compute; and the results were then filtered by importance down to the present list. The vast majority went through the same pipeline, using an unreleased internal model. The README names two exceptions: a zero-free region for the Riemann zeta function, and the Hodge conjecture for CM abelian varieties. Separately, the text of the Re s > 11/12 zero-free region paper was edited by hand to make it easier to read.

A “result family” groups related papers together: one main result, along with supporting arguments, corollaries or alternative proofs. The 722 papers fall into 372 families; 205 families contain a single paper, and the largest contains 14. The only author listed in the Lean directory is OpenAI, and the author field of the commit says Anonymous.

Two more small details. The entries in the contents are numbered up to 377, but there are only 372 of them: 045, 061, 070, 123 and 163 are missing, and the README does not say why. Each manuscript's directory name carries a date, the earliest September 10 and the latest October 6. Of the 720 whose dates can be read, 563 fall in the five days from September 23 to 27. Those look more like the days the papers were tidied up and finalized than a measure of how fast they were produced, but the repository does not say.

The list is full of problems you may have heard of. Here are 14, paraphrased from its own abstracts, without comment. They all have the same status: OpenAI says they are proved, and none has been peer-reviewed. Cards with a teal dot in the top right corner have a Lean page.

The five without a dot are BSD, Hodge, Hilbert's tenth problem over ℚ, L = RL = BPL, and integer multiplication. Both results tied to Millennium Prize Problems, the low-corank case of BSD and the CM case of Hodge, are in this group.

There are plenty of counterexamples, too. The word counterexample appears in 44 titles, and conjecture in 130. For instance, the Borsuk conjecture fails in dimension 9, and the Hadwiger conjecture gets a counterexample as well.

Navier-Stokes is in there too, but not the September 8 result. Entry 376 constructs viscous flows with smooth forcing: given a Turing machine, it compiles a forcing term such that a certain particle reaches a fixed region if and only if the machine halts. In other words, flows of this kind can carry out universal computation.

Who is going to check 722 papers? The repository's answer is Lean. For a result that has Lean, you don't need to read the proof. You read only a very short “challenge statement” and let a tool called Comparator do the checking. According to its documentation, passing the check guarantees three things: the theorem in the proof states the same proposition as the challenge file, it uses only the permitted axioms, and the Lean kernel accepts it. All of this assumes that Mathlib and the kernel themselves can be trusted.

Here is the one for the quasi-Riemann hypothesis. The whole file is 9 lines, and the statement itself is 2:

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

"permitted_axioms": [
  "propext", "Quot.sound", "Classical.choice"
]

In plain words: whenever the real part of a complex number s is greater than 7/8, the Riemann zeta function is not zero at s. A person needs to check only three things: whether ζ is Mathlib's riemannZeta, whether the inequality points the right way and is strict where it should be, and whether the only permitted axioms are propext, Quot.sound and Classical.choice. Once you have read these few lines, you know exactly what has been proved if Lean accepts the proof.

If these two lines hold, what follows? First, what is the quasi-Riemann hypothesis? The Riemann hypothesis says that all nontrivial zeros of ζ have real part 1/2. The quasi-Riemann hypothesis is much weaker: it asks only for some fixed θ < 1 such that the region Re s > θ contains no zeros. OpenAI says that θ = 7/8 works, and works uniformly for all Dirichlet L-functions.

Weak is not the same as small. Zero-free regions and the error term in the prime number theorem are two sides of the same coin:

Compare this with where things stood. The best unconditional result until now is the zero-free region that Vinogradov and Korobov obtained around 1958. It hugs the line Re s = 1 and gets narrower with height, and the corresponding error term in the prime number theorem is x times a shrinking factor of order exp(−c(log x)^3/5) (ignoring loglog factors). If 7/8 holds, the error drops to the order of x to the power 7/8. Nobody had proved this before, and OpenAI's overview presents it as having solved the quasi-Riemann hypothesis.

The statement is two lines long. So where is the proof? In the repository's Lean library. The lean/OAI directory holds 121,734 .lean files, about 1.57 GB of source; the challenge statements that people have to read come to 405 files, about 4.4 MB. Drawn as areas:

Machines check the big square on the left; people read the small red dot on the right. The form can grow too large for anyone to read through, but the small piece that the function depends on still has to be read by someone.

Where did all this Lean come from? The file lean/formalization.yaml describes it in three lines: the scope is Partial progress, the automation is agent, and the review status is unchecked. In other words, it was done mainly by agents and has not yet been reviewed. Here is what each of the three layers of verification still lacks:

Challenge statements are not always this short. The one for log-Brunn-Minkowski runs to 41 lines. It first has to define six things, Euclidean space, convex body, origin symmetry, support function, Wulff shape and logarithmic combination, which take 12 lines; only then comes a 5-line theorem. Any one of those definitions could hide a subtle misstatement, and the reader has to work through all of them first.

The repository also includes 10 reasoning summaries. I read one of them, on the Mézard-Parisi formula for diluted spin glasses. It opens with an excerpt from the prompt, which says, roughly: even if a problem is labeled “open,” the intent is for you to solve it; you may give either a complete rigorous proof or a rigorous disproof; brute-force enumeration and computer assistance are discouraged. Then come three stages of reasoning, interspersed with the model's own words. One line reads:

It reads like someone muttering to themselves over scratch paper. The last sentence of the summary says only that the final answer “claims” the lower bound matches the interpolation upper bound. Whether that is true is still for people to judge.

As noted above, 235 result families have a Lean page, 63% of the total. Broken down by field, the differences are large:

In mathematical logic all 6 have one, in functional analysis 10 of 11, and in combinatorics 33 of 37. Algebraic geometry has only 7 of 36, and topology only 3 of 18. My guess is that this tracks how much ready-made foundation each field already has in Mathlib: combinatorics and logic are well stocked, while areas like schemes and homotopy theory, which need a lot of groundwork laid from scratch, are thin. That is a guess; the repository does not say.

This has a consequence. Algebraic geometry, home of Hodge, has the second-lowest coverage, 7 of 36; number theory, home of BSD, has about half, 16 of 31. Neither of those two results has a Lean page of its own. They can only be checked by people reading them.

On September 29, an advisory group on mathematics and AI (AGMAI), based at the Institute for Advanced Study in Princeton, published “Responsible Release of AI-Generated Mathematics.” It has nine members, including Gowers, Hairer, Vakil and Witten. They asked the mathematical community for input, received more than 600 responses, and set out a list of practices for the labs. OpenAI's post this time says it drew on their recommendations in releasing these results. Here they are, item by item:

When it comes to the formal pieces, OpenAI has done a thorough job: the challenge statements, formalization.yaml and the status notes are all community standards the group asked for by name. What is missing lies at the other end: the failed attempts, how the problems were chosen, the prompt, time and cost for each result, and a home the lab does not control.

At the very start of its recommendations, the group says plainly that it does not approve of labs testing hard mathematical problems on models outsiders cannot use, and asks them to stop. These results come from exactly that: an unreleased internal model. An OpenAI spokesperson told Scientific American that the team takes the recommendations seriously and tries to follow them as far as it can, but is not bound by them. He also said that many of the released results have not yet been understood even by the company's own mathematicians.

There is a precedent. For the ten problems released on August 1, two authors carried out a human audit (arXiv:2608.14673). They found no confirmed substantive errors in the main results, but acknowledged that their reading varied in depth and that some dependencies were only partly checked. That was an audit of ten problems, not of 372.

Start with Tao. Nearly four hours before the repository appeared, he posted four times. In traditional mathematics (Math 1.0), he said, the proof of a major conjecture sets off a chain of follow-ups: talks, workshops, new collaborations, new people coming into the field. Along the way the proof is digested and simplified, and eventually it makes its way into textbooks. What is happening now is that problems are being solved by AI in bulk, prompted by people who have no interest in the field and cannot answer questions about the results. A solved problem cannot be made unsolved again, and even the bare news that a solution exists contaminates the efforts of those who come later to find other routes and see more. His conclusion is that Math 2.0 has to shift its weight away from just solving problems: more exposition, more community, more new directions.

An OpenAI spokesperson told Scientific American that almost all of these results came from a single agent working from a single prompt (some may have taken more than one attempt). Andrew Sutherland of MIT responded that until the model is released and others can reproduce the work, any claim that a problem was solved by a single agent from a single prompt should be treated as unverified, and OpenAI should be asked to back it up. Daniel Litt in Toronto took the opposite view: if people want to know the answers to these problems, there is no reason to have a company keep them secret on our behalf, and he thinks this is good for mathematics.

On Hacker News, I read the first thirty top-level comments. Some called it progress, not a circus. Some said the labs only came to deal with mathematicians after being called out in public. Some pointed out that Lean proves only the proposition you write down, and someone still has to look at whether you wrote it down correctly. One person asked what a PhD student should do if the problem they are halfway through ends up on the list. And some criticized AGMAI's call to stop testing, saying it looked like a way for mathematicians to protect their jobs.

Those are other people's reactions. My own view comes down to how to read the list. Before you read, ask three things.

In 1976, IBM computers ran for more than a thousand hours to prove the four color theorem, and the department's postmark was changed to “Four Colors Suffice”. This time, OpenAI says three hours per result on average. The two numbers can't be compared: one is machine time spent checking, the other is thinking compute converted into hours. One thing hasn't changed: understanding the results still costs human time.

“A list can be written overnight;
understanding it goes one item at a time.