Executive Summary

On the night of October 6, 2026, OpenAI opened a GitHub repository called openai/math. Inside were 722 mathematical manuscripts written by an unreleased internal model. One manuscript is not one result; several can make up a single result, so the repository counts those groupings separately and puts the number at 372 families. The README says the model was posed approximately 4,000 problems and that, on average, each result used three hours of ChatGPT Pro thinking compute. What dropped out between 4,000 and 722, and by what criteria, is not written down. What the repository does state is that the output was aggregated into result families and manuscripts and filtered by requiring an appropriate level of significance.

The same passage records exceptions. The README says the vast majority of results came out of the same procedure, then names two pieces of work that did not follow it: work on a zero-free region for the Riemann zeta function, and the proof of the Hodge conjecture for CM abelian varieties. It adds that within the former, the writeup covering the region with real part above 11/12 was human edited for readability. These three sentences are identical in the release-day edition and the current one. What does not exist is any per-manuscript record of which manuscript came out of which procedure. The README inside each manuscript directory (every one this article opened had the same shape) holds a title, an author, a date and a BibTeX block for citation. Revised manuscripts get a version note in that spot; withdrawn ones get a withdrawal notice. And the proof named as the second exception heads family 032, which closes this section.

This article was written by downloading the repository at the release-day commit and at the current commit and counting the lists inside the files directly. So it starts with what happened over those three days, in order. Every rate that follows was made inside them.

1.1One event, three dates

Coverage mostly framed this as a withdrawal within a day. Open the primary documents and that one day splits into three. The withdrawal notices say in their own text that the papers were withdrawn on October 6; the repository's history file files the work under an October 7 heading; and the commit that actually put the change into git is dated early on October 8. Rather than any one of them being false, each document is recording a different moment. So instead of reducing them to one date, this article lays all three side by side.

Both commit timestamps were queried directly through the GitHub API. The withdrawal date the notices give is the same day as the release, and the change reached git two days later.

▲ The same four points as the table above, laid out on a time axis. The bracket marks the gap between the date the notices give for the withdrawal and the moment that change actually landed in git.

1.2What changed: three removed, twenty-seven revised

The history file records three kinds of work. Three manuscripts were withdrawn, fourteen were revised and reissued as new editions, and thirteen more had only their references touched so that they cite the revised editions. Add the last two together and twenty-seven manuscripts were given a new edition. Matching the two editions of the contents file directory by directory, this article counted twenty-seven as well. That number returns in §5.

The fourteen revised manuscripts are not scattered across the repository. The history file groups them by subject. Four sit in Lipschitz heights and Ashkin–Teller currents, six in Kähler minimal model programs and abundance, two in taming and hypersymplectic deformation, and the remaining two stand alone. The first three groups alone come to twelve, so the revisions clustered in three subjects. One of the remaining two is not even a proof repair: it removes an obsolete introductory citation that pointed to a supporting manuscript no longer there. The listed changes are proof repairs, corrected statements, and hypotheses and dependencies set out more clearly.

The manuscript count fell from 722 to 719 while the family count stayed at 372. The three that went had all been inside one family.

1.3One sign brought down three papers

All three withdrawal notices point at the same root. A September 18 manuscript inside family 032 had a sign assigned wrongly in one place, and two other papers in the same family had borrowed that construction. All three sat inside family 032, which held eight manuscripts at release. It holds five now. The notice puts the faulty sign like this. The proof assigned each reverse stabilization trace a sign of +1 and concluded that the signed count comes to zero; because the two branches of the standard cusp carry opposite source orientations, each reverse trace takes a sign of −1 in this convention.

The proof assigns each reverse stabilization trace sign +1 … Accounting for the opposite source orientations of the two branches of the standard cusp gives sign −1 for each reverse trace in this convention. Source: withdrawal notice, "Algebraicity of Weil classes on split abelian eightfolds"

Correct the sign and the quantity that was supposed to sum to zero no longer does. The notice gives the resulting count as −2m, with m greater than zero. If that value is not zero, the hypothesis of the cancellation theorem the proof was leaning on is not met. No deeper mathematics is needed here. One sign flipped in one paper, and the two papers resting on it came down with it.

The notices carry one more sentence. All three close with it, word for word.

This withdrawal concerns the proof; it does not assert that the mathematical statement is false. Source: all three withdrawal notices, openai/math

