Overview
- OpenAI published a GitHub repository on Tuesday containing 722 AI-generated manuscripts organized into 372 result families that the company says come from an internal, unreleased model.
- The release includes machine-checkable Lean formalizations for only a subset of results and ten condensed reasoning summaries, with OpenAI’s repository listing about 162 main results as formalized and reporting average compute near three hours of ChatGPT Pro–equivalent time per result.
- Mathematicians and groups including the Association for Human Mathematics and many Fields Medal winners sharply criticized the mass posting for using a proprietary model, urging caution about credit, ethical norms, and the practice of testing frontier problems on closed systems.
- Experts note limits to verification because a Lean check confirms logical steps but not that the formal statement matches the classical problem, the model and prompts remain undisclosed, and the repository has already seen a small number of retractions or corrections.
- Independent human review, formal checking, and community triage are now under way and are expected to take months to determine which claims are correct, which are novel, and how AI outputs should be integrated into peer review, prize adjudication, and researchers’ careers.