OpenAI's Navier-Stokes Proof Still Needs Humans

StarTalk brought astrophysicist Mordecai-Mark Mac Low to stress-test OpenAI's claim that it has solved the Navier-Stokes existence and smoothness problem, one of the Clay Mathematics Institute's Millennium Problems, and the conversation turned skeptical fast.

The claim itself is stark. OpenAI says its system found a counterexample to the smoothness hypothesis that has stood since the 19th century equations of Claude-Louis Navier and George Stokes, which describe how fluids move. The problem was whether those partial differential equations always produce smooth, finite solutions or whether they can blow up to infinity, and Mac Low notes that an infinity would signal the model breaking as a physical description, not a real fluid going infinite.

That last part matters.

If the proof holds, it would mean Navier-Stokes is not universally smooth, and the failure is baked into its own assumptions. Mac Low traces it to the continuum approximation at the heart of Navier-Stokes, where gas is treated as continuous, versus the Boltzmann equation, which treats it as colliding particles obeying Newton. Chapman and Enskog derived Navier-Stokes from Boltzmann only by assuming gradients stay small, and a blow-up is exactly where that linearization fails. The physics already knows this. The math did not have a proof.

What OpenAI produced is not a readable proof. StarTalk notes the output was delivered as a formal verification in Lean, the math-checking language, comprising about 26,000 sub-theorems generated by roughly $6 million worth of GPUs running for 88 hours. Nobody can read that directly and build on it, Mac Low says, and the value for mathematics is in the road others can travel, not an answer that pops out as 42.

That is why two human mathematicians are now gating the story. Tristan Buckmaster of NYU and Levent Alpoge, now at Anthropic, tell StarTalk they have been translating what Mac Low calls AI slop into human readable form, and that they had been pursuing a similar proof with OpenAI tools themselves. OpenAI says it did not train on their inputs, Buckmaster has questioned that handling, and Mac Low puts his own confidence at more likely true than not only if Lean itself is reliable, which is a separate project involving dozens of contributors at MIT and elsewhere.

StarTalk also surfaces the scale behind the announcement. The system was described as thousands of agents working in parallel, a level of brute force that dwarfs the $1 million Millennium prize and bypasses the usual human journey through partial differential equations where offramps often matter more than the final claim. Even Mac Low, who uses AI as a literature exploration tool that still hallucinates authors while finding real papers, says the unpacking is the point. Until another AI can explain the Lean package to humans, or Buckmaster and Alpoge finish a checkable version, the result remains a gated artifact, not a theorem the field can use.