OpenAI, the Millennium Problems and the bar for proof

On 8 September, MIT Technology Review reported that OpenAI has announced that its agents solved one of the Millennium Prize Problems, the list of seven open questions the Clay Mathematics Institute endowed with a million dollars each back in 2000. Under normal circumstances that would be the largest mathematical achievement ever credited to an AI system. The announcement, however, arrived surrounded by accusations, and that is the part worth looking at slowly (MIT Technology Review).

It helps to set the scale. Of the seven problems, only one is considered solved: the Poincaré conjecture, proved by Grigori Perelman in the early 2000s and validated by the community after years of review. That is the bar, and it is not a bureaucratic detail. In mathematics a result does not exist because someone announces it, but when other people capable of finding the flaw fail to find it. The process takes months or years, and it is precisely what a corporate statement cannot replace.

The article details the accusations that have clouded the announcement, and that outcome is not yet written. Handing out verdicts from the outside with first day information would be premature. What can be analysed, and what will repeat itself next time, is the mechanism: how a result like this is communicated, what is offered as evidence, and how long it takes for an independent check to exist.

Generating is not proving

The distinction matters because current models are extraordinarily good at producing text shaped like a proof. A mathematical proof has recognizable structure, vocabulary and rhythm, and that is exactly the kind of pattern a model learns well. The difference between a correct proof and one that breaks at step fourteen is not on the surface of the text: you have to follow it line by line. A competent human reviewer takes weeks to do that with a long paper, and the reviewers able to audit a Millennium Problem can be counted on one hand.

There is a technical way out of that bottleneck and it is not new: formalization. Proof assistants like Lean, with its mathlib library, allow mathematics to be written in a language a machine verifies exhaustively. If a proof compiles in Lean, it is correct, with no committee and no good faith involved. In 2024 DeepMind showed with AlphaProof that a system could reason inside that framework at silver medal level in the International Mathematical Olympiad.

That is why the relevant question facing any announcement of this kind is not whether the model is powerful, but in what format the result was delivered and who checked it. If there is a verifiable formal artifact, the discussion closes quickly and in public. If what there is amounts to a PDF and a press release, the timeline is set by peer review, not by the communications department.

What this leaves for people working with agents

The lesson jumps from mathematics to anyone putting agents to work. An agent produces plausible output with disarming fluency, and plausibility is not correctness. In software that is handled with tests, types and CI: the model proposes and a machine rules. In domains without an automatic verifier, the cost of checking grows until it eats the speed gain, and that is where many deployments stall without quite admitting it.

Which is why the boring work, building the verifier before the generator, remains the one that pays off most. Defining what counts as a valid result, automating that check and letting the agent iterate against it is what separates a pilot that impresses in a demo from something you can leave running in production.

Our position is deliberately dull: announcements get read, results get verified, and months fit between the two. The MIT Technology Review piece is right not to settle the matter, because the ones who have to settle it are the mathematical community and not a press room.