That is exactly right, and this article holds the same line. A proof collapsing and a statement being false are different things. In mathematics a statement in the former condition goes back to being a conjecture. The notices also wrote the repository commit hash into the archive link that points at the pre-withdrawal manuscript. Because it is a hash and not a path, the PDF as of that moment opens at the same address no matter what happens to the files afterwards. This article counts a good many empty fields later on; this one is among the fields filled well.

1.4With three papers gone, the family's headline claim narrowed

The surface figure of three withdrawn papers hides something. In the contents file, the title of family 032 changed. At release that line read "Hodge and Kuga–Satake results for all projective K3 surfaces"; now it reads "The rational Hodge conjecture for CM abelian varieties". A sentence that took all projective K3 surfaces as its subject disappeared entirely, and a sentence about a narrower subject took its place.

Compare the summary under that title across the two editions and you can see which sentence went. The release-day summary ran to three sentences, and the first of them already had CM abelian varieties as its subject. The K3 surfaces were carried by the last sentence: companion results prove rational Hodge for arbitrary products of projective complex K3 surfaces and algebraicity of the Kuga–Satake correspondence for every such surface. The two withdrawn papers are exactly those two companion results, and the current summary no longer has that last sentence. That is why the family title now matches the summary's first sentence. There is one more layer. From day one, the exceptions passage in the README called this work "proof of the Hodge Conjecture for CM abelian varieties", and that sentence is identical across both editions. So the narrow name was inside the repository from the start, and the contents file moved onto it. The paper heading the family also changed to the manuscript carrying that name as its title.

The mathematics is outside this article's scope. In the shape of the record, what disappeared is less three manuscripts than a headline claim covering a whole class, and that change leaves no trace at all in the figure 722 → 719. Neither does the fact that two files in the same repository had been calling the same family by two different breadths.

Open the README of openai/math today and how much formal verification has been done is stated in one line: the repository has ~42% top-line results formalized. That single line is the source of the figure quoted most often in coverage. Open the same spot at the release-day commit and the sentence is not there. A different sentence sits in the same bullet, in the same position.

The README was downloaded at each of the two commits and the same bullet compared line for line. It is not only that a number appeared. The thing being counted changed.

Two things moved in those two days. A word became a number, and the unit being counted shifted from manuscripts to top-line results. The second is the larger change. A manuscript is a unit the repository counts as files, so anyone can count it the same way. A top-line result is not. What that phrase counts as one is taken up in the next section.

That line was not the only thing to change. The same commit touched three of the repository's explanatory documents. First, a line pointing at the history file appeared right below it, and the file being pointed at was itself created in this commit, which means that at release the repository had no place recording what changed when. Second, the Lean-side checking instructions grew. At release they were ten lines of install-and-run commands; this commit added a section naming five configurations that check supporting results rather than principal theorems, and a line saying that per-paper coverage and limitations live in separate scope notes. Third, the line giving the manuscript count changed from 722 to 719.

Put together: the sentences in which the repository explains the scope and limits of its own work arrived together in one commit two days after release, and the widely quoted 42% is one of them. That is why this article notes, every time it counts, which commit the number was counted at. The field §4 looks at runs the other way: it is identical at both commits. There, the fact that nothing changed is itself the value worth counting.

Measure again in the unit that was used first and you get the value "many" stood for. At release, 162 manuscripts were in the formalization catalogue and there were 722 manuscripts in total, so counting manuscripts gives 22.4%. Count again at the current commit and it is 23.9%. The actual value in the position the word "many" occupied sits nearly 20 percentage points below the 42% written in later.

The repository holds a file called the formalization catalogue. It lists which papers have been formalized in Lean, and a comment in its opening lines states its own scope: it is a list of papers whose main results have been formalized. Count that list, then match the paths it points at against the contents file, and you get a rate. It is a different value from the rate the repository writes in its README.

Neither side is wrong. The three rates count three different things, and on release day the spot the README's own rate now occupies held a word rather than a number. The figure below gathers them in one place.

The four rows count different things: papers whose paths join the formalization catalogue, the result families those papers belong to, the rate the repository writes in its README, and the word that stood in that spot on release day. The first two are values this article obtained by counting the repository's files directly, the third is the value the repository states, and the fourth is not a number at all. The catalogue itself holds 173 paper entries, of which 172 join the current contents file by path. The one left over is the manuscript §5 is about.

