Ten Off the Shelf

Ten problems came off a shelf that took sixty-two years to build. Six moved by a hair, four ended outright, and not one of them was a new question.

In 1964 a French mathematician named Eugène Ehrhart asked a question about balance. Take a convex body, meaning any solid with no dents in it: a ball, a cube, a lopsided potato. Lay it on the integer grid, the lattice of points whose coordinates are whole numbers. Now demand two things at once. Exactly one lattice point may sit strictly inside the body, and that point has to be the body's own center of mass.

How big can such a body be?

Ehrhart worked out what he thought the answer was, a particular triangle and its higher-dimensional cousins, and he could not prove it. Neither could anyone else. The question sat there for sixty-two years, which is longer than most mathematical careers.

On the first of August, 2026, it was answered. The answer is the one Ehrhart guessed, and the proof arrived inside a 249-page document that also settled nine other questions, published by OpenAI, with no human author named anywhere in it.¹

That is the release this notebook is about. Ten more sit underneath it. Each child takes one result and teaches the mathematics. This one does the job none of them can do alone, which is to look at the ten as a set and ask what kind of thing just happened.

I want to be exact about the register here, because the subject invites two bad readings and I would like to avoid both. This is an audit. Where the release is careful, and it is careful far more often than its coverage suggested, I say so and show the receipt. Where I could not check something, I say that too, in the sentence where the claim is made, not in a caveats section at the end.

What I could check came out lopsided in the release's favor.

The last three are where this gets interesting, and none of them is a complaint about the mathematics.

Ten problems, off a shelf built over sixty-two years

Before anything else, the ten questions themselves. In plain language, in an order chosen for you, not for the paper, and with no chapter numbers attached. You will not learn the mathematics from this section. You will learn what is being asked, which is the thing almost every account of this release skipped straight past.

Start with the two you can picture. Ehrhart's, from above, asks which balanced shape holds the most volume. The second asks whether every group can be imitated by shuffling a finite deck of cards.

That needs one word unpacked. A group is a collection of moves you can compose and undo: the rotations of a cube, the ways of rearranging a deck, the integers under addition. Some groups are infinite and strange. The question, named soficity after a Hebrew word for finite, is whether any group at all, however exotic, can be approximated to any accuracy you like by permutations of finitely many objects. Approximated means that the composition table of your group is reproduced by shuffles, with as few errors as you care to specify. Almost everyone expected the answer to be yes for every group. Nobody had produced a counterexample, or a proof, in twenty-seven years.

Three more need one layer of abstraction. The first is a question about shadows. Given a group, there is a standard way to build an algebra of operators out of it, which throws away a great deal of information and keeps some. If two different groups cast the same shadow, must the groups themselves have been the same? Alain Connes conjectured that for a large and natural class of groups, they must, and the conjecture became the organizing question of a whole subfield.

The second is about spheres. Take identical balls and pack them into space as densely as you can. In two dimensions the answer is the honeycomb and has been known since Gauss. In three it is what greengrocers do with oranges, and proving it took until 1998. In a hundred dimensions nobody knows, and the interesting question has shifted underneath: not how dense the best packing is, but how good our best proof technique for bounding it can ever be. That second question is the one that got answered.

The third is the same question wearing different clothes. You want to send a message over a channel that flips bits at random. So you agree in advance on a set of permitted messages, called codewords, chosen far enough apart that no amount of flipping short of some threshold can turn one into another. The more codewords you allow, the more you can say; the further apart you keep them, the more noise you survive. Those two goals fight, and the question is how. The best known answers have stood since 1977 and 1978. Note that this is a packing problem too: codewords are points that must not come too close, which is why these two chapters end up in the same place later on.

Then a pair from combinatorics, both of them Erdős questions, and both about how much structure you can avoid.

