Leo's log

数学

比蒙之跃

Beamon's Leap

一九六八年十月,墨西哥城奥运会,跳远决赛。鲍勃·比蒙第一跳落地,电子测距仪的光学导轨滑到尽头,够不着他的落点。裁判只好去找一把卷尺。

量出来是 8.90 米。此前的世界纪录是 8.35 米。跳远的纪录,过去三十多年是一厘米一厘米往前挪的:欧文斯一九三五年的 8.13 米,二十五年后才被改写。比蒙一跳,多出去五十五厘米。

他听不懂米制。有人替他换算成英尺,二十九英尺二点五英寸。他明白过来,双膝跪倒在跑道边上。


二〇二六年十月六日,OpenAI 在 GitHub 上开了一个仓库,叫 openai/math。[1]

README 很短。里面说,他们一直用开放的研究问题评估自己的模型,现有的数学评测已经饱和,所以扩大了评测。这个仓库收的,是一个未发布的内部模型交出来的东西:七百一十九篇论文,归成三百七十二个“结果族”,按学科分类。

做法也写在里面。模型一共被问了大约四千道题,绝大多数结果走的是同一套固定流程,每个结果平均用掉约三小时 ChatGPT Pro 级别的思考算力。产出按族归并,再按“足够重要”筛了一遍,剩下的就是这份目录。约 42% 的主结果附有 Lean 形式化证明,其余没有。README 自己写着:没有形式化的结果里,有些可能有问题。[1]

我把三百七十二个族的标题从头到尾读了一遍。[2]读到一半,就不太能继续把它们当成一份清单了。

Khot 的唯一博弈猜想,证明了。L = RL = BPL,对数空间的随机化可以完全去掉。哈德维格猜想,给出了反例。卡普兰斯基的零因子猜想,反例。汤普森群 F 不顺从。自由群因子 L(F2)L(\mathbb F_2) 与 L(F3)L(\mathbb F_3) 同构。有理数上的希尔伯特第十问题,答案是否定的。平面不能用五种颜色染色,色数只剩六或七两种可能。博苏克猜想在九维就不成立。CM 阿贝尔簇的有理霍奇猜想。整数乘法跑进了 nlog⁡nn\log n 以内。

论文的落款日期,从九月二十三日排到十月七日。

这里面任何一条单拎出来,放在往年,都够一个领域热闹一整年。Scott Aaronson 当天的博文标题叫《The Mathocalypse》,说这是数学史上最重大的日子之一。[5]


有两个结果,可以画在同一张纸上。

第一个是 π。一个无理数能被分数逼近得多好,用它的无理性指数来量:指数越小,越“难”被逼近。几乎所有实数的指数都是 2,人们相信 π 也是,但证明是另一回事。一九五三年,马勒证明了 π 的指数不超过 42。此后七十年,这个上界被一点一点往下压:20,19.89,8.016,7.606。二〇二〇年,Zeilberger 和 Zudilin 把它压到 7.103。

仓库第 017 号:π 的无理性指数恰好是 2。[2]

顺带解决的,还有那个出了名难缠的 Flint–Hills 级数 ∑1/(n3sin⁡2n)\sum 1/(n^3\sin^2 n)。它收敛。

第二个是矩阵乘法。两个 n×nn\times n 矩阵相乘,最快需要大约 nωn^\omega 次运算,ω 是多少,没人知道,只知道不小于 2。一九六九年施特拉森把它从 3 压到 2.808,震动了整个领域;此后二十年,几代人把它压到 2.376;再往后三十多年、七八篇论文,从 2.376 磨到 2.3713。小数点后第四位上的战争。

仓库第 107 号:ω≤9/4\omega \le 9/4。[2]

π 的无理性指数(上界,对数轴)251020421960198020002020理论下限 = 2Mahler 1953Hata7.103 (2020)2(2026,声称)矩阵乘法指数 ω(上界)2.02.252.52.81198020002020理论下限 = 2Strassen 19692.376 (1990)2.3713 (2024)9/4(2026,声称)
图 · 两条纪录。左:π 的无理性指数上界(对数纵轴),从 Mahler 1953 年的 42 到 Zeilberger–Zudilin 2020 年的 7.103。右:矩阵乘法指数 ω 的上界,从 Strassen 1969 年的 2.808 到 2024 年的 2.3713。墨色阶梯为人类文献中的历次纪录;着色虚线是 openai/math 的声称值(π 为 2,ω 为 9/4),据仓库均附 Lean 形式化,尚未经过同行评审。两边的虚横线都是理论下限 2。

