Yesterday, OpenAI released 722 AI mathematics manuscripts in one go, and just now it withdrew 3 of them.
The reason is simple: a plus-minus sign was written incorrectly.
Just now, OpenAI published its first update log in the openai/math repository. The log shows that OpenAI withdrew 3 manuscripts, revised 14, and updated citations for another 13. The total number of manuscripts in the repository dropped from 722 to 719.
One plus-minus sign brings down three papers
The three withdrawn papers are all related to the Hodge conjecture, one of the Millennium Prize Problems:
Algebraicity of Weil classes on split abelian eightfolds
Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
The rational Hodge conjecture for products of K3 surfaces
The problem lies in the first paper. In the withdrawal note, OpenAI wrote that in a key argument, the paper recorded the sign of a certain geometric operation as +1, whereas according to the paper's own convention, it should be -1.
https://github.com/openai/math/blob/main/history.md
A plus versus a minus makes a world of difference. A count that should have canceled out and ultimately been zero became a nonzero number. A classical theorem on which the paper relies has as its precondition precisely that this count must be zero. With the precondition failing, the entire subsequent construction loses its support.
The other two papers both borrowed this construction, so they were withdrawn as well.
However, in all three withdrawal notes, OpenAI emphasized the same sentence: what is withdrawn is the proof, which does not mean that these mathematical propositions themselves are wrong. The original manuscripts were also not deleted and can still be viewed through archived links.
These three papers all belong to the repository's result family No. 032, that is, the previously most closely watched results related to the Hodge conjecture.
After the withdrawal, the name of this family also changed: from "Hodge and Kuga–Satake results for all projective K3 surfaces" to "the rational Hodge conjecture for CM abelian varieties".
In other words, the part of the conclusions concerning K3 surfaces has been removed from the list. The core conclusion of this family, namely proving the rational Hodge conjecture for all complex CM abelian varieties, is still retained, and the new version of that paper only updated citations.
It is worth mentioning that the paper with the error is dated September 18, making it one of the earliest batch of manuscripts in the repository. From its date to its public release was nearly three weeks, and it was withdrawn within one or two days after publication. As for who discovered the error, OpenAI did not say.
Another 14 papers were revised
In addition to the withdrawals, OpenAI also revised 14 manuscripts, including patching proofs, correcting statements of conclusions, and clarifying preconditions and dependencies.
These 14 involve Lipschitz heights and the Ashkin–Teller model in statistical physics (4 papers), the Kähler minimal model program and abundance in complex geometry (6 papers), symplectic geometry (2 papers), general computation for Navier-Stokes fluids (1 paper), and one BSD formula paper from which outdated citations were removed.
One revision is quite representative. Result family No. 342 claimed to prove the "tame pushforward compatibility" conjecture proposed by Simon Donaldson. The main conclusion did not change, and there is a Lean formalization. But a stronger incidental conclusion in the paper was found to be overstated: the revised version narrows it to a specific case and also adds an example showing that it does not hold in general.
Formalization rate: 42%
The update also added 6 Lean formalizations and 5 supplementary auxiliary results. According to OpenAI's accounting, the main results of 300 manuscripts have now been formalized, accounting for about 42% of all 719.
Among the newly added formalizations, several carry considerable weight, such as the 103rd achievement family in theoretical computer science claiming to prove that logarithmic space computation can be fully derandomized (L = RL = BPL).
It should be noted that the "about sixty percent" we previously reported was counted by achievement family, meaning that as long as one paper in a family comes with a formalization, it is counted; the 42% announced by OpenAI is counted by individual main results, which better reflects the actual proportion that has been checked line by line by a computer.
Where errors occur, there is no Lean oversight
Comparing with the repository directory reveals a pattern: the content that was retracted and substantially revised this time almost all falls in the parts without Lean formalization.
This also confirms the earlier reminder from the mathematics community: results that have not undergone formalization and peer review can currently only be regarded as "claims".
Fortunately, this erratum was handled fairly properly: the errors were clearly stated, the dependency chain was explained, and the old version was kept available for reference, in line with the "modification with a trace" principle recommended by the Institute for Advanced Study's Mathematics and Artificial Intelligence Advisory Group.
However, just two days after more than 700 manuscripts were made public, the first erratum arrived. It most likely will not be the last.
This article comes from the WeChat public account "Machine Heart" (ID: almosthuman2014), editor: Panda