The first is a coloring problem. Take a network where every pair of nodes is connected, and color each connection with one of k colors. Once the network is big enough, some color is forced to contain a triangle, meaning three nodes joined by three edges all of the same color. This is Ramsey theory, and its slogan is that complete disorder is impossible. The question is quantitative: how big is big enough, as a function of the number of colors? For two colors the answer is six, which you can check on a napkin. For twenty colors nobody knows, and until this release nobody knew even how fast the answer grows.

The second is about density. Fix some pattern you want to forbid, then ask how many edges a network on n nodes can have while containing no copy of it. That maximum is called the extremal number, and for most patterns it grows like n to some power. Erdős conjectured two things about how those powers behave when you forbid a whole family of patterns at once. Both conjectures turned out to be false.

The last three want a complexity frame, which is to say they are about what is hard to compute rather than what is true.

The permanent is the determinant's near-identical twin. Both are sums over all the ways of picking one entry from each row and column of a square matrix. The determinant attaches a plus or minus sign to each term; the permanent adds them all with a plus. That single difference is the gap between something every linear algebra course computes in cubic time and something nobody knows how to compute efficiently at all. The question is how much harder the permanent provably is, and progress on it has been agonizing, because proving that something is hard is far more difficult than proving something is easy.

Then a question about games. Imagine a cooperative game two players cannot reliably win: they are questioned separately, cannot communicate, and have to give consistent answers. Now play many copies at once. Intuitively your chance of sweeping every copy should collapse exponentially in the number of copies. Proving that is called parallel repetition, and it is much harder than it sounds, because the players can correlate their strategies across copies. It gets harder still if the players are allowed to share quantum entanglement, which lets them coordinate in ways no classical strategy can imitate.

And last, the closest vector problem. A lattice is an infinite regular grid of points, like graph paper extended to many dimensions, described by a handful of basis vectors. Given a lattice and a target point that is probably not on it, find the nearest lattice point. In two dimensions you can eyeball it. In four hundred dimensions this is believed to be intractable, and modern post-quantum cryptography is built on the belief. The question here is how hard it is provably, and how rough an answer you can allow yourself before it becomes easy.

That is the set. Now the thing about it that took me longest to notice, and which changed how I read the whole release: every single one of those questions already existed. Each was posed by a named human being, published, and left sitting there. The oldest is Ehrhart's, from 1964. The newest was flagged as open in a 2004 paper by Cleve, Høyer, Toner and Watrous, in a footnote.

Now the caveat, and I want it in the prose and not in a footnote because the framing it corrects was everywhere. No chapter in the paper states how long its problem had been open. There is no "open for sixty years" claim anywhere in 249 pages. Every duration in that figure is arithmetic I did, from the earliest citation each chapter gives, which is why each bar carries its anchor where you can see it. The one exception is Chapter 6, which writes that its problem was "explicitly noted as open by 2004," and that is as close as the release comes.

Those citations have to exist before any of this works, so that is the first thing to check, and it is the failure mode everybody expects from a language model. Forty-six arXiv identifiers appear across the paper, the walkthroughs and the blog post. All forty-six resolve to real papers. Not one is a plausible-looking number attached to nothing.

The anchors themselves are as solid as I could make them without becoming a specialist in ten fields at once. Twenty-two priority papers are cited across the ten chapters, and for all twenty-two the abstract states the relevant result or conjecture plainly enough to date it. None of them required reading the body to establish who asked what, and when. That is a lower bar than it sounds, and it is also the bar this whole section rests on, so it is worth saying out loud which one I cleared.

Three of the paper's claims are not theorems at all, and they are the ones a hostile reader goes for first. Two sit in a single sentence: these are "the first improvements to the respective general high-dimensional exponents since 1977 and 1978." The third is that Kalorkoti's 1985 cubic lower bound on formula size has stood ever since. Nothing in the Lean touches any of them. They are assertions about fifty years of other people's work, and the only way to test one is to walk forward through everything that cites the original.