两个月前我写《临界线上的领土》,管黎曼猜想那条路上的进展叫“厘米战争”:三十年,不到一个百分点。那篇文章写的是一次例外。现在回头看,例外在两个月里变成了批发。

而且临界线那边,这次也有消息。第 003 号把它叫作“拟黎曼猜想”:所有狄利克雷 L 函数,包括 ζ 本身,在 Re⁡s>7/8\operatorname{Re}s>7/8 的整片半平面上没有零点。[2]一百多年来,已知的无零点区域都贴着 Re⁡s=1\operatorname{Re}s=1 那条边,越往上越窄,窄到趋于零;从来没有人能划出一条固定的竖线,说线右边一个零点也没有。如果这篇论文成立,零点被关进了 1/8 到 7/8 之间的带子里,Landau–Siegel 零点也一并排除了。离黎曼猜想还差得远,但这是另一种意义上的圈地:上一次是从临界线往外扩,这一次是从外面往里收。


比蒙那一跳,测距仪的导轨不够长。这一次也一样,量它的尺子不够长。

先说量得出来的部分。Lean 形式化过的结果,在“推理有没有错”这件事上,是可以放心的。我在《费马找到了一个真正奇妙的证明》里写过,内核不需要理解数论,只按规则检查;这样的检查可以由任何人重复运行。七百一十九篇里,大约三百篇的主结果走到了这一步。[3]

但那篇文章里也说过另一半:**工具能检查证明,却不能仅凭名字,保证陈述就是读者以为的那个结果。**形式陈述和论文里的那句话是否一致,仍然要人去对。仓库为此单独准备了 Comparator 的检查说明,这是对的。

剩下的四百多篇,是另一回事。

发布第二天,history.md 里出现了第一条更新。一篇关于“分裂阿贝尔八维簇上 Weil 类代数性”的论文里有一个符号错误,一个关键的抵消论证因此失效。另外两篇建立在它之上,一起撤回。三篇都在霍奇猜想那一带,都没有形式化。同一天,十四篇论文被修订,另有十三篇随之更新了引用。[3]

我不觉得这是丑闻。错误被找出来、撤回、留档,旧版本仍然可以查到,这是一套系统在正常工作。可它也提醒了一件事:一个符号错误,带倒了三篇论文,而这三篇在被撤回之前,看上去和其余七百多篇没有任何区别。

还有两处要读仔细。README 说,“拟黎曼猜想”和 CM 霍奇猜想这两项,恰好不在那套固定流程之内;11/12 那篇的成稿还经过人工编辑,以便阅读。[1]最惹眼的两项,是例外。仓库没有说例外在哪里。

Aaronson 在同一篇博文里写,有些结果带着 Lean 证书,但几乎还没有任何一个人真正读懂过这些证明。他的妻子 Dana Moshkovitz 为唯一博弈猜想工作了很多年,她觉得这些论文写得很差,不借助 AI 很难读下去。[5]

数学的同行评审,是按“一年几篇”的速度设计的。审一篇长论文,可能要几个月。现在一个上午到了七百篇。


仓库还放出了十份推理摘要。我读了 π 那一份。[4]

四十二页。是摘要,而且是删节过的。几乎每一页都在失败。

它试了 Padé 逼近,试了 Salikhov 的复端点方法,试了 BBP 公式,试了 Toeplitz 矩阵、模形式、CM 共轭之间的插值,试了 Roth 定理的多变量版本,又拿 Liouville 数去反驳自己。每条路都撞上同一堵墙:解析上省下来的余量,被分母的算术代价吃掉。摘要里夹着几句原话,像实验记录本页边的潦草字迹:

它先拿到的不是 2,是 62/25,也就是 2.48。这个数刚好小于 5/2,足够让 Flint–Hills 级数收敛。第二部分,它把第一部分的插值与行列式技术当作起点,不再依赖 62/25,一路推到 2。

