OpenAI published 722 math manuscripts from an internal model on GitHub

A frontier model wrote proofs about the Navier-Stokes equations, and the proofs are in Lean so another computer can check them. OpenAI published 722 mathematical manuscripts on GitHub at openai/math, grouped into 372 related result families, and released a second repository, openai/NavierStokesAndEuler, with Lean 4 certificates for two of the headline results.

The release covers results in number theory, combinatorics, algebra and operator theory, mathematical physics, and computational complexity, according to the openai/math README. The company says the manuscripts came from evaluating an unreleased internal model on about 4,000 posed problems, and that the average cost per result was roughly three hours of ChatGPT Pro thinking time.

What the Navier-Stokes repository actually proves

The openai/NavierStokesAndEuler repository holds machine-checkable Lean 4 proofs for two results. On Navier-Stokes, the proof shows that for every positive viscosity, smooth solutions with bounded kinetic energy need not exist globally, both on all of three-dimensional space and on a periodic torus. On Euler, the proof constructs smooth, compactly supported initial velocities that develop singularities in finite time. OpenAI frames these as alternatives (C) and (D) to the Clay Mathematics Institute's Navier-Stokes Millennium Prize statement.

A blowup theorem is not the same as answering the Clay problem, which asks whether smooth solutions exist for all time. The repository is specific about which alternative it addresses, and it includes a Comparator tool other mathematicians can run against the Lean files.

Caveats OpenAI and others stated

Many manuscripts carry Lean formalizations, the README says, and many do not. The repository is described as an ongoing collection with materials "at different stages of verification," which means some results are formal, some are reasoning summaries, and some are pending human review. OpenAI consulted the Institute for Advanced Study's Advisory Group on Mathematics and AI about publication.

Reactions reported by Latent Space include a quote from Levent Alpoge of Anthropic calling it the most significant moment in mathematical history, and a note from OpenAI researcher Will Depue that he expects some results to contain errors. Francois Chollet, cited in the same post, asked whether the gains will carry over to domains where results are harder to verify.

If you build or evaluate AI models on reasoning tasks, there is now a corpus of 722 dated, versioned artifacts to work with, each tied to a specific result family and a method statement, and a smaller Lean-formalized set that another computer can check. The caveats are stated at the source, which is how the honest version of this story reads.

Source

Primary: openai/math and openai/NavierStokesAndEuler, OpenAI on GitHub. Reactions: Latent Space.