That turns out to be doable from a public API, and all three survive. Samorodnitsky, writing in 2024, calls the 1977 bound "the best known asymptotic upper bound for binary codes." Cohn and Zhao, in 2014, name the 1978 bound as the current best in all sufficiently high dimensions. And among the 49 works citing Kalorkoti, the strongest later bounds are quadratic, against a weaker target. Three claims about the state of three literatures, and the specialists best placed to contradict them say the opposite instead.

So the citations are real, the dates are real, and the records the paper claims to have broken were still standing. The one thing that is not in the paper is the sentence everybody quoted. The ubiquitous "AI solves 60-year-old problem" headline is downstream invention. That matters on its own, and it is also a warning about the rest of the coverage: several of the most repeated facts about this release are not in it.

There are three kinds of result here, and the coverage saw one

The ten are not one kind of thing. The difference between the kinds is larger than the difference between any two individual chapters, and once you see it the release stops being a list and becomes an argument.

Six of them improve a rate. Chapters 1, 2, 5, 6, 7 and 9 all take a quantity that grows with some size parameter and prove a better bound on how it grows. These are genuine asymptotic advances and every one of them is numerically inert at any scale you or any machine will ever touch. I will make that precise in a moment, because "numerically inert" is the kind of phrase that deserves a number.

Three of them refute something. Chapters 3, 4 and 10 produce counterexamples, and the paper groups them that way itself. A counterexample either is one or it is not. There is no asymptotic hedge available, no regime where it half works. Connes conjectured that groups in a certain class are pinned down by their operator algebras; Chapter 4 writes down two different groups with the same one. Everyone expected every group to be sofic; Chapter 3 writes down one that is not.

And one closes its problem outright, which is rare enough to be its own category. Ehrhart's bound is proved sharp, and it is attained, by an explicit simplex you can write down. In the plane the answer is exactly 4.5. Not asymptotically 4.5, not 4.5 up to lower-order factors. Four and a half.

Two details sharpen the split, and both are the kind of thing that gets flattened in a summary.

Chapter 8 does not merely improve its bound. The previous record was 4ⁿ, later pushed down to 4ⁿe^{−cn}, and the true answer turns out to be (n+1)ⁿ/n!, which is about e^{n+1}/√(2πn). So 4ⁿ became eⁿ. That is a different exponential, not a tightening of the old one.

Chapter 10's refutation is polynomial rather than marginal, and it is aimed at the live target rather than the easy one. The compactness conjecture's original 1982 form already had simple counterexamples, which Yuval Wigderson documented; what Chapter 10 kills is the repaired version, in which every member of the forbidden family has to contain a cycle. That version said the family as a whole would need density on the order of n^{4/3}, no cheaper than its cheapest single member. The counterexample family gets away with n^{4/3−1/48}, which is n^{21/16}, while every individual member in it still needs the full n^{4/3}. The family is cheaper than any one of the patterns inside it, and that is exactly what compactness forbids. The family it builds is connected and bipartite, more than the refutation strictly needs. The conjecture is not slightly wrong at the boundary. It is wrong by a polynomial factor.

The split matters because the two kinds age differently. A rate improvement is a position on a number line, and the next paper moves it again; six of the ten will be superseded, and their authors would tell you so. A refutation is permanent. Connes rigidity will never be true again, and no future work will make the sofic question open. So of the ten advances, four changed the map and six changed a coordinate on it, and the coverage that treated all ten as interchangeable was measuring the wrong thing. Keep the distinction in hand for the next section, where the coordinates turn out to be even smaller than they look.

The numbers are vacuous, and the doors they close are not

There are two questions you can ask about a result like these, and I want to ask both, because the answers point in opposite directions.

The first question is how far the number reaches. Take Chapter 7, which proves that finding the closest grid point stays hard even if you only want an answer within a factor of n^(1/400). That exponent is doing a lot of work. For the approximation factor to reach a mere 2, you need n ≥ 2⁴⁰⁰, which is about 2.58 × 10¹²⁰, which is roughly 10⁴⁰ times the number of atoms in the observable universe. The theorem is true. The regime where it says anything you could act on does not exist and never will.

