AI’s claimed mathematical breakthrough: what did the proof checker verify?

When you stir the coffee in a cup with a spoon, small swirls are created. Even if you stop your hand, it spins for a while and then subsides. From the air around an airplane to the blood passing through blood vessels, the name that appears to describe this flow is the Navier-Stokes equation. Although it is a formula that has been used for a long time, it is still a difficult mathematical problem whether, under the specified conditions, solutions remain smooth for all time.

There is a $1 million prize at stake for this problem. It is one of the seven Millennium Prize Problems selected by the Clay Mathematics Institute in 2000. One million dollars was allocated to solve each problem. The familiar formula for explaining the movement of water remained a question worth a large prize to mathematicians.

An announcement was made that AI had found the answer to that question. However, if you follow the announcement and the verification debate, you will see that there are things to look at before the prize money. What exactly does it mean to say that a computer has confirmed the proof?

There are things we don't know about the formulas we already use.

The Navier-Stokes equations express the movement of fluids mathematically. However, the Millennium Prize Problem is not a matter of creating the equation for the first time or calculating the airflow of a specific airplane once. It asks whether the movement of a three-dimensional fluid that starts out sufficiently smooth remains smooth over time, or whether the solution may collapse at some point.

It is also important to treat water as a continuous substance rather than tracking it down to individual molecules. Just because a quantity grows infinitely large in a mathematical solution does not mean that actual coffee splatters at an infinite speed. There is a gap between the idealized world expressed by the equation and the actual movement of matter.

Between announcement and confirmation

OpenAI announced on September 8 that its internal AI system had found proof that the solution to the fluid equations creates a singularity in finite time. It is the result of conditions under which external forces act, and the company claimed that this solves items C and D of the formal problem. Both the human-readable proof and the proof formalized in Lean that computers can check were released.

The Clay Mathematics Institute also expressed its expectations for the announcement of a solution in a statement on September 11. It also said it would not rush the process of assessing the result and determining credit. When checked on October 15, the problem page was still marked “Active.”

The prize money is not paid out immediately upon announcement. The results must be published through a publication channel recognized by the institute, and at least two years have passed since then, and the results must be generally recognized by the world mathematics community to be considered for review. OpenAI said it does not intend to claim the Millennium Prize for these results. It was announced that the million-dollar question had been answered, but it does not mean that AI has already received the prize money.

Is the translated proof the same as the original proof?

One of the clues to understanding the controversy is ‘translation.’ Lean is a tool that expresses mathematical sentences in a defined format and mechanically checks whether the inferences are valid within that formal system. However, when translating a human-written sentence into that language, what happens if one condition is missing or the meaning is different? You should check whether the sentences that passed the test are the same as the sentences you originally intended to check.

The paper by Alexander Bastounis, Fabian Circelli, and Anders C. Hansen, released on October 6, points out this very gap. The researchers cited OpenAI's Navier-Stokes proof as an example and argued that natural language proofs and proofs formatted in Lean do not correspond. This publicly released paper should not yet be described as a peer-reviewed journal result, nor its argument as the final judgment of the mathematical community.

This does not mean that computer testing is useless. This means that you need to check what you entered to be checked. Even if the correct answer appears on the calculator, it is similar to looking again to see if the formula you entered the first time is the same as the formula written in the problem. The actual mathematical translation is much more complicated than the analogy, but it makes sense that there are two separate steps.

The swirl inside the cup subsides after a while, but the debate surrounding the proof that explains the movement continues. What is now in front of the $1 million prize are two types of documents rather than a check. Proofs read by humans and proofs checked by computers. Mathematicians are taking another look at whether two documents give the same answer to the same question.