还有一个细节。参考文献第 17 条写着:OpenAI,《Catalan 常数是无理数》,2026。这是同一个仓库里的第 005 号。摘要里一次又一次提到,是那篇关于 Catalan 常数的论证,给了它“算术与解析相比较”的思路。README 也说了,有些结果建立在模型此前的结果之上。[1][4]

它在引用自己。


那么,这一跳是谁的?

反对的声音来得很快,也很重。十月七日,Terence Tao 在自己的博客上转贴了“人类数学协会”(AHM)的声明:七百多份文件同时发布,是力量的展示,不是学术;数学家没有要求做这件事;他们呼吁数学家停止与 OpenAI 合作。[6]

Tao 自己的话温和一些,但分量更重。据《财富》的报道,他认为找到解答的过程,比解答本身更重要。从前,一个重大证明会带来报告、讨论班、新的合作者、教科书里的新章节;方法、失败的路、顺手冒出来的新问题,都长在这个过程里。一个问题被解决了,就不能再“未解决”一次。成批地收割开放问题,土地会变得贫瘠。他说,“数学 1.0”到此为止了,“数学 2.0”要重新看重讲解与共同体。[7]

多伦多大学的 Dan Litt 说,这些结果对数学是好事。他担心的是别处:如果公众觉得“AI 已经把数学解决了”,经费会少,年轻人会不来。纽约大学的 Tristan Buckmaster 则质疑,OpenAI 没有做足功课,去确认模型没有借用别人尚未发表的工作。[7]

还有发布方式。九月,OpenAI 在普林斯顿高等研究院设立了一个独立的顾问组。顾问组的建议包括:按传统论文的格式发布,公开模型、提示、耗时和成本,说明题目是怎么选的,报告失败的尝试。OpenAI 采纳了一部分,没有全部采纳。[7]差不多同一时间,另一项由 AI 给出关键想法的结果,3SUM 与全源最短路,是由 Josh Alman 和 Virginia Vassilevska Williams 两位人类学者写成论文发布的。[5]同一件事,可以有不同的交法。


说说我自己怎么看。

**第一,这一跳很可能是真的。**至少形式化了的那一部分,正确性上没有什么好争的。“只是组合已有的想法”“没有真正理解”,这类说法我在《临界线上的领土》里就不太同意,现在更不同意了。四十二页的失败记录,不像是在背答案。

**第二,变的不只是速度,是单位。**过去数学进步的单位是一个定理,一篇论文,一个名字。这次的单位是一份目录:四千道题,三小时一道,按重要程度过筛。这和比蒙不一样。比蒙是选手里的一个,他那一跳之后,别人知道了沙坑可以那么远,于是接着练。这一次,起跳的不在跑道上。

**第三,证明的价格在往零走,理解的价格没有变。**我在《没人打分的地方》里写过,数学是少数有铁面打分人的地方,所以机器在这里最先跑起来。现在看,打分人能管的只是“对不对”。“懂不懂”“值不值得”“接下来该问什么”,仍然没有人替我们打分。瓶颈从发现挪到了消化。七百一十九篇论文,四百多篇没形式化,几乎没有一篇被人读懂过,这才是这个仓库真实的样子。

所以我同意 Tao 的诊断,但不太同意 AHM 的药方。一刀切地不合作,解决不了“尺子不够长”;它只会让尺子更短。真正该要求的,是那些顾问组已经写下来的东西:论文写成人能读的样子,失败的尝试也公开,让一个结果和它的来路一起发布,而不是让三百多个结果在一个上午同时落地。

一个问题被解决,曾经同时意味着三件事:答案有了,方法有了,懂它的人有了。这一次,第一件事来得太快,后两件事还在路上。


比蒙的纪录保持了将近二十三年。一九九一年,迈克·鲍威尔跳出了 8.95 米。这二十三年里,跳远没有停,人们一直在跳。

比蒙那天跪下来,不是在落地的时候,是在听懂那个数字的时候。量出 8.90 米要一把卷尺,听懂它,还要有人把它翻译成他熟悉的单位。