3.1162 and 300 are not before and after

The story that spread runs like this: it was 162 at release, and further work took it to 300. The repository's own record denies that ordering. The history file says the October 7 work added 6 formalizations and 5 other additions, bringing the total to 300 of 719. If adding six got you to 300, the value just before was 294, not 162.

So what is 162? It is the count of entries in the formalization catalogue at release. This article counted them, and in the current edition there are 173. The eleven added line up exactly with the history file's "6 formalizations and 5 other additions". The same work, in other words, was recorded as eleven in one ledger and as six in the other. The two numbers do not differ by moment in time. They differ by counting rule.

3.2"top-line result" is defined nowhere in the repository

To know what the denominator and numerator behind 42% count, you need the meaning of the phrase. This article looked in eight places: the README, the history file, the Lean library instructions, the Comparator instructions, the overview PDF released alongside (read end to end), the three commit messages, a search across the whole repository's code, and the issues and pull requests. The phrase appears in exactly two spots, that one sentence in the README and one sentence in the history file, and neither of them defines it. In the overview PDF it does not appear at all. Issues and pull requests both stand at zero, so there was no channel for anyone outside to ask.

With no definition, the only option is to work backwards from the numerator. The catalogue file contains several countable lists. We counted all of them, and none comes to 300.

Values at the current commit. The numerator 300 matches the length of no list this file holds. It could be a tally kept outside the repository, or an internal ledger counting by another rule, but the published files cannot tell us.

The second row comes close even in name. Inside the catalogue file there is in fact a list labeled main_results, and it carries 200 Lean declarations. At release it carried 185. This list is the only place in the repository that enumerates main results in a machine-readable form, and its length is not 300 either.

More striking is that the two lists are not joined to each other. The same file holds 173 papers and 200 declarations, and there is no line saying which paper was formalized by which declaration. The specification provides two places for exactly that. One field pairs the original prose statement against the formal declaration (alignment), and another records, per source, which theorem or which section is being pointed at (sources[].location). Neither is used even once in this file. So there is also no way to read out of the repository's files which sentence in which paper is that paper's main result. "top-line result" is not the only thing left undefined.

3.3The most-read explainer sourced 300 to a file that has no 300 in it

The most widely read explainer on this episode is Melissa Lee's October 9 piece, written for The Conversation and picked up by phys.org. It says OpenAI claims to have formalized 300 main results as of writing, and hangs a link to the formalization catalogue file on that sentence. This article downloaded both editions of that file and searched the text. "300" does not appear in it once. The only place 300 is written is the history file.

It is hard to call that the reader's mistake. The line in the README puts the catalogue link and the rate inside one sentence. Right after saying that the Lean library and the formalization catalogue describe the available formal proofs, the tail of the same bullet says the repository has ~42% top-line results formalized. A reader following the link will take the rate to be a value that came out of that catalogue. Count that catalogue and you get 173.

3.4There is a third record inside the repository

Besides the catalogue, the repository writes formalization down in one other place: 242 files under lean/docs/. For each result family, these scope notes say in human-readable prose exactly what that paper's Lean proof established, and they link to Comparator files that actually exist. This article opened all of them and pulled out the paper paths they link to, which came to 340 papers. Of those, 168 are not in the formalization catalogue. We opened two at random, and the linked Lean files were really there and not empty shells.

What these documents record is scope. Each one identifies the manuscript its formalization belongs to, states in readable sentences what the Lean proof established, and sometimes goes on to state what it did not establish. The scope note for the family on the irrationality exponent of π, for instance, says plainly that the Flint Hills series consequence the paper derives separately falls outside the statement chosen here. The job of recording how far into the original a formalization reached is being done in these documents, in prose.

Nor are they hard to find. The repository's contents file hangs a link to these scope notes on each family: 235 of them at release, 242 now. The Comparator instructions from the previous section also carry a line saying to look at these documents for per-paper coverage and limitations. That line, though, was added two days after release.

3.5How to count these numbers again yourself

Every number in this section came out of published files, so anyone can count them again. Download the formalization catalogue at the release-day commit and at the current one, count the paper entries, and match the manuscript directory paths those entries point at against the contents file. Do not match on titles. There are five pairs where the same paper is written with Unicode symbols on one side and spelled out in ASCII on the other, and one pair of genuinely different papers carrying identical titles. The only stable unit for counting papers in this repository is the file path.

