A week before OpenAI published 722 machine-generated mathematics manuscripts, an independent advisory group published five specific technical conditions for doing exactly that. OpenAI’s announcement cites those recommendations by link. So this release can be graded rather than argued about, and what the grading turns up is not that it falls short in places, but which shortfalls OpenAI names itself and which one it does not.

The checklist comes from the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, whose recommendations are dated 29 September 2026 and drawn from “over 600 replies” to a community survey. The release went up on 6 October. Both documents are public; what follows is each recommendation against what is in the repository.

Recommendation 1: readable papers with proper attribution

The group asks that labs scour the literature and cite prior ideas, and that proofs be rewritten in the conventions of a traditional paper, not “full of wordy reasoning and non-standard terminology that renders them virtually incomprehensible.”

OpenAI concedes this one in its own announcement: “For future releases, we are committed to further improving the quality of the papers via the citations, mathematical exposition, and presentation of the results for better understanding.” That sentence is a promise about the next release, which makes it a statement about this one. I did not read the 722 manuscripts, so I cannot grade the prose myself; what I am reporting is OpenAI’s own assessment of it.

Recommendation 2: a repository nobody’s lab controls

The wording is unambiguous. Results “should be deposited in a timely manner in appropriate scholarly repositories. These should not be controlled by any AI lab,” and must guarantee “a persistent citable identifier.”

The release is at openai/math, which OpenAI controls. The announcement does not dodge it: “We’re continuing to explore other community-hosted alternatives for this release which meet the committee’s guidelines.” The repository’s README repeats the point. The repo was created on 6 October at 21:47 UTC under Apache-2.0, per GitHub’s API. Citation is handled by per-manuscript BibTeX blocks and a stated promise to preserve release history, which is not the same as a persistent identifier issued by a repository the publisher cannot rewrite.

Unmet, and conceded.

Recommendation 3: name the model, the prompts, the compute

Here the record splits. Time and cost are disclosed: “The average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking.” The chain of thought is partially disclosed, as the README lists exactly ten reasoning summaries against 372 result families. The model name is not disclosed at all: the announcement calls it “an internal frontier model,” the README “an unreleased internal OpenAI model.” The prompts are not published.

Two of five sub-items met, on my count.

Recommendation 4: formalize it, and state the status

This is where the artifacts are richest and the headline is softest. The recommendation asks for formalization “as far as possible,” with artifacts meeting community standards including “a challenge file for comparator, and a formalization.yaml.”

Both exist. lean/formalization.yaml is there, written against the schema published by the mathlib initiative, and the comparator challenge files are there too, one JSON per result naming the theorem and its permitted axioms. On technical form, this recommendation is met properly.

Coverage is where the announcement’s wording does work. It says OpenAI is “sharing formalizations of many of the proofs in Lean.” Counting the YAML’s source list against the repository’s manuscript map: 162 of the 721 linked manuscripts have a formalized main result, or 22.5%, covering 127 of the 372 families, or 34.1%. Those are my counts, not published figures. “Many” is defensible for 162 papers in absolute terms. It is also a minority of the collection, which the announcement does not say and the README does: “This collection includes results at different stages of verification. Not all have accompanying Lean formalizations.” The README goes further than the announcement in the reader’s favour, which is worth stating plainly: “Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly.”

The gap nobody disclosed

The same recommendation says that where formalization lags, “the formalization status of the paper should be clearly stated.” The status is stated, and it is weaker than it looks.

Inside formalization.yaml, two fields describe the collection’s own verification standing. Its scope reads Partial progress. Its review status reads unchecked.

Compare OpenAI’s previous formalization release, openai/ten-proofs, from the August “Ten Advances in Mathematics” work. Same schema, same filename. That one declares review: status: agent-reviewed, a sorry_count of 0 and sorry_in_definitions of 0, lists twelve named main results each with its own declared axioms, and records both the model and the wall-clock time in its automation block. The new file declares no sorry_count at any level, names no model, and lists 185 theorem declarations with no per-result verification metadata at all.

So the larger release carries less machine-readable assurance than the smaller one, in the same field of the same file format. That is not a contradiction, and the honest reading is that unchecked is the accurate label for a collection assembled from roughly 4,000 attempted problems in weeks rather than twelve results over one. But it is the single gap here that appears in neither the announcement nor the README, and it sits in the one field a machine would read to decide whether to trust the proofs.

Recommendation 5: say how much failed

The last recommendation is the one most labs would want to skip: publish “how many other problems of comparable difficulty the models tried and failed to solve, as well as how the problems were chosen.”

The README answers it in two sentences. “Over the course of the evaluation, the model was posed approximately 4,000 problems. Aggregating the output into result families and manuscripts and requiring an appropriate level of significance led to the catalog outlined above.” That is 372 families from about 4,000 attempts, stated by the party with the least incentive to state it. The selection criterion, “an appropriate level of significance,” is vague enough to hide a great deal. The denominator is not.

Met, and met in the document fewer people will open.

What the people on the other side of it said

The advisory group’s own framing is sharper than any of this grading. Its opening paragraph says of testing problems on proprietary models: “we do not endorse this practice, and we ask them to stop.” It asks labs to “refrain from treating the release of mathematical results as marketing vehicles to promote their models.”

The same day the release went up, the maintainer of erdosproblems.com announced he was closing the site’s proof-claim comments, writing that its main public use had become “to advertise their AI-generated proofs, often without any attempt to explain them,” recorded “as a way to record a (increasingly meaningless) priority claim.” His line for why a problem site should not also be a proof dump: “Just as one does not open a restaurant in an abattoir.” Not everyone agrees. The top comment on that post calls the change “very disappointing” and argues it only makes mathematical progress less visible.

That is the environment this release landed in, and it is why five mechanical recommendations exist at all. Graded against them, OpenAI met one cleanly, met one in form while its volume claim leans on a soft word, partly met one, and failed one by its own admission. The part of the checklist it satisfied best is the one about failure rates. The part nobody checked is the field that says unchecked.