OpenAI has withdrawn three mathematical research manuscripts from its GitHub mathematics repository, according to an update posted by Dan Roberts. The withdrawn papers are:
- 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 withdrawals were announced as part of a broader update to OpenAI’s math repository. According to Roberts, the update included 6 new Lean formalizations—mathematical proofs written in the Lean proof assistant language—along with 19 modifications to existing entries. Lean formalizations represent a high standard of mathematical rigor, as they involve translating mathematical results into code that can be verified by a computer.
Following these updates, the repository now contains approximately 42% of its top-line results in formalized form. Roberts indicated that OpenAI intends to continue updating the repository with new formalizations and to address any errata discovered in existing work.
The three withdrawn manuscripts all relate to algebraic geometry, a field concerned with geometric properties of solutions to polynomial equations. Specifically, they address topics in the theory of algebraic varieties and conjectures about their structure. The decision to withdraw these papers suggests that upon formal verification or further review, issues were identified that warranted removal from the repository.
OpenAI’s mathematics repository represents an effort to formalize mathematical results using automated proof systems, which can help ensure the correctness of complex mathematical claims. The repository combines newly formalized results with corrections and withdrawals as errors or issues are discovered during the formalization process.
Key facts
- OpenAI withdrew three mathematical manuscripts from its GitHub math repository
- The withdrawn papers address topics in algebraic geometry and K3 surface theory
- The repository update included 6 new Lean formalizations and 19 modifications
- Approximately 42% of the repository’s top-line results are now formalized
- OpenAI plans to continue updating the repository with new formalizations and errata corrections