今年 9 月 8 日中午，OpenAI 宣布：它的上万个 AI 智能体证明了，三维 Navier–Stokes 方程在加上一个光滑的外力之后，可以在有限时间里“爆掉”。这是克雷数学研究所 2000 年悬赏一百万美元的七个千禧年难题之一，也是其中离日常生活最近的一个，因为它描述的就是水和空气怎么流动。

这条新闻让我想起五十年前的另一个夏天。1976 年 7 月，美国伊利诺伊大学的两位数学家宣布，他们靠一台计算机证明了四色定理。

两件事隔了整整五十年，问的却是同一个问题：一个主要由机器完成的证明，我们凭什么相信它？又从中懂得了什么？

这篇文章沿着这五十年走一遍。结论先放在这里：机器先是替我们算，后来替我们查，现在开始替我们写；越来越稀缺的，是判断。

四色问题是 1852 年提出的：随便画一张地图，只要求相邻的区域颜色不同，四种颜色够不够用？题目简单到小学生都能听懂，却难住了数学家一百多年。

三种颜色有时确实不够。主图左边那张小地图就是例子：中间一个国家，被五个国家围成一圈。外圈的五个国家首尾相接，要三种颜色才涂得开；中间的国家和它们全都相邻，只好用第四种颜色。

阿佩尔（Kenneth Appel）和哈肯（Wolfgang Haken）的办法，是把无穷化为有限。第一步，证明任何地图里都一定藏着某种局部结构，他们一共找出 1936 种，组成一个“不可避免集”。第二步，逐一证明每一种结构都可以被化简掉，也就是“可约”。第一步主要靠人，第二步交给计算机，在伊利诺伊大学的 IBM 计算机上跑了上千个小时。

证明完成后，伊利诺伊大学数学系把邮资机上的戳记改成了一句话：Four Colors Suffice，四色足矣。这枚邮戳用了好几年，如今还收藏在美国史密森尼博物馆里。

庆祝之外，是长久的不安。上千种情形，没有人能用手检查一遍。数学史上第一次，接受一个证明需要“相信一台机器”。1979 年，哲学家蒂莫兹科（Thomas Tymoczko）发表了一篇有名的论文，认为四色定理把一种“实验”带进了数学：我们接受它，不是因为读懂了它，而是因为相信计算机没有出错。

二十多年后，同样的不安又来了一次。1998 年，黑尔斯（Thomas Hales）宣布证明了开普勒猜想：同样大小的球怎么堆最省空间，答案就是水果摊上堆橙子的那种堆法。证明里同样有大量计算机计算。《数学年刊》请了 12 位审稿人，查了四年多，最后只敢说“99% 确定是对的”。

黑尔斯的回应很硬气：既然人查不完，就让机器把每一步都查一遍。2003 年，他启动了 Flyspeck 计划，用证明助手把整个证明改写成机器能逐行检查的形式。这项工作做了 11 年，2014 年 8 月完成。

差不多同一时期，冈蒂耶（Georges Gonthier）用证明助手 Coq，把四色定理从头到尾重新验证了一遍，2004 年完成，代码约六万行。从此，相信四色定理不再需要相信当年那台 IBM，只需要相信一个很小的检查内核。

后来，形式化越来越快。2020 年底，菲尔兹奖得主舒尔策（Peter Scholze）担心自己一个关键证明里藏着漏洞，向 Lean 社区发起挑战，一年半后验证完成。2023 年，陶哲轩和合作者的一个新定理，从论文到 Lean 只用了三周。

这二十多年里，机器的角色变了，从替人算，变成了替人查。“相信我”变成了“你自己跑一遍”。检查第一次变得便宜。

再下一步，机器开始自己写证明。2024 年，DeepMind 的 AlphaProof 在国际数学奥林匹克竞赛中达到银牌线；2025 年，Gemini Deep Think 拿到经过官方认证的金牌线（满分 42 分得 35 分），OpenAI 的模型也报告了同样的成绩。

不过竞赛题有标准答案，研究问题没有。真正的转折，发生在流体方程上。

流体方程会不会“爆破”，几十年来几乎只能靠数值模拟去猜。2022 年，侯一钊（Thomas Hou）和 Jiajie Chen 用计算机辅助证明，严格证明了带边界的三维 Euler 方程（不考虑黏性的流体方程）可以从光滑的初始状态出发爆破。所谓计算机辅助，是让计算机做数值计算，但每一步的误差都用区间算术给出严格的上界，所以结论和手算一样可靠。

2025 年 9 月，DeepMind 和 Gómez-Serrano、Buckmaster、Ching-Yao Lai 等数学家合作，用神经网络找到了几族“不稳定”的奇点解，精度逼近计算机双精度的极限。神经网络负责找，严格数值负责证。到 2025 年，这条“机器搜索、机器验证”的路已经铺好了。

