Day: 9 September 2026

A 50-year-old computer-assisted proof

Posted on by John

The idea of using computers to assist with proofs is not new. The first major computer-assisted proof was published in 1976, the proof of the four color theorem by Kenneth Appel and Wolfgang Haken. The authors reduced the proof of the four color theorem to verifying calculations on 1,834 configurations, each checked by a computer program.

The proof was simplified over the years, and formalized in Coq in 2005. Everyone is satisfied that the theorem is true, but there has never been a satisfying proof, one that a human could read and say “I see now why any map can be colored using only four colors.” And there may never be one, but see this post for a contrary prediction.

The IBM mainframe that ran the calculations completing the proof of the four color theorem did not generate the proof. It simply executed the FORTRAN program that Haken and Appel (and Koch [1]) gave it.

I don’t see the recent proof of finite-time blowup for solutions to the Navier-Stokes equations as entirely different. Computers did higher-level tasks for the OpenAI team than the mainframe did for Haken and Appel, and these tasks were not as directly programmed as the tasks that were given to the mainframe, but still machines do what they are told to do.

Related posts

[1] John A. Koch was a programmer who worked on the four color proof with Haken and Appel. I don’t know how much credit he deserves, but I suspect it may be more than he was given.

AI is an intelligence multiplier

Posted on by John

A rising tide may lift all boats, but the AI tide lifts some boats much more than others.

By all accounts, the best programmers have had the biggest productivity boost from AI. And top tier mathematicians are using AI to settle long-standing mathematical conjectures. AI is a powerful tool, but tools don’t come to life and make things on their own.

I routinely have naive amateurs [1] send me proofs of open conjectures, and naturally more recent such proofs involve AI. I’ll get an email saying something like “I’ve solved the Collatz conjecture using ChatGPT, but I’m not a mathematician so I need some help verifying the proof.” And of course the supposed proof is rubbish.

The recent Navier-Stokes proof is impressive, but AI didn’t initiate the proof any more than LaTeX did. Nor did a child steer AI into proving the conjecture. Professional mathematicians were able to use AI to pursue their ideas at superhuman speed. But someone without an understanding of the Navier-Stokes problem, and familiarity with recent ideas for approaching the problem, could not have directed AI to produce a proof.

Computer scientists have been saying “garbage in, garbage out” from the beginning. A variation on this aphorism for the age of AI would be “mediocrity in, mediocrity out.”

***

[1] Amateurs can and do make contributions to mathematics. For example, in 2022 David Smith, a retired print technician, discovered a single shape that can be used to create an aperiodic tiling of the plane. By “naive amateurs” I mean people who literally do not know what they are talking about.

The part of Navier-Stokes no one is talking about

Posted on by John

Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as their conventional human-readable proof.

Quite a few other mathematical conjectures have been settled recently using AI, and these have also been accompanied with formal proofs, using Lean 4 in particular.

Until very recently, generating machine-verifiable formal proofs has been excruciatingly tedious. In 2005, Henk Barendregt and Freek Wiedijk wrote

To give an indication of how much work is needed for formalisation, we estimate that it takes approximately one work-week (five work-days of eight work-hours) to formalise one page from an undergraduate mathematics textbook.

That was the rule of thumb: forty hours per page. And this in the context of undergraduate textbooks. Research publications are much denser than textbooks. Furthermore, page 100 of a textbook probably depends mostly on material on pages 1 through 99. A sentence in a research article could cite anything that has been published before.

Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook. Then formalizing the 166-page paper from OpenAI would take 132,800 person-hours. It took OpenAI 17 hours to verify their proof in Lean. I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude is revolutionary.

I’ve used AI to generate formal proofs to check my work just for a little blog post. I wouldn’t dream of doing that if I had to pay someone a week’s salary to check my work.

Formal verification doesn’t just apply to mathematics. You could, for example, formally verify that a set of security policies are consistent and that, given certain assumptions, they accomplish their purpose. You could formally verify that a smart contract imposes a certain maximum liability. You could verify the correctness of mission-critical algorithms. These problems are easier than formalizing mathematics research, and it is easier to quantify the return on investment.

Related posts