OpenAI withdraws 3 math papers after a sign error, revises 14 more
- OpenAI withdrew three manuscripts after a sign error in "Algebraicity of Weil classes on split abelian eightfolds" invalidated a stabilization-trace cancellation argument and the construction two dependent papers used.
- The retracted trio is Algebraicity of Weil classes on split abelian eightfolds, Algebraicity of Kuga-Satake Correspondences for K3 Surfaces, and The rational Hodge conjecture for products of K3 surfaces; each now carries a notice explaining the gap and linking to the archived manuscript.
- 14 other manuscripts were revised with proof repairs, corrected statements, and clarified hypotheses, including four on Lipschitz heights and Ashkin-Teller currents and six on Kähler minimal model programs and abundance.
- 13 additional manuscripts were updated to cite the revised editions of companion papers, changing references and version dates, and one obsolete citation was removed from the exact Birch-Swinnerton-Dyer paper.
- Six more formalizations and five other supporting additions bring the total of top-line results formalized to 300 of 719, about 42%.
Hacker News opinions
so much for the "it's Lean verified" defense, huh
the withdrawn papers weren't Lean verified and never claimed to be. can you point to where anyone actually made that defense?
proof by authority works right up until human mathematicians actually run the code. back to prompt engineering.
without a real mathematical community pointing these things out it would have stayed broken. and like Tao said, automated math puts that community at risk.
has anyone got a link to who caught it? looks like they found the problems while going through the formal proofs, not from a review.
3 mistakes so far out of ~400 is still a pretty good hit rate.
can the others even be disproven if they're so messy that no human can follow them? the onus should be on OpenAI to prove they're right, not on hundreds of mathematicians wading through slop.
honestly I'm glad they withdrew them. claim, test, refute, withdraw is the core loop of science, and we should keep improving these tools so they're as easy as possible to review.
I'm conflicted. we'll see what the final total looks like once an enormous amount of human effort goes into verifying AI outputs. a little sad if that's the future of math.