Navier–Stokes 方程由法国工程师纳维（1822）和英国数学家斯托克斯（1845）先后写下，描述水、空气这类有黏性的流体怎么流动。天气预报、飞机设计、血管里的血流，都离不开它。

千禧年难题问的是一件看似朴素的事：在三维空间里，从一个光滑的初始状态出发，解会不会永远保持光滑？还是说，流速可能在有限时间内、在某一点变成无穷大？后一种情况叫“爆破”，那个点叫“奇点”。

克雷研究所的官方题目由数学家费弗曼（Charles Fefferman）执笔，给了四个选项，证出其中任何一个都算解决：

OpenAI 宣布证明的，是（C）和（D）：对任意大小的黏性，都可以构造一个光滑、只作用在有限区域里的外力，让一团原本静止的流体，在总能量始终有界的情况下，到时刻 1 时流速变成无穷大。

按 OpenAI 公布的数字，一个多智能体系统从 9 月 1 日开始运行，至少一万个智能体并行工作了 88 个小时，消耗约 1300 亿个输出 token，写成 166 页的论文；随后又用 17 个小时，把它翻译成 Lean 4 的形式化证明。这个 Lean 工程是公开的，任何人都能下载编译，让机器把每一步再检查一遍。

爆破是怎么造出来的？核心思路来自马德里的两位数学家，科尔多瓦（Diego Córdoba）和马丁内斯-索罗亚（Luis Martínez-Zoroa）。他们和合作者在几年里的一系列工作中，搭出了一种“无穷级联”：解由无穷多层涡旋叠成，每一层都比上一层更强、更靠近中心、存在的时间更短。层数是无穷的，时间加起来却是有限的，奇点就出现在那个时刻。

他们已经用这套办法让方程的几种变体爆破，但一直差最后一步：让外力本身完全光滑。据《Quanta》杂志报道，补上这一步的，正是 AI。

不会。布朗大学的流体力学家卡尼亚达基斯（George Karniadakis）指出，对空气来说，这样的奇点要等涡旋缩到大约 70 纳米宽才会出现，这已经和空气分子的平均自由程相当，“流体是连续的”这个前提先失效了。所以，这是一个关于数学模型的定理，不是关于明天天气的预言。

还有一点更要紧：大家最关心的不加外力的情形，也就是（A）和（B），依然没有答案。

消息出来以后，各方的反应很能说明问题。

9 月 11 日，克雷研究所表态：这个问题“看来已经解决”，但评审过程会“刻意不着急”。按规则，结果要在正式刊物上发表，再经过至少两年的检验。截至我写这篇文章时（10 月初），还没有公开的独立核验结论，问题状态被标为“进行中”。OpenAI 自己也表示，不打算申领这一百万美元。

当年为克雷研究所写下题目的费弗曼说，他很高兴看到问题被解决，但这个故事真正的英雄，是科尔多瓦和马丁内斯-索罗亚。

几乎同时，还有另一组人在做同一件事。纽约大学的布克马斯特（Tristan Buckmaster）和合作者阿尔波格（Levent Alpöge，任职于另一家 AI 公司 Anthropic，两人称这是私人合作）借助几家公司的 AI 模型，证明了带光滑外力的 Euler 方程等几个相关结果，比 OpenAI 早大约 12 小时公布。随后布克马斯特公开表示，OpenAI 的工作受到了他们进展的启发；OpenAI 否认接触过他们的工作。双方各执一词，至今没有定论。

也是 9 月 11 日，二十多位菲尔兹奖得主联名发表公开信，题为《AI 在数学中的严重错位》。他们担心 AI 公司把悬而未决的难题当成刷榜题目，发布太急，留给写作和引用的时间太少，来源和署名都说不清。信里强调，一个解答最有价值的地方，是人能读懂它、学会它的方法，再用这些方法做出新的东西。陶哲轩说得更直接：解决这些难题，只是“增进理解”这个主要目标的替代指标。

这两年我常用一句话概括 AI 带来的变化：生成塌了，验证没塌。今年九月的事，让我想把这句话说得更准确一些。

生成确实塌了。五十年前，两位数学家加一台大型机，花了好几年；今天，一万个智能体，三天半。

验证的最底层，其实也在塌。一份 166 页的证明，逐行交给机器检查，只用了 17 个小时。

没塌的，是判断。今年 8 月，有两位研究者把“验证”拆成三层：推导是否有效，形式化的命题是否忠实于原来的问题，结果有什么意义。只有第一层能交给机器。

落到这次的事情上，至少有三件事，机器替代不了我们。

所以，我想把那句话改成：生成塌了，检查也快塌了，判断没塌。

1976 年的问题是：机器算的，我们查不了。2026 年的问题变成了：机器写的，我们查得了，却未必读得懂。