The pattern repeats across the six rate improvements. Chapter 5's lower bound on the permanent, C(perₙ) ≥ (n²/144)(log₂log₂n − 3), where C counts the gates in an arithmetic circuit, is negative until n passes 256, and the theorem states its own threshold as n ≥ 2¹⁶ = 65,536. Chapter 6's parallel repetition decays like ε¹³, where ε is the error you are trying to drive down, so at an error of a tenth you need something like 10¹³ repetitions, multiplied by a constant the chapter leaves unspecified. Chapter 9's Lean file pins its explicit constant at 1/(6e³⁸), which is about 5.2 × 10⁻¹⁸. Chapter 2 beats the 1977 and 1978 code records at every parameter, and on its kissing-number strand that means moving an exponent from 0.400944 to 0.39661, a gain of about 0.0043 bits per dimension. And Chapter 1 moves the sphere packing exponent from 0.59906 to 0.60440, an improvement of 0.89 percent.

I did one piece of arithmetic here that the paper does not do, and I want to show it, not assert it. Chapter 5's bound is an improvement on a bound of order n², and order n² is also roughly what you get for free, since any circuit computing the permanent has to read all n² entries. So when does the new bound actually beat the free one? You need (log₂log₂n − 3)/144 > 1, which means log₂log₂n > 147, which means n > 2^(2¹⁴⁷). The exponent alone, 2¹⁴⁷, is about 1.78 × 10⁴⁴.

That is not a criticism of Chapter 5. Lower bounds in circuit complexity are notoriously scarce, and moving one at all is real work. It is a criticism of any sentence that reports the result without saying which n it has in mind.

Now the second question, which is the one almost nobody asked: what does each result actually settle?

Chapter 1's 0.89 percent is the smallest number in the release. It is also attached to the result that closes an entire method. The Cohn-Elkies linear programming bound has been the main lever on sphere packing in high dimensions since 2003, and Chapter 1 proves that no function of that type can ever push the rate past √(e/(2π)), which is 0.657744…. Anyone still pulling that lever now knows exactly where it stops. They can stop pulling.

Meanwhile Chapters 3, 4 and 10 carry no numerical improvement whatsoever, and they are the ones that end decades-old questions.

Sort the ten by how far their numbers reach and you get one order. Sort them by what they settle and you get almost the reverse. That anti-correlation is the most useful single thing I found in three days of reading, and no single chapter shows it to you.

The chapters are more careful than their headlines

This is the part I did not expect, and it is the reason the rest of this notebook gets to be skeptical without being a hit piece.

Chapter 7 is about lattice problems, which are what post-quantum cryptography is built on. It never names Kyber, Dilithium, ML-KEM or ML-DSA. Not once. Its entire discussion of cryptography is a single passage ending with the observation that those applications "rely on appropriate structured or average-case assumptions, rather than directly on the worst-case NP-hardness of CVP." And there is a harder reason underneath the caution: the approximation regime cryptography actually uses sits inside NP ∩ coNP, so NP-hardness can never reach it. The chapter contains the proof that its own most exciting reading is unavailable. Every "AI breaks encryption" take was manufactured downstream.

Chapter 3 does something similar three separate times. Soficity is the hypothesis under which four other open problems become theorems: Gottschalk's surjunctivity conjecture, Kaplansky's direct finiteness conjecture, Lück's determinant conjecture, and the algebraic eigenvalue conjecture. Finding a non-sofic group removes the universal route to all four and refutes exactly none of them. The chapter says so in its own words: "We do not know whether Rˣ is surjunctive. A positive answer would produce a surjunctive nonsofic group, while a negative answer would disprove Gottschalk's conjecture."

