Mathematicians dispute OpenAI's account of how its proposed Navier-Stokes proof works

In early September, OpenAI presented a 166-page proposed solution to the Navier-Stokes problem, written in the formal verification language Lean. The company said the proof followed the approach of Spanish mathematicians Diego Córdoba and Luis Martínez-Zoroa. Several groups of experts now disagree, Scientific American reports. "When you go to the details, it is a different approach," said Gonzalo Cao-Labora of EPFL, who described the similarities as only surface-level. Lean checks every logical step, but that does not on its own make the argument readable to humans. The Clay Mathematics Institute has been reviewing the proof since its release. Before publication, NYU mathematician Tristan Buckmaster accused OpenAI of building on work he had done with Anthropic's Levent Alpöge using publicly available models. OpenAI denied this and said it never used Buckmaster's data. Camillo De Lellis of the Institute for Advanced Study said a definitive answer is probably impossible because language models are black boxes. In early October, OpenAI also released roughly 400 more results as a loose collection on GitHub. Many mathematicians were angered by the format, and the community can barely keep up with the volume. The dispute shows a growing gap between producing machine-checked proofs and explaining them in a way mathematicians can assess and credit.