五十年前，伊利诺伊大学的邮戳上印着“四色足矣”。要是今天也刻一枚邮戳，我想刻的是：

“证明可以交给机器，
理解还得我们自己来。

At noon on September 8 this year, OpenAI announced that more than ten thousand of its AI agents had proved that the three-dimensional Navier–Stokes equations, once a smooth external force is added, can “blow up” in finite time. This is one of the seven Millennium Prize Problems for which the Clay Mathematics Institute offered a million dollars each in 2000, and the one closest to everyday life, because it describes how water and air flow.

The news reminded me of another summer, fifty years ago. In July 1976, two mathematicians at the University of Illinois announced that, with the help of a computer, they had proved the four color theorem.

The two events are a full fifty years apart, yet they raise the same question: when a proof is done mostly by a machine, on what grounds do we believe it? And what do we come to understand from it?

This essay walks through those fifty years. Here is the conclusion up front: machines first computed for us, then checked for us, and are now starting to write for us; what grows ever scarcer is judgment.

The four color problem was posed in 1852: draw any map, and ask only that neighboring regions get different colors; are four colors always enough? The question is simple enough for a schoolchild to follow, yet it stumped mathematicians for more than a century.

Three colors are sometimes not enough. The small map on the left of the main figure is an example: one country in the middle, ringed by five others. The five in the outer ring join end to end, so they need three colors between them; the country in the middle borders all five, so it has to take a fourth.

Kenneth Appel and Wolfgang Haken's approach was to turn the infinite into the finite. Step one: prove that every map must contain one of a certain collection of local configurations. They found 1,936 of them in all, forming an “unavoidable set.” Step two: prove, one by one, that each of these configurations can be reduced away, that is, that it is “reducible.” Step one was mostly done by people; step two was handed to a computer, and it took more than a thousand hours on the University of Illinois's IBM machine.

After the proof was finished, the University of Illinois math department changed the stamp on its postage meter to a single line: “Four Colors Suffice.” The postmark was used for several years, and it is now in the collection of the Smithsonian.

Beyond the celebration lay a long unease. More than a thousand cases, and nobody could check them all by hand. For the first time in the history of mathematics, accepting a proof meant “trusting a machine.” In 1979, the philosopher Thomas Tymoczko published a well-known paper arguing that the four color theorem had brought a kind of “experiment” into mathematics: we accept it not because we have understood it, but because we trust that the computer made no mistake.

More than twenty years later, the same unease came back. In 1998, Thomas Hales announced a proof of the Kepler conjecture: the densest way to pack equal spheres is the way oranges are stacked at a fruit stand. This proof, too, relied on a great deal of computer calculation. The Annals of Mathematics brought in 12 referees, who spent more than four years on it and in the end would only say they were “99% certain” it was correct.

Hales's response was defiant: if people can't check it all, let a machine check every step. In 2003 he launched the Flyspeck project, using proof assistants to rewrite the entire proof in a form a machine can check line by line. The work took 11 years and was completed in August 2014.

At around the same time, Georges Gonthier used the proof assistant Coq to verify the four color theorem again from start to finish, completing it in 2004 with about 60,000 lines of code. From then on, believing the four color theorem no longer required trusting that IBM machine from years ago, only a very small checking kernel.

After that, formalization got faster and faster. At the end of 2020, the Fields medalist Peter Scholze, worried that one of his key proofs might hide a gap, put out a challenge to the Lean community; the verification was finished a year and a half later. In 2023, a new theorem by Terence Tao and his collaborators went from paper to Lean in just three weeks.

Over those twenty-odd years, the machine's role changed from computing for us to checking for us. “Trust me” became “run it yourself.” For the first time, checking became cheap.

The next step was for machines to write proofs themselves. In 2024, DeepMind's AlphaProof reached the silver-medal level at the International Mathematical Olympiad; in 2025, Gemini Deep Think reached an officially certified gold-medal level (35 out of a possible 42 points), and OpenAI reported the same score for its model.

But competition problems have known answers, and research problems don't. The real turning point came with the equations of fluids.

For decades, whether fluid equations can “blow up” could only be guessed at with numerical simulations. In 2022, Thomas Hou and Jiajie Chen used a computer-assisted proof to show rigorously that the three-dimensional Euler equations with a boundary (the fluid equations without viscosity) can blow up starting from smooth initial data. “Computer-assisted” means the computer does the numerical calculation, but the error at every step is given a rigorous upper bound by interval arithmetic, so the conclusion is as reliable as a calculation by hand.

In September 2025, DeepMind, working with mathematicians including Gómez-Serrano, Buckmaster and Ching-Yao Lai, used neural networks to find several families of “unstable” singular solutions, with accuracy close to the limits of double precision. The neural networks did the finding; rigorous numerics did the proving. By 2025, the road of “machine search, machine verification” had been paved.

