OpenAI’s repository history records that on Oct. 7 it withdrew three math manuscripts after a sign error invalidated an argument and a construction used by two dependent papers. The withdrawals followed the company’s Oct. 6 release of mathematical results produced by an internal frontier model.
OpenAI withdrew three manuscripts after an error
The sign error invalidated a stabilization-trace cancellation argument and a construction used by two papers that depended on it. OpenAI’s Oct. 7 history also records fixes to 14 other manuscripts and reference updates to 13 additional manuscripts.
The release began the day before, when OpenAI announced the results and made manuscripts and supporting proof artifacts public. OpenAI says its evaluation posed approximately 4,000 open problems. It estimates that an average result used compute equivalent to roughly three hours of ChatGPT Pro thinking.
What the OpenAI math repository currently contains
The current repository lists 719 manuscripts in 372 families. Those are different counts: a family groups related papers, which may include a main result, supporting arguments, consequences or alternative proofs.
What Lean formalization means
Lean is a proof assistant that lets a computer check a formalized proof. OpenAI reports that 300 of 719 top-line results—about 42%—have Lean formalizations. That figure does not mean all 719 results have been formally checked.
The repository’s account of verification
OpenAI says the results are at different verification stages. Not all have Lean formalizations, and the repository cautions that unformalized results may have issues. A formalization gives a computer-checkable proof; it does not, by itself, establish a result’s mathematical significance or make it easier for people to understand.