这七百一十九篇论文,现在缺的就是这样的翻译:把一个数字,变成一个人能懂的距离。


Mathematics

Beamon's Leap

比蒙之跃

October 1968, the Mexico City Olympics, the long jump final. Bob Beamon landed his first jump, and the optical rail of the electronic measuring device slid to the end of its track without reaching his mark. The officials had to go and find a tape measure.

It came to 8.90 metres. The world record had been 8.35. For more than thirty years the long-jump record had moved forward a centimetre at a time: Jesse Owens’s 8.13 metres from 1935 stood for twenty-five years. Beamon added fifty-five centimetres in one jump.

He didn’t think in metres. Someone converted it for him into feet: twenty-nine feet, two and a half inches. When he understood, he dropped to his knees beside the runway.


On October 6, 2026, OpenAI opened a repository on GitHub called openai/math.[1]

The README is short. It says they have been evaluating their models on open research problems, that performance on their existing mathematical evaluations had saturated, and that they expanded the evaluations as a result. The repository holds what an unreleased internal model produced: 719 papers, grouped into 372 “result families” and sorted by discipline.

The method is described there too. The model was posed roughly four thousand problems. The great majority of results came out of the same fixed procedure, each using on average about three hours of ChatGPT Pro–level thinking compute. The output was grouped into families and then filtered for significance, and what was left is this catalogue. About 42% of the top-line results come with Lean formalizations; the rest do not. The README says so plainly: some of the unformalized results could have issues.[1]

I read all 372 family titles from top to bottom.[2] About halfway through, I could no longer read them as a list.

Khot’s Unique Games Conjecture: proved. L = RL = BPL: randomness can be removed from logarithmic space entirely. Hadwiger’s conjecture: a counterexample. Kaplansky’s zero-divisor conjecture: a counterexample. Thompson’s group F is nonamenable. The free group factors L(F2)L(\mathbb F_2) and L(F3)L(\mathbb F_3) are isomorphic. Hilbert’s tenth problem over the rationals has a negative answer. The plane cannot be coloured with five colours, so its chromatic number is six or seven. Borsuk’s conjecture already fails in dimension nine. The rational Hodge conjecture for CM abelian varieties. Integer multiplication below nlog⁡nn\log n.

The papers are dated from September 23 to October 7.

Any one of these, in an ordinary year, would keep its field busy for twelve months. Scott Aaronson titled his post that day “The Mathocalypse” and called it one of the biggest days in mathematical history.[5]


Two of the results can be drawn on the same page.

The first is π. How well an irrational number can be approximated by fractions is measured by its irrationality exponent: the smaller the exponent, the harder it is to approximate. Almost every real number has exponent 2, and people believed π did too, but believing is not proving. In 1953 Mahler showed that the exponent of π is at most 42. Over the next seventy years the bound was pushed down a piece at a time: 20, 19.89, 8.016, 7.606. In 2020 Zeilberger and Zudilin brought it to 7.103.

Family 017 in the repository: the irrationality exponent of π is exactly 2.[2]

Settled along the way is the notoriously stubborn Flint–Hills series, ∑1/(n3sin⁡2n)\sum 1/(n^3\sin^2 n). It converges.

The second is matrix multiplication. Multiplying two n×nn\times n matrices takes about nωn^\omega operations at best. Nobody knows what ω is, only that it is at least 2. In 1969 Strassen brought it down from 3 to 2.808 and shook the field. Over the next twenty years successive generations pushed it to 2.376; over the thirty-odd years after that, seven or eight papers ground it from 2.376 down to 2.3713. A war fought in the fourth decimal place.

Family 107: ω≤9/4\omega \le 9/4.[2]

Irrationality exponent of π (upper bound, log scale)251020421960198020002020floor = 2Mahler 1953Hata7.103 (2020)2 (2026, claimed)Matrix multiplication exponent ω (upper bound)2.02.252.52.81198020002020floor = 2Strassen 19692.376 (1990)2.3713 (2024)9/4 (2026, claimed)
Figure · Two records. Left: upper bounds on the irrationality exponent of π (log scale), from Mahler's 42 in 1953 to Zeilberger–Zudilin's 7.103 in 2020. Right: upper bounds on the matrix multiplication exponent ω, from Strassen's 2.808 in 1969 to 2.3713 in 2024. The ink staircase is the succession of records in the human literature; the dashed coloured line is the value claimed in openai/math (2 for π, 9/4 for ω). According to the repository both come with Lean formalizations; neither has been peer-reviewed. The dotted horizontal line on each side is the theoretical floor of 2.