The release-day commit is adc7f124 and the current one is fd4aeeb2. As of October 13, 2026, when this was written, no commit has landed since.

One word needs splitting first. In writing about this episode, "verification" points at three different jobs. Run them together and everything below reads wrong.

None of the three substitutes for another. Every rate counted in §3 concerns the first. What this section looks at is the second.

That a machine check cannot stand in for the second is not something this article is saying first. Our own report of August 9, 2026 set out the gap formal verification cannot close as five patterns. That account is not repeated here. What is new this time is elsewhere: that gap is now written down as a grade, in one vendor's machine-readable metadata.

4.1The value written at the end of the catalogue

At the very end of the catalogue file counted in §3, there is not a list but a block describing the work as a whole. It comes to three lines.

This block is identical, character for character, at the release-day commit and the current one.

This file format is not OpenAI's invention. It is a public specification maintained by the mathlib-initiative, and openai/math uses version 0.4 of it. Download the specification and the description for the review.status field lists a recommended vocabulary of six steps: unchecked, agent-reviewed, self-assessed, peer-reviewed, author-verified, and other/freeform. The value the repository wrote is the bottom one of those six.

▲ The value the repository actually wrote (highlighted) alongside the other five values the description lists. The order follows the description as quoted in the body; the field itself is not an enforced enum.

These six steps are not a list of values the specification enforces. In the machine-readable schema the type of this field is simply a string, and the six steps are a recommended convention stated in the description. The neighboring automation.method field does enforce five values; review.status does not. So the accurate description is not "the bottom of a standard-mandated six-level enum". It is: a freeform field for which the standard offers a six-step recommended vocabulary has the bottom value written in it.

The block itself, though, is not a place you may leave empty. The specification pins down four top-level fields as required: project information, the source list, the automation method, and this review block. What the repository chose was not whether to write something but what to write in a field that has to be filled. The value it chose is the bottom one. The fields in the next subsection are the opposite case: leave those empty and the specification says nothing at all.

The other fields in the same block have to be read alongside it. The field for who reviewed and the field for how they reviewed are both empty, and the method by which the formalizations were produced is given as an agent. Put together, on the question of whether a person checked the machine-made formal proofs against the original claims, the repository has written "not done" in a machine-readable place.

4.2This is not the only empty field

We read the full specification and went through the optional fields one by one in the openai/math catalogue. A set of them is unused: the field for where a formalization diverges from the original, the field pairing the original prose statement against the formal declaration, the field for whether the original authors took part in or approved the formalization, the field for how many holes were left inside a proof and which axioms it used, the field for unproven external results a proof assumes, and the field for which models and tools did the automation and at what cost. Those are six phrases, but the specification cuts the same ground into more fields than six. Two separate fields count the holes left in a proof, the axioms used get a field of their own, and the automation side breaks into three more: models, tools, cost. Counted as fields, there are ten.

This is not to say the optional fields went unused as a class. Some are used. The field giving the scope of the work in one line, "Partial progress.", is used; so is the list of 200 declarations counted in §3; so is the field enumerating the Lean libraries that were imported. The dividing line runs elsewhere. The fields that are filled record what was done. The fields that are empty record how much of the original it covered and who confirmed it. The ten transparency fields gathered above are all of the latter kind.

This too is not read one way. Whether an empty field means the tracking was not done, or that it was done and not written down, cannot be told from the published files. As far as can be stated: of the ten optional transparency fields the specification provides, none is filled.

4.3A mathematician wrote a sentence that same week aimed straight at that field

On October 9, a guest post about the Lean theorem prover appeared on Terence Tao's blog. The author is not Tao but the mathematician Thomas Hales. It is a general argument about how Lean ought to be handled, and inside it is a sentence that points exactly at the field this article is about.

… a proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity. Source: Thomas Hales, guest post on Terence Tao's blog, 2026-10-09

In the same post he unpacks that into two plainer questions. Is the verified theorem the one we think it is? Do the definitions inside Lean correspond to the definitions we have in mind? Fairness requires noting that he is not running formal verification down. In that same post he also writes that a Lean proof should not be trusted until the kernel has checked it. He is on the side of insisting on the machine check, and then asking for statement-fidelity review on top of it.

