A mathematician from New York University and a researcher at Anthropic published on 8 September a proof of finite-time blow-up for the incompressible Euler equations in three dimensions under regular forcing, extending an earlier result obtained under coarser assumptions. The work was carried out with the help of Claude and Codex. The decisive point: the proof is formally verified.
On Saturday we asked the question of what a proof is when no one can verify it. Here is the answer, two days later, and it is better than we had hoped.
What "formally verified" means
This is the difference between this announcement and the ones we have covered previously.
When a model produces a proof in natural language, you either have to trust it or read it all over again. We have stressed how misplaced that trust is, given that these systems are as confident when they are wrong as when they are right.
A formally verified proof is written in a language that the computer can check line by line. Each step must follow mechanically from the previous ones, according to explicit logical rules. If a single step does not hold, the verifier rejects it.
The consequence is decisive: you no longer need to trust the model. You only need to trust the verifier, which is a relatively simple program, written by humans and audited by the community for years.
Why this is the right setup
This was exactly what we were calling for on Saturday, and it is worth stating clearly.
The model does what it does well: propose. Explore avenues, suggest lemmas, try constructions, produce volume. This is work where endurance matters, and where being wrong often does not matter as long as you occasionally hit the mark.
The verifier does what the model cannot do: guarantee. It understands nothing, it proposes nothing, it simply checks that each step is valid.
This division resolves the problem of the dual use of trust. It turns an unverifiable result into a verified one, without requiring a human to read the whole thing.
Three things remain beyond the verifier's reach, and they need naming. It validates that the proof is correct, not that it is interesting: judging the importance of a result remains human. It validates the demonstration, not the statement: if the formalised question does not match the one you meant to ask, the proof is valid and beside the point. And it says nothing about the respective share of human and machine in the discovery, a question we address this evening in a separate article.
Why this particular result matters
Without going into the technicalities, the equations in question describe the flow of a perfect fluid. Whether their solutions can become infinite in finite time — what is called a blow-up — is a central problem in mathematical physics, related to one of the great open questions in the field.
This is therefore not a demonstration exercise: it is a subject on which mathematicians have worked for decades, and where an earlier result had just been obtained under less satisfactory assumptions. Extending that result to a more regular setting is real progress.
What it says about use in research
This case sheds light on a distinction we drew in our article on whether models can have ideas.
We reported a test in which models largely failed to recover the idea of a paper from its premises alone, with scores between 3 and 15%. We concluded that these systems excel at exploiting the known and stumble on what is not.
This work does not contradict that finding; it refines it. The model did not have the intuition in place of the researcher: it multiplied their capacity to explore, test and formalise. This is a collaboration in which the human keeps the direction and delegates the endurance.
This is probably the most productive setup, and it is very different from the one suggested by press releases announcing that a model has solved open problems.
What to take away
This result matters to mathematicians, and it matters just as much as a methodological model.
It shows that these systems can be used in a framework where their main flaw — producing plausible output with confidence — is neutralised by an external device. This is not trust; it is verification.
We wrote on Saturday that a proof no one can verify is not yet a proof, but that it can become one if you can verify what verifies it. That is exactly what has just been done. The remaining question is whether this requirement will become the norm, or whether results will keep being announced without it because it is faster.