OpenA has announced a set of new mathematical results produced by an internal frontier model. The results were published in a GitHub repository, with Lean formalisations of some of the proofs.
OpenAI also released ten summaries of the model’s reasoning and an estimate of the compute used. According to the company, the average result required roughly the equivalent of three hours of ChatGPT Pro thinking.
The model has not been released publicly. Science.org reports that it attempted about 4,000 problems to arrive at the 372 results.
OpenAI says it consulted the independent Advisory Group on Mathematics and AI at the Institute for Advanced Study on how to share the work. Engadget reports that the guidelines covered prompt release through traditional academic channels and disclosure of the model used, the prompts and the compute costs.
In September, OpenAI said its models had resolved more than 100 long-standing open problems.
Why The Reported Numbers Differ
Reports use several figures, and each means something different.
- 722: the number of manuscripts uploaded on 6 October.
- 719: the number remaining after OpenAI withdrew three. Science.org reports that the company has also revised 14.
- 372: the number of result families. Decrypt explains that a family can include a main theorem alongside companion arguments, consequences or alternative proofs, so 722 is a count of manuscripts rather than solved problems.
The number of Lean-formalised results has also changed. Decrypt reported 162 manuscripts with a Lean-formalised main result at the time of release.
Science.org reports that 300 of the 719 remaining papers have now been formalised. OpenAI has said it will add formalisations as they are completed.
The figure of 372 is therefore OpenAI’s own claim. It has not been independently verified, and at least three of the manuscripts have already been withdrawn.
What Lean Formalisation Establishes
Lean is a programming language that allows a computer to check each logical step of a proof. A successful check is a strong form of evidence, but it applies to a specific thing.
An independent audit of OpenAI’s earlier proofs describes the limit. A passing check establishes the encoded statement relative to the kernel, the definitions, the imported results and the axioms. It does not by itself confirm that the encoded statement matches the mathematics in the paper.
A preprint found that the Lean formalisation of OpenAI’s Navier-Stokes result does not match the proof described in the accompanying paper. Researchers told Science.org this does not mean the result is wrong, but that computer verification may not carry the weight often attributed to it.
Coverage also remains incomplete. On Science.org’s figures, roughly 419 of the 719 remaining papers have no Lean formalisation. OpenAI itself says that some unformalised results could contain issues, according to Decrypt.
What Is The Quasi-Riemann Hypothesis?
The quasi-Riemann hypothesis is one of the most searched results in the release.
The Riemann hypothesis states that the non-trivial zeros of the zeta function lie on the line where the real part equals 1/2. It remains unproved. The quasi-Riemann hypothesis is a weaker statement. It asks whether there is a fixed number below 1 beyond which the zeta function has no zeros.
Nature reports that none of the 722 manuscripts claimed a solution to any of the five remaining Millennium Prize Problems.
A separate preprint has since been built on OpenAI’s argument. A follow-up preprint is not the same as independent refereeing, and the result has not been confirmed through that process.
The Verification Bottleneck
Reaction from mathematicians has been divided. Nature reports that Ursula Martin of the University of Oxford described the release as an unfinished draft that the community is expected to review.
The Conversation collects a range of responses, from strong praise to sharp criticism of how the material was released.
Several concerns recur. The volume is large, the formal verification is partial, and no established process exists for assessing hundreds of manuscripts released together.
One recent paper on proof checking argues that making checking cheaper does not reduce the verification burden attached to a body of knowledge. Generating results can become fast without making review any faster.
For organisations using AI to produce code, analysis or research, the same questions apply:
- Who is responsible for reviewing output produced at machine scale?
- Does an automated check confirm the right thing?
- How should credit and provenance be recorded when a model produced the work?
- What happens when generation outpaces review?
The release shows how quickly AI systems can now produce research.It also shows how much slower independent confirmation is.
Organisations that generate more than they can verify will need a review process designed for that volume.
Comments ( 0 )