A word about scope. The OpenAI case Hales raises in that post is the September 8 Navier–Stokes announcement, not the October 6 release of 722 manuscripts. He did not comment on this release. This article sets the two sentences side by side for a different reason. A mathematician wrote that nothing should be accepted before a human audit, and the repository wrote "not done" in the very field where that audit is recorded. They are three days apart, and neither was written with the other in view.

4.4The same day, that gap turned into a theorem

On the very day the repository went up, a paper was submitted to arXiv. It is by Bastounis, Circelli and Hansen of King's College London and Cambridge, and its title already says "lost in translation". Here is the claim. Resolving the ambiguity of natural-language mathematical statements sits arbitrarily high in the Solvability Complexity Index, and that index is infinite for it. The halting problem has index 1, so faithful autoformalisation comes out harder than any computational problem, the halting problem included.

It did not stay an abstract worry. The paper points at two places in OpenAI's Navier–Stokes Lean formalization where the natural-language statement and the formal one come apart. One is the number of derivatives: the Lean side imposes a condition one degree stronger than the smoothness the natural-language inequality requires. The other is an expression bounding pressure and flux, where the Lean inequality carries a variable that the natural-language statement does not have.

The disclaimer the authors attached belongs next to it.

Disclaimer: We do not make claims about the correctness of OpenAI's NL proof, we only make statements about mistranslations into Lean. Source: arXiv:2610.08144

The scope again. What this paper examined is one formalization from September 8, not the 722. Writing that discrepancies were found in the Lean formalizations of the 722 would be false. The sentence that can be written is this one. That a formal statement and a natural-language statement can come apart is not an abstract worry; two places were found actually apart in another Lean artifact from the same company; and that report was submitted on the very day this repository was published.

Reduced to one line: the machine checks whether the translation holds together. It does not check whether the translation says the same thing as the original. The place that records whether a person did that job is the review field, and the value written there is "unchecked".

Back to the number counted in §1. Twenty-seven manuscripts were given a new edition. Match those twenty-seven against the release-day formalization catalogue and they fall almost entirely to one side. Twenty-six were outside the catalogue; one was inside. The three withdrawn papers were all outside as well.

We do not settle that skew in either direction. It can be read as formalization having filtered the errors out, or as people having looked only at the unformalized side. The repository does not say which. What we verified stops at the fact that the repairs tracked the boundary of the list almost exactly. More important than the skew is the one manuscript on the inside of it.

5.1In that one inside manuscript, the editions came apart

It is the manuscript titled "Taming implies compatibility" on four-manifolds. A new edition appeared on October 6 and the date in its directory name moved from September 23 to October 6. The README of the new edition carries a version note, and one of the changes listed there is a narrowing: the cone-equality claim was restricted to hold only under a particular condition. The one-line summary in the contents file, though, does not mention the narrowing. It records only what was added; the restriction of scope appears solely in the version note inside the directory README.

The catalogue entry for it, though, is exactly the same now as it was at release. The path it points at is still the September 23 directory. The third record from §3.4 behaves the same way. The scope note for this family is byte-identical across the two commits, and the PDF it links to in its text is the September 23 edition. So there are two Lean-side records, and both point at the old edition. Open the README in that September 23 directory and there is no marker saying it has been superseded.

The manuscript whose claim was narrowed and the two records saying that manuscript was formalized point at different editions. The contents file was updated to point at the new edition; the two Lean-side records were not.

There is one more thing. The README in the old edition's directory still holds the BibTeX block issued for citing that edition. The new edition's README links back to the old one from its version note, opening a path upstream; the reverse direction is not open. From the old edition there is no way to learn that a newer one exists, and the citation block sits there, unmarked, ready to be cited.

Does that mean the Lean proof is wrong? No one can say. The narrowed claim is the weaker one, so the formalization may well still hold; or the formal statement may be pointing at a broader claim that no longer exists. Whether the two match has not been checked by anyone. The same file says "unchecked" in exactly that spot.

5.2The specification has a field for exactly this case

One of the optional fields passed over in §4 is a place made for exactly this situation. The specification has a field called fidelity.divergences, and its description spells out what to put there: the points where a formalization diverges from the original, meaning where it generalized, where it weakened a hypothesis, where it renamed a lemma. Weakening a hypothesis is the same kind of thing that happened in this manuscript. In the openai/math catalogue, though, the field is not merely empty: the fidelity block does not exist at all. That holds in both editions.

