OpenAI released hundreds of mathematical results this week, drawing warnings from mathematicians who told The Verge that understanding the work could take years.
The scale of the release, which researchers described as "pure insanity," has overwhelmed the field and raised concerns about how academia will verify and absorb such a rapid arrival of machine-generated proofs. OpenAI announced the release on its website, stating that it was sharing "a broad range of new mathematical results produced by an internal frontier model." OpenAI The results appear in a GitHub repository containing 719 manuscripts across 372 families, along with supporting proof artifacts in Lean, a programming language that allows computers to check proofs.
The repository's current catalogue spans multiple mathematical disciplines, with each family grouping related papers that may include principal results, companion arguments or alternative proofs. About 42% of the top-line results have been formalized in Lean, according to the repository's description. OpenAI said it will continue adding Lean formalizations as they are obtained. On average, each result required the equivalent of three hours of ChatGPT Pro thinking compute, using an unreleased internal OpenAI model that was posed approximately 4,000 problems during the evaluation. The company published 10 summaries of the model's reasoning for selected results, covering topics such as the irrationality exponent of π, the Mézard–Parisi formula for diluted spin glasses, and the three-dimensional relativistic Vlasov–Maxwell system.
The Verge spoke with more than three dozen mathematicians and reported that their reactions included "Staggering," "Overwhelming," "Surreal," and "Pure insanity." Beyond the awe, the article described "a deep-seated anxiety over what it all means—and what comes next," along with a consensus that understanding what OpenAI had released could take years, let alone determining where human mathematicians fit in the field. The low share of Lean-formalized results compounds the challenge. Without machine-checked proofs for most manuscripts, the community must rely on traditional peer review at a time when the volume of generated output far outstrips the available reviewer pool.
Commenting separately on the release, cognitive scientist Gary Marcus noted that the model's architecture combines large language models with symbolic AI—a neurosymbolic approach he has long advocated. Gary Marcus However, he added that "it still doesn't mean they have AGI; the math stuff AFAIK does not generalize broadly, because you can't use the same symbolic verification … in the open-ended real world." OpenAI said it will fund a series of workshops, conferences and special programs to help the community study the models' major results, and it is exploring community-hosted repositories for future releases.