OpenAI Published 722 Proofs and Withheld the Model's Name

OpenAI published 722 mathematical manuscripts to a GitHub repository on 6 October 2026, grouped into 372 result families and all produced by an unreleased internal model. Seven days earlier, an independent advisory group based at the Institute for Advanced Study had published a list of conditions for releasing exactly this kind of material. The release meets some of those conditions to the letter and misses others the group had singled out.

The repository's README puts the catalogue at 722 manuscripts in 372 families, where a family groups a principal result with companion arguments, consequences or alternative proofs. OpenAI says the model was posed approximately 4,000 problems over the evaluation, and that aggregating the output and "requiring an appropriate level of significance" produced the catalogue. Each result used, on average, three hours of ChatGPT Pro thinking compute. The named families include the irrationality exponent of pi, the symmetric and general Mahler conjectures, Kaplansky's direct-finiteness conjecture in characteristic two and the three-dimensional relativistic Vlasov-Maxwell system.

Where the checklist was met

The Advisory Group on Mathematics and Artificial Intelligence published its recommendations on 29 September 2026, after asking the mathematical community for feedback and receiving more than 600 replies. On formalisation it was unusually specific: proofs should be formalised as far as possible, and the artefacts should carry copyright headers, a challenge file for comparator, and a formalization.yaml. OpenAI's repository contains a lean directory with a formalization.yaml, a formalisation catalogue and a ComparatorChallenges folder of checking instructions. On versioning the group asked for persistent citable identifiers and recorded modifications. OpenAI says it will preserve the release history, record corrections as new versions, keep earlier versions accessible, and ship a BibTeX block with each manuscript.

Ten summaries out of 372 families

Ten is the number to hold onto. The group asked labs to make public, for each result released, the name of the model, the prompts used, a summarised chain of thought, the time taken and the estimated cost of computation. The repository lists reasoning summaries for families 007, 017, 087, 102, 159, 197, 221, 271, 287 and 362. That is ten of 372. The prompts are not published. Neither is the name of the model: OpenAI's announcement calls it "an internal frontier model" and the README calls it "an unreleased internal OpenAI model".

The repository is also OpenAI's own. The group asked that results be deposited in scholarly repositories that "should not be controlled by any AI lab", and github.com/openai/math is controlled by the lab that produced the results. OpenAI acknowledges the gap twice over, saying it is "continuing to explore other community-hosted alternatives for this release which meet the committee's guidelines", while the README repeats that it is "exploring community-hosted repositories for these materials".

On citation and exposition the company concedes the standard is not yet met. The group asked labs to scour the literature and cite the papers where ideas were first introduced even if a model rediscovered them independently, and to rewrite proofs so they are not "full of wordy reasoning and non-standard terminology that renders them virtually incomprehensible". OpenAI's answer is prospective: for future releases, it says, it is committed to improving the quality of the papers through citations, mathematical exposition and presentation.

Who decides where the money goes

The sharpest unresolved point is funding. OpenAI says it will fund "a series of workshops, conferences, and special programs around the understanding of major results produced by AI", with more detail to come. The group asked for that support and attached a condition: the decision about which efforts get funded "should be taken neither by this group nor by AI labs, but by separate, already existing nonprofit institutions that have established processes for distributing funding". OpenAI's announcement names no intermediary. The group also recorded, pointedly, that accepting such support "would not be conferring legitimacy on the practices of the AI labs".

As Parallax Nexus has reported, mathematicians had already objected to how AI labs announce proofs, at a point when OpenAI had claimed more than 100 resolved open problems and published none of them. The survey behind these recommendations asked respondents about that exact situation, one in which OpenAI "announced the existence of many results without giving details". This release is the answer to that complaint.

What is not established

No part of the collection has been independently verified, and OpenAI does not claim otherwise. The README says the collection "includes results at different stages of verification", that "not all have accompanying Lean formalizations", and that "some of the unformalized results could have issues". The 4,000 figure yields no success rate, because problems posed, manuscripts and families are three different units, and OpenAI publishes neither a problem-by-problem outcome table nor the account the group requested of how many comparably hard problems the model failed and how the problems were chosen. Two results departed from the standard procedure, and the write-up of the zero-free region for the Riemann zeta function above real part 11/12 was, by the README's own admission, edited by a human for readability.

The honest reading is that OpenAI has satisfied the machine-checkable half of the recommendations and deferred the human half. A formalization.yaml and a comparator challenge file are cheap to generate and easy to audit. Literature citation, readable exposition, a named model, published prompts and an arm's-length funding body are none of those things, and every one of them is either promised for later or simply absent. The counter-argument deserves weight: turning recommendations into a structurally compliant release in seven days is fast by the standards of any research institution, and the group's opening request, that labs stop running advanced mathematics on proprietary models at all, was never going to be granted by a company whose stated plan is to ship the model instead.

The test that matters now sits outside the repository. It is whether a mathematician with no connection to OpenAI can read family 017, the irrationality exponent of pi, and explain in their own words why it holds. The group's central claim is that until somebody can do that, the result is not yet part of mathematics.