← All posts
This post is written in English.
On 6 October, OpenAI posted 722 maths manuscripts to a public GitHub repository, grouped into 372 families of results. The Next Web reports they came from an internal model that hasn't been released, tested on about 4,000 problems at an average of about three hours of compute per result.
Nearly every paper came from a single prompt to a single agent, according to OpenAI's comments to Scientific American.
Why people are cautious
- Verification is partial. Many proofs have Lean versions, but not all, and OpenAI says some without formal versions could have issues.
- It can't be reproduced. MIT's Andrew Sutherland said the single-agent claims should be treated as unverified until others can run the model.
- Experts have doubts. NYU's Tristan Buckmaster, who works on Navier-Stokes, said: "I don't think they've done their sort of due diligence at all."
- Access is a concern. The advisory group AGMAI warned that using proprietary models for maths "risks creating a two-tier system", and said its advice wasn't an endorsement.
OpenAI's research lead responded that testing internal models helps build better tools, and that the proofs were a byproduct.
A later O'Reilly roundup says three papers have since been withdrawn and some proofs are disputed. I haven't checked those withdrawals myself.
My read
There are two separate questions: are the proofs correct, and do they mean what OpenAI implies? Lean can help with the first, for the proofs that have it, though someone still has to confirm the statement says what it claims. The second takes years of mathematicians reading and using the results. I wouldn't dismiss 722 papers, and I wouldn't count them as 722 results yet. If the withdrawals are the only corrections after a real review, that would be a remarkable outcome.