Set against that, what the repository did well shows up too. The README said previously released editions would remain accessible, and they do. The commit hash pinned into the withdrawal notices in §1 is the same instinct. Preserving editions is something this repository got right. What is empty is not preservation but correspondence: the place recording which edition is paired with which formal proof, and the place recording how the two diverge if they do.

That promise does not reach beyond the manuscripts. Take the overview PDF released alongside them. It describes the collection as a whole, and its contents changed in the fix commit: the manuscript count on the cover fell from 722 to 719. The cover date, though, still reads October 6, and there is no version note and no new file name. The old edition surfaces only by walking back through the git history. The promise in the README was made about manuscripts, so this is not a promise broken. What this article counts is not promises but fields. Two documents bearing the same date carry different numbers, and nothing inside either document tells them apart.

On September 29, a week before the repository opened, the Advisory Group on Mathematics and Artificial Intelligence published a document titled "Responsible Release of AI-Generated Mathematics". It drew on more than 600 survey responses and carried five numbered recommendations. Before reading it, fairness requires setting out how the group came to exist.

By the founding announcement, the starting point was OpenAI's. OpenAI approached several mathematicians about forming an external advisory board, and those approached decided instead to form an independent body and invite others into it. The host is the Institute for Advanced Study in Princeton. There are nine members: François Charles, Camillo De Lellis, Timothy Gowers, Martin Hairer, Nikhil Srivastava, Ulrike Tillmann, Ravi Vakil, Edward Witten and Melanie Matchett Wood. Some summaries list Terence Tao as a member of this group; his name is not on the nine. He published the founding announcement on his blog, nothing more. So these recommendations are not criticism arriving from outside. They are a document that came out of a seat OpenAI convened and that turned into an independent body.

6.1The five things Recommendation 3 asked for

Of the five recommendations, the one that meshes with this article is the third. It is the clause on what to publish alongside a released result, and it names five items.

For each result released, the AI lab should make public the name of the model, the prompts used, a (summarized) chain of thought, the time taken, and the estimated cost of computation. Source: AGMAI, "Responsible Release of AI-Generated Mathematics", Recommendation 3

Match those five against what the repository actually published and one column stands out. Four of the five already have a dedicated field in the file format from §4. This is not a demand to release model weights; it asks for a name, the prompts, the time and the cost to be written down.

Built by opening the full text of the recommendation, the formalization catalogue, and version 0.4 of the specification the catalogue follows, and matching them. The recommendation asked for five items per result; what the repository supplied is one as a collection-wide figure and one for ten families.

A second recommendation overlaps. The fifth asks that, for each solution to a problem, it be made clear exactly how AI came to be used. Where the repository does that job is the three README sentences from §1: that the vast majority of results came out of the same procedure, that two pieces of work did not follow it, and that one of those writeups was human edited for readability. Because that is said about the collection as a whole, the unit does not match the one the recommendation asked for. As §1 showed, the manuscript-level READMEs have no slot for such a statement. Worth recording, though, is that those three sentences name the exceptions outright. That is the side that did not round everything off into a uniform process.

6.2Another project on the same specification filled those fields

There is an obvious objection to make about empty fields: isn't everybody's left empty? We opened the repository list of the organization behind the specification and looked for projects using the same format. One of them, the formalization showing the sum-product conjecture false over the reals, has those fields filled in. Its review status reads self-assessed with an agent audit, it carries reviewer names and review notes, and it records the models and tools used, the time it took and the cost. It also writes down its own limitation: this was not independent peer review.

We do not generalize from this one case. That project is small (one theorem, four authors) and nothing like openai/math in scale, and the specification version it uses is 0.3, one step behind. So nothing can be said about what other projects mostly do. What can be said is this. At least one, inside the same ecosystem, filled the same fields in a form a person can read.

6.3Even the item that was published is uneven

We looked separately at the one item of the five that was partly supplied: the ten families for which reasoning summaries were published. TechCrunch noted those ten first. The point this article adds is that the ten barely overlap with the formalization catalogue. Twenty-two papers belong to those ten families, and nine of them appear in the catalogue. By family, six of the ten have no formalization at all by the catalogue's reckoning.

That sentence carries a condition. Match it against the third record from §3.4 and all six of those families do have a scope note in lean/docs/ along with Comparator files that really exist. So "no formalization at all" is true only by the official catalogue. The fact that the two records give different answers turns up here once more. To add: the contents entries for those six families carried links to their scope notes from day one. Nothing was concealed from a reader who wanted to look. It simply did not enter the tally.

