OpenAI withdrew three manuscripts from its AI-generated mathematics collection after a sign error in one paper invalidated a proof argument and a construction used by two related papers.
Complex-number notation on a blackboard. The image is illustrative, not a page from the withdrawn manuscripts.
OpenAI’s Oct. 7 repository update names the affected paper as “Algebraicity of Weil classes on split abelian eightfolds.” The two related manuscripts concern Kuga–Satake correspondences for K3 surfaces and the rational Hodge conjecture for products of K3 surfaces.
The same update lists repairs to 14 other manuscripts, including proof fixes, corrected statements and clarified assumptions about which results they depend on. It also updates citations in 13 more manuscripts so they point to revised companion papers.
OpenAI added six formalizations and five supporting results, bringing its count of formalized top-line results to 300 of 719, or about 42%. A Lean formalization encodes proof steps in a language a computer can check. That check applies only to the encoded proof. The repository says its manuscripts remain at different verification stages, not all have Lean proofs, and some unformalized results could contain problems.
Image: Jacob Rus, “Blackboard bold on a blackboard”, CC BY-SA 4.0, via Wikimedia Commons.
