OpenAI has published a large set of mathematical manuscripts on GitHub. The repository README says the current catalogue contains 722 manuscripts organized into 372 families, produced by “an unreleased internal OpenAI model.” A family, in that README, groups related papers: a principal result, companion arguments, consequences, or alternative proofs. The license file in the repository is the Apache License, Version 2.0.
The counts, the procedure, and the caveats below come from that README.
What the README says was run
The README says the vast majority of results used the same procedure. “On average, each result used three hours of ChatGPT Pro thinking compute with that model.” Over the evaluation, it says, the model “was posed approximately 4,000 problems.” Aggregating the output into families and requiring “an appropriate level of significance” produced the catalogue.
The README names two exceptions to that fixed procedure: work on a zero-free region for the Riemann zeta function, and what it calls a proof of the Hodge conjecture for CM abelian varieties. It also says: “Additionally, the writeup for the Re(s) > 11/12 zero-free region for the Riemann zeta function was human edited for readability.” Ten families have abridged reasoning summaries, listed in the README.
Scientific American reports that an OpenAI spokesperson said the unreleased model produced almost every result from a single prompt handed to a single agent, and that some results might have taken multiple attempts. That account is the spokesperson’s, as Scientific American reports it. The README states the average compute and the number of problems posed. It does not publish the prompts.
Lean, and why checking is the bottleneck
Lean is a proof assistant. A claim is rewritten in a language a computer can check, step by step, so a finished formalization is a machine-checked version of that claim. The README says: “Not all have accompanying Lean formalizations.” It also says: “Many, but not all, of the manuscripts have been formalized.” Then: “Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly.”
That gap is the bottleneck for a reader. A formalized result can be rechecked by anyone who can run the Lean library in the repository. An unformalized manuscript still needs a person who can read the write-up, and the model that produced it is not available to rerun.
372 families, and a headline that says 377
The README’s count is 372 families and 722 manuscripts. Gizmodo’s headline says OpenAI released 377 new math results. On the manuscript map, the family headings run from 001 through 377, and five numbers do not appear: 045, 061, 070, 123, and 163. That is 372 headings. The highest family number on the map is 377. The README’s family count is 372.
So the numbers measure different things: 722 is the manuscript count, 372 is the family count, and 377 is the highest family number on the map.
What mathematicians told reporters
New Scientist reports that Kevin Buzzard of Imperial College London says the release included 30 papers relevant to his field of number theory, that only seven of those seemed impressive, and that only one was formally verified in Lean. The magazine quotes him: “Unfortunately, acceptance of these results by the community will take time, and journalists are going to have to wait while the mathematicians do their job.” He continues: “The six unformalised results will have to wait until either an expert is motivated to read and check the text, or a Lean formalisation is produced.”
In a 7 October comment, Jacob Aron writes that formalization of the release is incomplete, and that papers without it leave the checking to mathematicians. Scientific American quotes MIT mathematician Andrew Sutherland: “Until and unless they release the model and people can replicate their results, I think you should treat any claims about one-shotting problems with a single agent as unverified.” He adds: “We should ask for receipts.”
The Verge describes 722 manuscripts covering 372 result families, and says the advisory group AGMAI described solutions to “hundreds” of open questions. That wording is The Verge’s account of the group.
A day earlier, Thomas Bloom wrote that he would freeze new proof claims on the Erdos problems site. That report follows his guest post on Terence Tao’s blog. The freeze and the dropped solved count are his plan. These manuscripts are a separate release.
What is checkable now
The README says corrections will be recorded as new versions, with older versions kept, and that each manuscript can be cited from the BibTeX block in its directory. It also says the project is “exploring community-hosted repositories for these materials.”
Where a manuscript has a Lean formalization, that formalization is the object a developer can recheck. Where it does not, the README says some unformalized results could have issues. The model, the prompts, and a way to repeat the run are not in the repository.
The Campfire
No commentsNobody has pulled up a log by this one yet. Be the first to say what you make of it.
Held for the desk. It appears after a look.