6.4The group that issued the recommendations declined to judge compliance

Two more voices came out of mathematics that same week. Both are about something other than this article's subject, so they are recorded here as position markers only. One is a four-post thread Terence Tao put on Mastodon around 18:00Z on October 6, arguing that solutions to open problems are being harvested at scale in a way that is not sustainable, leaving many areas of mathematics far more barren than they would have been had they been worked through in the traditional way. Two things have to be clear. That thread predates the repository's publication by about four hours, and the name OpenAI does not appear in it. It was not written in response to this release, and it does not single out any company. The other is the Association for Human Mathematics statement of October 7, issued in the name of 808 members, saying that putting out more than 700 files at once is a demonstration of power rather than a demonstration of scholarship. This article neither endorses nor disputes that position.

The advisory group that issued the recommendations, meanwhile, stepped back twice in its October 6 statement. First it wrote that its advisory role should not be read as a judgment on the impact of these results, nor as an endorsement of the process by which OpenAI obtained them. Then it closes like this.

We have discussed them with OpenAI and appreciate the company's willingness to engage. While we consider these discussions constructive, it is ultimately up to the mathematical community to assess the extent to which our recommendations were followed successfully. Source: AGMAI, statement on OpenAI's release of mathematical results, 2026-10-06

The people who wrote the recommendations said they would not rule on whether they were followed, so this article does not rule either. What it did amounts to setting the five items next to the four empty fields. That is clear enough on its own. To add one thing: the recommendations open by asking labs to stop testing advanced mathematical problems on unreleased models, while the first paragraph of the openai/math README says that as part of model development they evaluate their models on open research problems. TechCrunch noted that collision first.

Why Pebblous cares

That field is what Pebblous sells

What Pebblous does is judge whether data is in a condition fit for AI, and leave that judgment behind as a record someone can read later. What this episode shows is that the job does not run properly even in the field with the strictest verification culture in the world. The point is not volume. Putting 722 manuscripts up at once is not the problem; nobody filling in the field that records what was confirmed and to what grade is. And as §6 shows, the field was already there. Building the field, filling it, and reading what is in it are three different jobs, and only the first was properly in place here.

Verification has three layers and most of us count only the first

The three things separated in §4 are not a distinction peculiar to mathematics. AI-generated training data, synthetic data and labels have the same three layers: what passed a schema check, what a person compared against the source, and what the domain accepted as fit for use. Most organizations count only the first and call that number "verified data". Few count the second, and fewer still leave the third behind as a record.

The edition mismatch in §5 adds a layer on top of that. The moment editions come apart, even the first layer's record stops telling you what it was a check of. This is the very point our August 2026 report made in saying that AI proofs leave no provenance, except that this time provenance was left, and came apart instead. Leaving a record and keeping that record aligned with what it points at are two different jobs.

▲ An original Pebblous diagram. It generalizes the split this article draws in §4 for the OpenAI repository — mechanical checking, statement comparison, mathematical-community judgment — to AI output in general (training data, synthetic data, labels).

Four questions to put to your own organization

First, is there a field in your output records that states the grade of "verified"? If not, settle the vocabulary before counting any rates. Unchecked, looked at by an agent, sampled by a person, and compared exhaustively do not deserve the same word. Second, is anyone reading that field? In this episode OpenAI filled it in: at the lowest value, in a machine-readable place, from day one. Nobody read it, that is all.

Third, is the edition your verification record points at the same edition now in use? Is it pinned by commit or hash, or hung only on a directory path? A path drifts silently when a name changes, and the file still opens perfectly well after it has drifted. Fourth, what is the denominator of the "verification pass rate" you report? Items? Families? Main results? Are three different numbers circulating inside one organization at the same time? What §3 showed is exactly that condition.

The same measure, turned on ourselves

Where Pebblous stands is on the side of making the field that states an AI output's verification grade a standard, and counting whether that field got filled. We are not in the volume race. It has plenty of entrants already. And turning the same measure on ourselves first gives this. Pebblous's DataClinic reports and synthetic-data outputs still have no formal equivalent of a review.status field. Since this article counts OpenAI's empty fields, writing down our own comes first.

References

The object of this article — repository files