The most absolute-looking result in the release has consequences its own authors carefully fenced off, in writing, in the paper. I think that is the fairest single fact about the document, and it belongs before any criticism, not after it.

Even Chapter 8 does it, and that is the one I would have bet against. It is the cleanest result here: a bound of (n+1)ⁿ/n!, proved sharp, attained by a simplex you can write down. The obvious next sentence is that the simplex is the answer. The chapter does not write it. What it writes instead is that "we do not determine whether these are the only equality cases," which leaves the classification of extremal bodies open even while the bound itself is finished.

Chapter 2 is careful about somebody else's work rather than its own, which is the version of this that is easiest to check and easiest to get away with skipping. It beats the coding records of 1977 and 1978, and that is exactly the setup for the phrase "unimproved for nearly fifty years." The chapter does not use it. It writes that the work since then "improved only lower-order factors," and I went and looked: Cohn and Zhao's 2014 abstract says they revisit the 1978 argument and "improve their bound by a constant factor." The hedge is accurate to the word. A less careful write-up would have claimed a fifty-year drought, and that would have been false.

Four chapters, four chances to make the story bigger, and four refusals.

The release replicates itself once, and nobody noticed

Chapters 1 and 2 sit next to each other and are about different things. The first is about packing spheres, the second about error-correcting codes. They were almost certainly the two least-read chapters in the release, because the first opens on twenty-six pages of Fourier analysis for a payoff of 0.89 percent and the second is fifty pages about codewords.

They arrive at the same number.

Chapter 1 gets there through the Cohn-Elkies linear program, the standard machinery of the field, and lands on a limiting rate of √(e/(2π)). Written as an exponent, that is the paper's α* = ½log₂(2π/e), which comes to 0.6044005442916777. Chapter 2 gets there through spherical codes, using Sidelnikov's hemisphere inequality, and recovers the same exponent in its own words "entirely from spherical certificates," with none of Chapter 1's machinery anywhere in the derivation.

This is the part that made me sit up. Chapter 2 never prints the decimal. You only see the agreement if you take both chapters' own statements and evaluate them yourself. I did, in three lines of Python, and got 0.6044005442916777 from each.

Independent re-derivation is the oldest form of verification mathematics has, older than peer review by centuries, and it is stronger evidence than any proof assistant can offer, because a kernel bug is a single point of failure and two disjoint arguments are not. It happened here inside one release, apparently by accident of how the chapters were organized, and it went unremarked in every piece of coverage I read.

It is worth being precise about what it does and does not buy, because "two chapters agree" can sound like a coincidence dressed up. Lean tells you a derivation follows from its axioms. It cannot tell you the derivation is about the thing you meant, and it cannot catch a modeling error shared by the whole file. Two derivations that share no lemma, no transform and no bound can only agree by accident or because the constant is real. No third option is available to them, and that is a form of assurance the certificate does not provide and was never designed to.

I also want to flag what kind of fact this is, because it is the argument of this whole notebook in miniature. Nothing about it required running anything. It required reading two chapters, noticing they were about the same quantity, and evaluating two expressions. Any reader could have found it; the release ships it and does not point at it; and the only reason it is in this notebook is that somebody sat down with the paper. That is what reading produces and verification does not.

Two honest counterweights, and they both make the section stronger, not weaker.

Both chapters' theorems confirm conjectures that were already on the record, cited in the paper as [AJCHLT20, Conjs. 3.1-3.2] and [CG19, Conj. 1.5]. Nobody in either field was surprised by the answer. The machine agreed with the people who had already guessed correctly, which is a real result and a different kind of result from finding something unexpected.

And Chapter 1's other theorem is a no-go. It proves that no Cohn-Elkies function can beat the rate it identified, which closes a line of attack rather than opening one. A field that spends the next decade not trying to improve the linear programming bound will have gotten more out of this release than one that spends it celebrating 0.89 percent.

Nothing here required asking a new question

