OpenAI has published 722 mathematics manuscripts generated by an unreleased internal model, covering roughly 20 subfields from number theory to partial differential equations, SiliconANGLE reported Wednesday. Many of the papers come with Lean files that let a computer check the proofs, though not all of them do yet.

What Happened

The papers were posted to a GitHub repository late Tuesday. SiliconANGLE's report does not name the model that produced them, and OpenAI has not said when or whether it will be released.

The most prominent claim concerns the Riemann hypothesis, the more than 150-year-old conjecture about the distribution of prime numbers. The model did not prove the hypothesis. According to the report, it proved what is called the quasi-Riemann hypothesis, which SiliconANGLE described as an important piece of the larger problem.

RelatedOpenAI Says Its Models Broke Into Two Outside Data Sites and Left It Out of Their Answers

More than 80 of the papers deal with theoretical computer science. Three of them address matrix multiplication, the operation at the core of how AI models process data, and how fast it can theoretically be performed; the model produced a clearer definition of that limit, according to the report. A separate paper describes a new algorithm for multiplying integers.

More than a dozen proofs concern partial differential equations. They include a proof of a version of De Giorgi's conjecture, which relates to equations used to describe metal alloys, and clarifications of questions tied to the Navier-Stokes equations, which govern fluid flow. SiliconANGLE noted that OpenAI's model had tackled a different Navier-Stokes-related problem in September.

Why It Matters

The size of the release changes the verification problem. A single claimed breakthrough can be checked by a handful of specialists over months; 722 papers across 20 fields cannot be reviewed that way. That is why the Lean files matter. Lean is a proof assistant in which a proof is written as code, and if the code compiles against the stated theorem, the logic has been checked by machine rather than by a referee.

The catch is that only part of the collection is formalized. For papers without Lean files, the claims stand on the same footing as any unrefereed preprint, and a formal proof only confirms the theorem as it was encoded, so experts still need to confirm that the formal statement matches the result being claimed.

OpenAI said it will release Lean proofs for more of the papers and will finance research events and programs where mathematicians review the AI-generated results, according to SiliconANGLE.

Context

AI developers have spent the past two years trying to show their systems can do original mathematics rather than solve textbook or competition problems with known answers. Formal verification has become the main way to make such claims credible, because it removes the need to trust either the model or the company publishing its output.

Results on matrix and integer multiplication carry practical weight beyond pure math. Faster multiplication algorithms, even theoretical ones, feed into work on the cost of the linear algebra that dominates AI training and inference.

What to Watch

The first test is how specialists in each field respond, starting with the quasi-Riemann proof, which is likely to draw the most scrutiny. Additional Lean formalizations will show how much of the collection holds up under machine checking. The review events OpenAI plans to fund will indicate whether the math community treats the release as a source of new results or as a backlog of claims to be vetted.