• 1.OpenAI, openai/math — release-day commit adc7f124 (2026-10-06 21:58:50Z), fix commit 30148886 (2026-10-08 05:03:50Z), current commit fd4aeeb2 (2026-10-08 05:20:00Z). Every figure in this article was counted by downloading README.md, CONTENTS.md, history.md and lean/formalization.yaml at each of the two editions. The instruction comparison in §2 and the edition comparison in §5 additionally pulled lean/ComparatorChallenges/README.md, overview.pdf and lean/docs/342.md at the same two commits, plus the two manuscript-directory READMEs.
• 2.The three withdrawal notices — preprints/<directory>/README.md. All three open with "Withdrawn on October 6, 2026." and close with the same sentence. The sign-error equation appears in the notice for the September 18 manuscript, "Algebraicity of Weil classes on split abelian eightfolds"; the archive commit hash is pinned in all three.
• 3.The 242 files under lean/docs/, lean/ComparatorChallenges/README.md and the overview.pdf released alongside — the terminology search in §3.2 and the third record in §3.4 came from here. There are two routes to lean/docs/: the per-family links in CONTENTS.md (235 at release, 242 now) and the "per-paper coverage and limitations" line in the Comparator instructions. ⚠️ That second line was added in the fix commit, and lean/README.md itself does not describe this directory.
• 4.OpenAI, Sharing AI progress in mathematics — ⚠️ the official announcement. Access was blocked while this article was being written, so the full text could not be read. That is why nothing from it is quoted in the body.

Specification and recommendations

• 5.mathlib-initiative, the formalization.yaml specification, version 0.4 — the six-step recommended vocabulary for review.status, the five enforced values of automation.method, and the ten optional fields counted in §4.2 are all defined here.
• 6.mathlib-initiative, sum_product, its formalization.yaml — the comparison case in §6.2. ⚠️ It uses specification version 0.3 and is a small project covering a single theorem. No generalization about the ecosystem is drawn from this one case.
• 7.AGMAI(Advisory Group on Mathematics and Artificial Intelligence), Responsible Release of AI-Generated Mathematics, 2026-09-29 — drawn on more than 600 survey responses, with five numbered recommendations. The verbatim quote in §6.1 comes from the third.
• 8.AGMAI, Statement on OpenAI's Release of Mathematical Results, 2026-10-06 — source of the quote that closes §6.4, the sentence in which the group hands assessment of compliance to the mathematical community.
• 9.founding announcement of the advisory group, 2026-09-21 — the list of nine members and the account of OpenAI making the first approach are here. ⚠️ Terence Tao published this announcement on his blog but is not on the list of nine.

Scholarly and expert sources

• 10.Thomas Hales, What mathematicians should know about the Lean Theorem Prover (guest post on Tao's blog), 2026-10-09 — ⚠️ the author is Thomas Hales, not Terence Tao. The OpenAI case this post raises is the September 8 Navier–Stokes announcement, not the October 6 release.
• 11.A. Bastounis · F. Circelli · A. C. Hansen, Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs, arXiv:2610.08144, submitted 2026-10-06 — source of the two discrepancies and the authors' disclaimer in §4.4. ⚠️ What this paper examined is one Navier–Stokes formalization.
• 12.Terence Tao, Mastodon thread, four posts, 2026-10-06 18:00Z — ⚠️ it predates the repository's publication by about four hours and does not name OpenAI.
• 13.Association for Human Mathematics, AHM Statement on OpenAI's October 6 Release, 2026-10-07, in the name of 808 members — ⚠️ the statement was also reposted on Tao's blog, but the words are not Tao's.

Coverage and commentary

• 14.Melissa Lee(The Conversation), republished on phys.org, 2026-10-09 — the subject of §3.3. It links the formalization catalogue as the source of 300, and that file has no 300 in it.
• 15.TechCrunch (Tim Fernholz), 2026-10-08 — the report that first set out the collision between the recommendations' opening request and the first paragraph of the README, the ten families with reasoning summaries, and the Melanie Matchett Wood quote. The attributions in §6.3 and §6.4 go here. · aiweekly.co, 2026-10-09 — the route by which the figure 162 circulated.

Related Pebblous blog pieces

• 16.The provenance gap in AI mathematical proofs (2026-08-09) — the direct predecessor to this article. Its section setting out the gap formal verification cannot close as five patterns is the starting point for §4. · The Fields medallists' declaration (2026-09-14) · The Leiden Declaration (2026-06-30).