Every one of the ten targets was crisp before the machine arrived. Each was a numeric bound to push, a conjecture to confirm, or a yes-or-no to decide. Each had a name and a date attached, which is why the shelf figure was possible to build at all.

It helps to be concrete about what the alternative would look like, because "asking a new question" sounds vague until you name examples. Grothendieck asking what a space would have to be for a certain kind of cohomology to exist. Shannon noticing that information had a quantity. Erdős deciding that the interesting thing about a graph property was the threshold at which it appears. In each case the hard part was not answering, it was seeing that there was something there to ask about, and formulating it well enough that an answer could exist.

Nothing in this release does that. Every target was already formulated, already published, already understood well enough that a specialist could state it in a sentence. The machine was pointed at ten closed-form questions and it closed them.

That is a real boundary and it is checkable, which is unusual for a claim about what machines can and cannot do. The evidence is the same ten citations that produced the chronology, read as a limitation instead of as a chronology.

I want to give that second counterweight its full weight, because "it was just search" is both the most common dismissal and clearly wrong.

The Connes chapter supplies its own toy model, which is rare in a paper of this kind and charming. Take four points, the pairs of bits 00, 01, 10, 11, with each equally likely. Add them bitwise and you get one group, the Klein four-group, where everything is its own inverse. Now change the rule to (x,y) ⋄ (x',y') = (x+x', y+y'+xx'), which adds a carry only when both first bits are on. The same four points, with the same probabilities, are now the cyclic group of order four, where one element has to be applied four times to get back where you started. Same set, same measure, different group.

The refutation is that idea grown up. The operator algebra remembers the four points and how they are weighted, and it need not remember which of the two laws you used. Chapter 4 states that in one sentence, which I quoted in the figure above. It is an idea, not a sweep. Somebody or something had to think of it.

One more thing belongs in this section, because it corrects a claim the coverage made and the paper did not. One of the ten is not finished. Write R_k(3) for the smallest network that forces a same-colored triangle when you have k colors to work with. The Ramsey chapter proves it grows like k raised to some constant times k, which is what the chapter's k^Θ(k) says, and which is a genuine advance over the previous purely exponential bound. What it does not do is pin the constant. The proof leaves it somewhere between 1/3 and 1, so a factor of three survives in the exponent of the exponent, and the chapter says so. Ten advances, one of them explicitly partial, and I did not see that fact reported anywhere.

Can you tell whether any of it is right?

Every result in the release ships with a Lean certificate. The repository as published held 842,760 lines of Lean across 4,319 files, about 356 MB, which works out to roughly 3,385 lines of formal proof per page of paper. Those are the released numbers and they had a shelf life of about four hours. The tree that replaced them carries the same results in 23 files and 545,947 lines. Every figure in this section is measured against the released state, for reasons the next section is about. Chapter 4 alone accounts for 352,269 of those lines, or 19,570 per page, most of it machine-generated certificate data. One file in that chapter, Entry002.lean, is 3.9 MB and 51 lines long, because it holds 424 integers of about nine thousand digits each.

So: is it right?

The strongest part of the answer is a thing the release never says out loud. Each of the twelve ComparatorChallenges files carries a line reading "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]. Those are Lean's three standard axioms and nothing else. sorryAx, which is what an unproved gap compiles to, is not on the list. Neither is Lean.ofReduceBool, which is what native_decide injects when a proof trusts compiled code instead of the kernel. I scanned every Lean file for the usual escape hatches and found zero native_decide, zero custom axiom declarations, zero unsafe, partial or opaque definitions, and zero @[implemented_by] overrides. Every theorem the challenge files declare exists in the tree and is proved, with no gaps, at every state of the repository I preserved.

The blog post says "we take responsibility for their correctness." The JSON says something far more checkable, and nobody quoted it.

Against that, four limits, all concrete.

First, a formal proof only certifies the statement as written. The release supplies its own example. As published, the Connes rigidity challenge asked for the refutation of an assertion that constrained one group and placed no hypotheses at all on the other, which meant a witness failing some unrelated condition would have discharged it without touching Connes's conjecture. Within four hours it was replaced by an explicit existence statement requiring both groups to satisfy every condition, plus a second theorem giving an infinite family. Nothing about axiom hygiene would have caught that. Only a person reading the quantifiers would. The full worked comparison belongs to Chapter 4's own notebook, where the two statements can sit side by side.

Second, the coverage is not uniform. The paper claims results on four Erdős problems. Three appear in the Lean by number, as erdos_183, not_erdos_180 and not_erdos_146. The fourth, #575, appears nowhere in the formalization, not even as a numeral. Any account that writes "formally verified" beside #575 is wrong.

Third, proved is not accepted, and how you measure that turns out to be the most interesting question in this notebook. It gets the rest of the section.

Fourth, the checker itself has been fooled. In the week of 25 July 2026, six days before this release, soundness bugs in Lean's handling of nested inductive types let a gap-free "proof of the Collatz conjecture" pass. The tool that accepted it was Comparator, which is the same tool these challenge files are addressed to. Carry the walk-back with the fact: the repository turned out to be a deliberate, openly-labeled bug demonstration by a formal methods researcher, the bug was fixed as soon as it was found, and the person who first wrote it up prepended a correction to his own post saying he had "jumped too fast on the easy story." The honest reading is the mundane one. Proof assistants are programs, programs have bugs, and this one behaved well when it had one.

And a fifth limit, which is mine and not the artifact's, and which I would rather state than have you find. Everything above is textual. I read the source, the manifests and the axiom allowlists; I never ran the build. Compiling 842,760 lines of Lean against a pinned Mathlib is a job measured in machine-hours, and until somebody does it, "the axiom allowlist forbids sorryAx" means the file says so, not that a kernel confirmed it. That distinction is the one this section is about, so it would be poor form to exempt myself from it.

There is a control group, and this section already owns it

Ten weeks before this release, on 20 May 2026, an OpenAI model disproved the Erdős unit distance conjecture, posed in 1946. That is the same species of result as three of the ten here: an outright refutation of a named, long-standing conjecture. This release is not a first, and almost nothing written about it said so.

What happened next is the measurement.

The nine were Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang and Wood. Nature ran the story on the 22nd under the headline "AI cracks 80-year-old mathematics challenge: researchers are astonished." Both papers went up on the same day as the announcement, and the nine-author digest followed Sawin by four hours and nine minutes. This section's prologue is a notebook about that one, and the rest of this section is what happens when you hold the two releases side by side.

Thomas Bloom's erdosproblems.com is the field's public ledger for these questions, and it is the closest thing to a scoreboard that exists. This is what it said when I checked it on 3 August 2026, two days after this release.

Read the right-hand column, not the statuses. The May result was written into the canonical record, credited to the model by name, and marked as Lean-verified, on the day it appeared. The four pages this release touches were last edited in January and April, which is to say months before it was published. So the correct sentence is not that the database has not caught up, which implies a queue. Nothing has happened to them at all.

I have to state precisely what OPEN means there, because getting it wrong has a recent and instructive history. Bloom himself: "The 'open' status only means I personally am unaware of a paper which solves it." It is a lower bound on acceptance rather than a verdict, and it can be stale in either direction. In October 2025 that confusion produced a public retraction, when an OpenAI executive posted that GPT-5 had solved open Erdős problems, Bloom corrected him within hours, and Demis Hassabis called the episode "this is embarrassing." Keep using the database, which is the best public signal available, and never write OPEN as though the field had considered a result and declined it.

With that stated, the comparison holds, and the honest reading of it is not the cynical one.

The difference is very unlikely to be quality. Nothing I checked suggests these ten are weaker than the May result, and the formalization here is far more thorough. May was one legible claim that a specialist could hold in their head. This is ten results across ten fields and 842,760 lines of Lean, published by an artifact that took fourteen distinct shapes in nineteen hours. It is harder to digest, so it has not been digested. That is a fact about throughput rather than merit, and it turns out to be the most important thing in this notebook.

One trap before leaving this section, because it is the easiest mistake available here. Erdős problem #113 already reads DISPROVED, and it has since 2023. It belongs to Oliver Janzer, not to this paper, and the paper says so itself in Chapter 10. There is no erdos_113 anywhere in the Lean. Say what a result proves, and do not award it money that belongs to somebody else.

The thing I went to cite stopped existing

I quoted a lot of numbers about the Lean repository in the last section. Every one of them needs a timestamp, and the reason is unusual enough to deserve its own heading.

openai/ten-proofs was created at 06:10:06 UTC on 1 August 2026. I have preserved fourteen distinct states of it from the following nineteen hours, and five of those fourteen were invisible to polling. I only have them because other people forked the repository at moments I did not observe, and I went and swept every fork for every reference. Thirteen of the fourteen are parentless root commits whose commit message is a single period. The version that was published on 1 August cannot be retrieved from upstream by any means I know of. As of the following day, GitHub's own public event feed for the repository shows no evidence that it was ever rewritten.

Now the turn. It is the reason this is not a scandal. Every change I observed was an improvement. A genuine loophole in a formal statement was closed within four hours. Independent kernel re-checking went from ten of twelve to twelve of twelve in a deliberate three-line push. A build defect that had stood since release was repaired. Nothing was ever weakened, at any state, by any measure I could apply.

Even the change that looks like a retreat is not one. When the declared theorem count fell from 41 to 38, the count of unproved gaps in the statement files fell from 45 to 42 in the same transition. Three claims went away and three unproved stubs went away with them.

For twenty-four minutes on 1 August, the repository had a history. One commit, with a parent, and the message "Remove unused Connes rigidity proof declarations." The message was accurate: 14,989 lines of unused lemmas removed, no claim touched. They kept a record once, it was useful, and then the practice stopped. That is a better sentence than "they never kept one," and it is also the true one.

The practical consequence is a convention you will see in all eleven notebooks in this section. Every number quoted from that repository is quoted against a dated, archived state, never against "the repo." The full investigation is its own piece, and the states themselves are preserved in a public archive so anybody can check my arithmetic against the same bytes I had.²

The general problem is worth naming, because it is going to outlive this artifact. A paper is a frozen thing; that is most of what a paper is for. A repository is a live thing whose identity is a name, and a name can be pointed anywhere. When the evidence for a mathematical claim is 842,760 lines in a repository instead of an argument on a page, citing the claim means citing a state, and the ordinary apparatus of scholarship has no slot for that. There is no accepted convention for "this proof, as it stood at 11:21 UTC." Nobody did anything wrong here. The tooling simply assumes a stability that the medium does not have, and every release of this shape will hit the same wall.

Nobody says who did what, and the model is not one thing

The paper's sole author is OpenAI. No human being is named anywhere in 249 pages. The words "Lean," "token" and "human" do not appear in it either, which means the document says nothing about how it was made.

The blog post says a little more. The results came from "an internal version of Astra, our next major model." I went looking for Astra. Across all 1,105 items in OpenAI's news feed, the string occurs exactly once, and it is the headline "OpenAI to acquire Astral," which is a different thing. Meanwhile the one published prompt for any OpenAI mathematics result names its model as "GPT 5.6 Sol Ultra." So the model that did the mathematics spans at least two identities and matches no public product.

That prompt is the most revealing document in the whole orbit, and it comes with a warning I have to put first. It is for a different result. It is two pages, it is titled for the Cycle Double Cover Conjecture, and the Cycle Double Cover Conjecture is not one of the ten. Whether the same harness produced these results is unstated anywhere. Read it as adjacent evidence about method and never as a description of this release.