Two months ago, in Territory on the Critical Line, I called progress on the road to the Riemann Hypothesis a “war of centimetres”: thirty years, less than one percentage point. That essay was about an exception. Looking back, the exception has turned wholesale in two months.

And there is news from the critical line, too. Family 003 calls it the “quasi-Riemann hypothesis”: every Dirichlet L-function, ζ included, has no zeros anywhere in the half-plane Re⁡s>7/8\operatorname{Re}s>7/8.[2] For more than a century, every known zero-free region has hugged the edge Re⁡s=1\operatorname{Re}s=1, growing narrower as you go up until its width tends to zero. Nobody had ever been able to draw a fixed vertical line and say there are no zeros to its right. If this paper holds, the zeros are shut inside the strip between 1/8 and 7/8, and Landau–Siegel zeros are ruled out along the way. It is still a long way from the Riemann Hypothesis, but it is a different kind of land claim. Last time the territory grew outward from the critical line; this time it is being closed in from outside.


When Beamon jumped, the measuring rail was too short. This time, too, the ruler is too short for the jump.

Start with what can be measured. For the results with Lean formalizations, the question “is there a mistake in the reasoning?” can be put to rest. As I wrote in Fermat Found a Truly Marvelous Proof, the kernel does not need to understand number theory; it only checks against the rules, and anyone can run that check again. Of the 719 papers, roughly three hundred have top-line results that have reached this point.[3]

But that essay also made the other half of the point: the tools can check a proof, but they cannot guarantee from a name alone that the statement is the result the reader thinks it is. Whether the formal statement matches the sentence in the paper still has to be checked by a person. The repository includes separate Comparator instructions for exactly this, which is the right thing to do.

The four hundred or so other papers are another matter.

On the second day, the first entry appeared in history.md. A paper on the algebraicity of Weil classes on split abelian eightfolds contained a sign error that broke a key cancellation argument. Two other papers built on it were withdrawn along with it. All three sit in the neighbourhood of the Hodge conjecture, and none was formalized. The same day, fourteen papers were revised and another thirteen updated their citations to match.[3]

I don’t think this is a scandal. Errors found, papers withdrawn, everything kept on record, earlier versions still accessible: that is a system working as it should. But it is also a reminder: one sign error brought down three papers, and before they were withdrawn, those three looked no different from the other seven hundred.

Two other things deserve a careful reading. The README says that the quasi-Riemann hypothesis and the Hodge conjecture for CM abelian varieties are precisely the two results that did not come from the fixed procedure, and that the writeup of the 11/12 version was edited by people for readability.[1] The two most eye-catching results are the exceptions. The repository does not say how they were exceptional.

In the same post, Aaronson wrote that some of the results carry Lean certificates, but almost no human has yet understood any of these proofs. His wife, Dana Moshkovitz, has worked on the Unique Games Conjecture for years; she found the papers poorly written and hard to read without help from an AI.[5]

Peer review in mathematics was designed for a pace of a few papers a year. Refereeing one long paper can take months. Seven hundred arrived in one morning.


The repository also released ten reasoning summaries. I read the one for π.[4]

Forty-two pages. A summary, and abridged at that. Almost every page is a failure.

It tried Padé approximation, Salikhov’s complex-endpoint method, the BBP formula, Toeplitz matrices, modular forms, interpolation among CM conjugates, a multivariable version of Roth’s theorem, and then used Liouville numbers to refute itself. Every road ran into the same wall: whatever margin it saved on the analytic side was eaten by the arithmetic cost of the denominators. Here and there the summary keeps a line of the original, like scrawl in the margin of a lab notebook:

