OpenAI Retracts Three Math Papers After a Single Sign Error Undermined Two More Proofs

OpenAI withdrew three papers from its public repository of AI-generated mathematics research on October 7 (local time), one day after releasing a batch of mathematical results along with verification material for some of the proofs. The company said a sign error in one paper invalidated its central argument, and that two other papers that relied on that argument were affected as well.

How one sign error spread to three papers

The flawed paper was titled “Algebraicity of Weil classes on split abelian eightfolds.” According to OpenAI, two other papers dealing with K3 surfaces borrowed the argument and constructions from it. When the underlying argument collapsed, the proofs built on top of it were withdrawn too. For each retracted paper, the repository now carries an explanation of the error along with a link to the earlier manuscript.

The corrections went beyond those three papers. OpenAI logged fixes to proofs, write-ups, and citations in 14 other papers, and updated citation information in 13 related papers.

How many proofs have been machine-checked?

OpenAI said it had added six new Lean formalizations. Formalizing a proof in Lean means rewriting it in a form a computer can check logically, step by step. After that additional work, 300 of the 719 main results had passed this kind of check. That is roughly four in ten, about 42 percent.

OpenAI acknowledged that results that have not been formalized may contain problems. When it published the research on October 6, the company said it planned to expand formalization further.

Can readers in Korea see the research?

Readers in Korea can view the papers and some of the proof material in the public GitHub repository. Alongside the manuscripts, the repository shows whether a result has been formalized, explanations of errors, and a record of revisions. Most of these results were produced by an internal model that has not yet been released. OpenAI said it gave the model roughly 4,000 research problems and collected the output. There are currently 719 manuscripts published, which group into 372 families of related work.

OpenAI estimated that the compute spent on producing a single result was equivalent, on average, to about three hours of thinking by ChatGPT Pro.

The retractions illustrate why any assessment of AI-generated mathematics has to look at proof verification and the dependencies between papers at the same time: an error in a single argument dragged down other results that leaned on it. What to watch next is how far OpenAI gets with the additional formalization it has promised, and what further corrections show up in the repository.