The Navier–Stokes equations were written down first by the French engineer Navier (1822) and then by the British mathematician Stokes (1845). They describe how viscous fluids such as water and air flow. Weather forecasting, aircraft design and the flow of blood in our vessels all depend on them.

The Millennium Prize problem asks something that sounds simple: in three-dimensional space, starting from a smooth initial state, does the solution stay smooth forever? Or can the velocity become infinite at some point within finite time? The second case is called “blowup,” and the point is called a “singularity.”

The Clay Institute's official problem statement, written by the mathematician Charles Fefferman, gives four options; proving any one of them counts as a solution:

What OpenAI announced is a proof of (C) and (D): for any value of the viscosity, one can construct a smooth external force, acting only within a bounded region, that makes a body of fluid initially at rest reach infinite velocity at time 1, while its total energy stays bounded throughout.

According to OpenAI's figures, a multi-agent system started running on September 1, with at least ten thousand agents working in parallel for 88 hours, using about 130 billion output tokens and producing a 166-page paper; it then took another 17 hours to translate the paper into a formal proof in Lean 4. The Lean project is public: anyone can download and compile it, and have a machine check every step again.

How is the blowup built? The core idea comes from two mathematicians in Madrid, Diego Córdoba and Luis Martínez-Zoroa. In a series of papers with collaborators over several years, they built an “infinite cascade”: the solution is a stack of infinitely many layers of vortices, each stronger than the last, closer to the center and shorter-lived. There are infinitely many layers, but their durations add up to a finite time, and the singularity appears at that moment.

They had already used this method to make several variants of the equations blow up, but they were always one step short: making the external force itself perfectly smooth. According to Quanta Magazine, it was AI that supplied this last step.

No. George Karniadakis, a fluid dynamicist at Brown University, has pointed out that for air, such a singularity would appear only once the vortex shrinks to about 70 nanometers across. That is comparable to the mean free path of air molecules, so the premise that “the fluid is continuous” breaks down first. This is a theorem about a mathematical model, not a forecast of tomorrow's weather.

There is a more important point, too: the case people care about most, the one with no external force, that is, (A) and (B), still has no answer.

The reactions after the news broke say a lot.

On September 11, the Clay Institute stated that the problem “appears to have been solved,” but that the review process would be “deliberately unhurried.” Under its rules, a result must be published in a recognized journal and then stand up to at least two years of scrutiny. As of this writing (early October), there is no public conclusion from independent verification, and the problem's status is marked “in progress.” OpenAI itself has said it does not plan to claim the million dollars.

Fefferman, who wrote the problem statement for the Clay Institute, said he was delighted to see the problem solved, but that the true heroes of the story are Córdoba and Martínez-Zoroa.

At almost the same time, another group was working on the same thing. Tristan Buckmaster of New York University and his collaborator Levent Alpöge (who works at another AI company, Anthropic; the two describe it as a personal collaboration) used AI models from several companies to prove several related results, including one for the Euler equations with a smooth external force, and announced them about 12 hours before OpenAI. Buckmaster then said publicly that OpenAI's work had been inspired by their progress; OpenAI denies having seen their work. Each side sticks to its own account, and the matter remains unsettled.

Also on September 11, more than twenty Fields medalists published an open letter titled “A Severe Misalignment of AI in Mathematics.” They worry that AI companies are treating open problems as leaderboard targets, announcing too hastily, leaving too little time for writing up and citing, and leaving both sources and authorship unclear. The letter stresses that the most valuable thing about a solution is that people can understand it, learn its methods, and use those methods to make something new. Terence Tao put it more bluntly: solving these problems is only a proxy for the main goal, which is “advancing understanding.”

For the past two years I have often summed up what AI has changed in one line: generation has collapsed, verification hasn't. What happened this September makes me want to put it more precisely.

Generation really has collapsed. Fifty years ago, it took two mathematicians and a mainframe several years; today, ten thousand agents took three and a half days.

The lowest level of verification is in fact collapsing too. Having a machine check a 166-page proof line by line took only 17 hours.

What hasn't collapsed is judgment. This August, two researchers split “verification” into three layers: whether the derivation is valid, whether the formalized statement is faithful to the original problem, and what the result means. Only the first layer can be handed to a machine.

Applied to this case, there are at least three things machines cannot do in our place.

So I would revise that line: generation has collapsed, checking is about to collapse, and judgment hasn't.

In 1976 the problem was: what the machine computed, we could not check. In 2026 it has become: what the machine writes, we can check, but we may not understand.

Fifty years ago, the University of Illinois postmark read “Four Colors Suffice.” If I were to carve a postmark today, I would want it to say:

“Proofs can be handed to machines;
understanding is still up to us.