Thoughts on OpenAI solving a Millenium Prize problem

8 Sep 2026

Earlier today, OpenAI published an announcement claiming to have solved the Navier-Stokes Millenium Prize problem by proving that solutions to the Navier-Stokes equations in three dimensions can develop singularities. They found this proof by throwing huge amounts of computational power at an “internal model” that is apparently more advanced than anything publicly available. The ethics of some of OpenAI’s behavior are in doubt; see for example this statement by Tristan Buckmaster of NYU, who (along with Levent Alpöge of Anthropic) found solutions to related conjectures using publicly-available LLMs in the period just before OpenAI’s effort. Such controversies aside, the solution of such a high-profile open problem in mathematics by an AI model is very big news. My initial reactions are as follows:

• I need to start paying more attention to AI. Until now, I have hardly used LLMs at all, other than the “AI Overview” that often shows up when I search something on Google, and have been pretty much oblivious to advances in LLM capabilities. This is despite the fact that I understand the basics of machine learning, having taken an undergraduate machine learning course two years ago (and having studied the subject a little in my free time), and am not anti-AI per se.* I don’t intend on becoming a chronic user of Claude or ChatGPT or whatever, but I definitely intend on learning how to use AI models to generate mathematical proofs, since it looks like that will be an important skill to have in the future.

• It is interesting that theorem-proving languages like Lean are seeing so much use now. I became interested in such languages, along with the mathematical field of type theory on which they are based, more than five years ago. At the time, it seemed that theorem-proving languages were interesting from a theoretical standpoint, but not of much practical use. That has clearly changed.

• One must not forget that the purpose of mathematics is to advance human understanding. Just as a proof by brute-force computation is less useful than a proof involving some additional insight, a proof that is largely or entirely generated by an LLM will almost always be less useful than one that is not. In the case of many conjectures, the resolution of the conjecture itself is not as important as the body of theory developed in order to prove the conjecture. This isn’t to say that AI-generated proofs are useless, of course; a proof of the Riemann hypothesis would (in contrast to this Navier-Stokes problem) have many implications, even if it were a total black box of pure calculus of constructions, say.

• I say “human understanding”, but that is really redundant. Although anthropomorphism can be useful sometimes, there is no such thing as “AI understanding” in a literal sense — AI models cannot understand things, because they do not have thoughts or feelings.

[*I do find the usual writing style of LLMs to be tasteless, and believe that one should not treat them as authoritative sources of information, especially in light of their known political biases.]