The first thing it reached was not 2 but 62/25, which is 2.48. That is just under 5/2, enough to make the Flint–Hills series converge. In the second part, it took the interpolation-and-determinant technique from the first part as a starting point, stopped relying on 62/25, and pushed all the way to 2.

One more detail. Reference 17 reads: OpenAI, Catalan’s constant is irrational, 2026. That is family 005 in the same repository. Again and again the summary credits that Catalan argument with suggesting a comparison between the arithmetic and the analytic sides. The README says it too: some results build on the model’s earlier results.[1][4]

It is citing itself.


So whose leap is this?

The objections came fast and hard. On October 7, Terence Tao reposted on his blog a statement from the Association for Human Mathematics: releasing seven hundred files at once is a demonstration of power, not scholarship; mathematicians did not ask for this work; mathematicians should stop working with OpenAI.[6]

Tao’s own words are milder, and carry more weight. According to Fortune, he holds that the process of finding a solution matters more than the solution itself. A major proof used to bring talks, seminars, new collaborators, a new chapter in the textbooks; the methods, the failed paths, the new questions that turn up along the way all grew out of that process. Once a problem is solved, it cannot be unsolved. Harvesting open problems in bulk leaves the ground less fertile. He said this marks the end of “Math 1.0”, and that “Math 2.0” must value exposition and community.[7]

Dan Litt of the University of Toronto said the results are good for mathematics. His worry lies elsewhere: if the public comes to believe “AI has solved math”, funding shrinks and young people stay away. Tristan Buckmaster of NYU questioned whether OpenAI had done enough to make sure its model wasn’t drawing on other people’s unpublished work.[7]

Then there is the manner of release. In September OpenAI set up an independent advisory group hosted at the Institute for Advanced Study in Princeton. Its recommendations included publishing in traditional paper format; disclosing the model, prompts, time and cost; explaining how problems were chosen; and reporting failed attempts. OpenAI adopted some of them, not all.[7] At around the same time, another result whose key idea came from an AI, on 3SUM and all-pairs shortest paths, was written up and released as a paper by two human researchers, Josh Alman and Virginia Vassilevska Williams.[5] The same kind of result can be handed over in different ways.


Here is what I think.

First, the leap is very likely real. At least for the formalized part, there is not much left to argue about on correctness. I already didn’t much agree, in Territory on the Critical Line, with lines like “it’s only recombining existing ideas” or “it doesn’t really understand”. I agree with them even less now. Forty-two pages of failures do not read like recitation.

Second, what has changed is not only the speed but the unit. The unit of mathematical progress used to be a theorem, a paper, a name. This time the unit is a catalogue: four thousand problems, three hours apiece, sifted by significance. That is not like Beamon. Beamon was one of the athletes. After his jump, everyone else knew the sandpit could be that far away, and went back to training. This time, the one who jumped was never on the runway.

Third, the price of a proof is heading towards zero; the price of understanding has not moved. In Where No One Is Keeping Score I wrote that mathematics is one of the few places with an incorruptible scorer, which is why machines took off here first. It now looks as though the scorer can only rule on “right or wrong”. “Is it understood?”, “Was it worth doing?”, “What should we ask next?”: nobody is keeping score on those for us. The bottleneck has moved from discovery to digestion. Seven hundred and nineteen papers, four hundred unformalized, almost none yet understood by a person: that is what this repository really looks like.

So I agree with Tao’s diagnosis, but not quite with the AHM’s prescription. Refusing to cooperate across the board does nothing about the ruler being too short; it only makes the ruler shorter. What is worth demanding is what the advisory group has already written down: papers written so that people can read them, failed attempts published too, each result released together with the path that led to it, rather than three hundred results landing on the same morning.

A problem being solved used to mean three things at once: there was an answer, there was a method, and there were people who understood it. This time the first arrived too fast, and the other two are still on their way.


Beamon’s record stood for nearly twenty-three years. In 1991 Mike Powell jumped 8.95 metres. Through those twenty-three years, the long jump did not stop. People kept jumping.

When Beamon went down on his knees that day, it wasn’t on landing. It was when he understood the number. Measuring 8.90 metres took a tape measure; understanding it took someone to translate it into units he knew.

That is what these 719 papers are missing now: a translation that turns a number into a distance a person can understand.


❧