--- title: "Ten Off the Shelf: What OpenAI actually released, read as a set" url: "https://chriscaruso.dev/notebooks/ten-off-the-shelf" type: "Notebook (interactive explainer)" site: "Caruso's Conjecture" author: "Chris Caruso" published: "2026-08-03" source: "writing/notebooks/ten-off-the-shelf.md" index: "https://chriscaruso.dev/llms.txt" narration_minutes: 57 narration_cues: "https://chriscaruso.dev/media/narration/ten-off-the-shelf/cues" narration_chapters: "https://chriscaruso.dev/media/narration/ten-off-the-shelf/chapters" tags: ["Mathematics", "AI", "Provenance", "Complexity"] --- # Ten Off the Shelf: What OpenAI actually released, read as a set **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.[^1] 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. ```figure:sheet?key=audit&placement=wide label: What I checked, and what I found head: What I checked | What I found row: Do the 46 arXiv citations across paper, walkthroughs and blog post resolve? | **All 46** verdict: pass row: Are the 22 in-text attributions accurate against the real abstracts? | **All 22** verdict: pass row: Do the 3 priority claims that predate arXiv hold up? | **All 3, corroborated independently** verdict: pass row: Are there soundness escape hatches in the Lean? | **None. Zero `native_decide`, zero custom axioms** verdict: pass row: Is every declared theorem present and proved? | **Yes, in every state I preserved, with no gaps** verdict: pass row: Was any claim ever weakened or retracted after publication? | **No. Every change I saw made it stronger** verdict: pass row: Does it overclaim on cryptography? | **No. It never names a cipher** verdict: pass row: Does it claim an Erdős prize? | **No, and it credits someone else for the one already solved** verdict: pass row: Did any of the ten require asking a new question? | **No** verdict: adverse row: Can a reader reconstruct how any of it was produced? | **No** verdict: adverse row: Does the released artifact still exist? | **No** verdict: adverse ``` 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. {.definition: Every one of the ten targets was posed by a named person, decades ago, and left on a shelf.} 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. ```figure:spans?key=shelf label: The shelf, and the day it was cleared from: 1960 to: 2032 now: 2026 span ehrhart: Which balanced body holds the most volume? at 1964: Ehrhart conjectures a simplex is the answer at 2026: closed, and the guess was right note: Measured from [Ehr64], the earliest citation Chapter 8 gives. The chapter never says how long the problem stood. span degeneracy: How dense can a graph get while avoiding a pattern? at 1967: Erdős poses the degeneracy question at 2026: disproved note: Chapter 10's older anchor, [Erd67]. Its other anchor is Erdős and Simonovits in 1982. span binary: How many codewords can differ in a fixed fraction of letters? at 1977: the second McEliece-Rodemich-Rumsey-Welch bound at 2026: beaten for all parameters note: Chapter 2's binary record. The anchor is MRRW-II. span kl: How densely can spheres fill high-dimensional space? at 1978: Kabatianskii and Levenshtein set the exponent at 2026: improved by 0.89 percent, and the method capped note: [KL78], cited by both Chapter 1 and Chapter 2. span connes: Do two groups with the same operator algebra have to match? at 1980: Connes poses rigidity at 2026: disproved note: [Con80] and [Con82]. The range 1980 to 1982 is the chapter's own citation spread. span compactness: Do density limits for forbidden patterns compose? at 1982: Erdős and Simonovits conjecture compactness at 2026: disproved, in its corrected form note: [ES82]. The original formulation already had counterexamples; this kills the repaired one. span ramsey: How fast does the k-color triangle Ramsey number grow? at 1983: Chung and Graham record Erdős's $250 and $100 offers at 2026: growth rate pinned, and still not finished note: [CG83], the chapter's own anchor for the question. This is the one bar whose problem is only partly closed. span permanent: How much harder than the determinant is the permanent? at 1985: Kalorkoti proves a cubic formula-size bound at 2026: improved note: [Kal85]. Nothing between 1985 and now claims a super-cubic bound. span cvp: How hard is finding the closest grid point, approximately? at 1998: Dinur, Kindler and Safra open the line at 2026: hardness from P not equal to NP alone note: [DKS98] through [DKRS03]. The chapter's earliest anchor is 1998. span sofic: Can every group be approximated by finite shuffles? at 1999: Gromov asks, Weiss names it soficity at 2026: no, and here is one that cannot note: [Gro99] and [Wei00]. Twenty-seven years, the shortest wait but one. span repetition: Does winning every copy of a hard game get exponentially unlikely? at 2004: Cleve, Høyer, Toner and Watrous note it open at 2026: yes, for all entangled games note: The one duration the paper effectively gives. Chapter 6 says "explicitly noted as open by 2004 [CHTW04, footnote 2]." mark 1964: the shelf starts mark 2026: the shelf is cleared note: Eleven bars for ten chapters, because Chapter 10 kills two separate conjectures. Sort by length and the range runs 22 to 62 years, with the median falling exactly on 44. Every duration here is my arithmetic from a citation, not a claim the paper makes. ``` {.trick: No chapter says how long its problem was open. The durations are my arithmetic from each chapter's earliest citation, and the figure shows the anchor beside every bar.} 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](claim:abstracts-suffice). 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. {.payoff: The results that improve a rate are numerically tiny. The results that kill a conjecture are absolute. Almost nothing in the coverage distinguished them.} 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. ```figure:tally?key=kinds label: What kind of result each one is axis x: what it settles from: improves a bound to: settles it outright axis y: how much of the answer is a number from: a headline number to: no number at all quadrant tr: settled, and unnumbered quadrant bl: a better bound, and a number to quote item ch1: Sphere packing, and a ceiling on the method x: 1 y: 1 tag: rate note: The exponent moves 0.59906 to 0.60440. It also proves no function of that type can ever do better, which is a result about the technique rather than the problem. item ch2: Codes, binary and spherical x: 1 y: 2 tag: rate note: Beats the 1977 and 1978 records at every parameter. The paper describes the work since as having "improved only lower-order factors," which is accurate, and a less careful write-up would have claimed no improvement since 1978. item ch5: The permanent x: 1 y: 0 tag: rate note: A gate lower bound that is negative until n is past 256. item ch6: Entangled parallel repetition x: 2 y: 3 tag: rate note: Decay rate epsilon to the thirteenth, for all games. Structural, and numerically out of reach. item ch7: Closest vector, approximately x: 2 y: 1 tag: rate note: Hardness to factor n to the 1/400, from P not equal to NP alone. item ch9: Multicolor Ramsey x: 3 y: 2 tag: rate note: Pins the growth rate at k to the theta of k. A factor-3 gap in the exponent-of-the-exponent survives, and the chapter says so. item ch3: A group that is not sofic x: 8 y: 9 tag: refutation note: Explicit, and the first one. Its consequences are carefully bounded by the chapter itself. item ch4: Connes rigidity is false x: 9 y: 9 tag: refutation note: The most field-central refutation in the release. item ch10: Two Erdős conjectures die x: 9 y: 6 tag: refutation note: Explicit finite graphs. Polynomial failure, not marginal. item ch8: Ehrhart's volume conjecture x: 10 y: 0 tag: exact note: Sharp, attained, and the only exact answer in the release. Also the only one that confirmed what was expected instead of breaking it. The chapter stops one step short of claiming the simplex is the only body that attains the bound. note: Switch to the table view and sort by either axis. The six rate improvements sit together and the three refutations sit together, and that is the taxonomy doing its job. ``` 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. ```figure:scale?key=vacuity label: The smallest problem on which Chapter 7's hardness reaches a factor of two value: 2^400 as: the number of grid dimensions needed before the proved approximation gap reaches 2 note: Chapter 7 proves hardness to a factor of n^(1/400). Setting that equal to 2 and solving gives n = 2^400. The theorem is about the limit; this is where the limit starts to mean something. ``` {.trick: An asymptotic bound is a statement about a limit. Asking where it starts to bite is a different question, and the paper never claims otherwise.} 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. ```figure:curves?key=bites label: Chapter 5's bound against the bound you get for free x: n axis x: matrix size axis y: gates required, lower bound from: 16 to: 1e12 curve free: n^2 as: what you get for free, since the circuit must read every entry note: any circuit computing the permanent of an n by n matrix has to look at all n² of its entries curve new: (n^2/144)*(log2(log2(n))-3) as: Chapter 5's bound emphasis: yes note: negative until n passes 256, and the theorem states its own threshold at n = 2^16 = 65,536 note: Drag the cursor. The two curves are the same shape; only the constant differs, and the log log term needs n past 2^(2^147) to make up 144-fold. The improvement is real and asymptotic, and the crossing is not on any axis that fits in this universe. ``` 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. {.payoff: Size and significance are close to uncorrelated across these ten. Every ranking the coverage produced was built on how big the claim sounded, which is the wrong axis.} 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. > **Interactive figure:** The ten results on two axes that disagree. ### 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. {.definition: Chapter 7 contains the proof that its own exciting headline is unavailable.} 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. {.payoff: Two chapters derive the same constant by routes that share no intermediate step, and Chapter 2 never prints the decimal, so the agreement is invisible unless you compute both.} 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. > **Interactive figure:** Two derivations that share no intermediate step, landing on one constant. 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. ```figure:hypothesis?key=posed id: machine-chose claim: The model picked which problems to work on. truth: Nothing in the release says who chose the ten. Every target is a named, published, decades-old question, and the selection is undisclosed. The only published OpenAI prompt for any mathematics result names its problem in the first line, so at least in that case a human handed the problem over. effect: The claim that nothing here required a new question survives, and it gets sharper. Choosing the problems is the step nobody has shown a machine doing. id: just-search claim: It was enumeration. The machine tried things until something worked. truth: Chapter 4 states its whole strategy in one sentence, and it is an idea rather than a sweep: "The crossed product remembers the Haar probability space and its K-action, but need not remember the compact group law on Â." It answers a question Sorin Popa posed and makes his countability bound sharp, and Popa is thanked in the acknowledgments. effect: Withdraw this and the section's thesis narrows correctly. The limit is about which questions get asked, not about the quality of the reasoning used to answer them. id: all-finished claim: All ten problems are now closed. truth: Chapter 9 proves k^((1/3−o(1))k) ≤ R_k(3) ≤ k^((1+o(1))k), which pins the growth rate at k^Θ(k) and leaves a factor of three in the exponent-of-the-exponent. The chapter says so plainly. effect: At least one of the ten advances is explicitly partial. The paper is clear about this and the coverage was not. id: first-of-kind claim: The mathematics itself is unprecedented in kind. truth: Ten weeks earlier the same lab disproved a 1946 Erdős conjecture, and the record of that one sits in the canonical database with a named attribution. This release is at least the fourth OpenAI mathematics announcement in nine months. effect: Removes "first" from every sentence in this notebook, correctly. What is new here is the count and the formalization, not the category. ``` 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? {.definition: The strongest claim in the release is one it never makes in prose. Every challenge file pins an explicit axiom allowlist, so a proof leaning on an unproved gap or on compiled code fails mechanically rather than by reviewer diligence.} 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](claim:textual-audit) 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. {.trick: A Lean proof is only as strong as its statement, and reading the statement is a separate skill from checking the proof.} **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](claim:no-independent-check). 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. ```figure:sheet?key=may-artifacts&placement=wide label: What the May result produced, within five hours head: Artifact | Submitted, UTC | What it was row: arXiv 2605.20579, Will Sawin | 20 May 2026, **00:37:35** | Made the exponent explicit, `n^1.014`, against OpenAI's inexplicit `ε ≈ 6.24 × 10⁻³⁸` row: arXiv 2605.20695, **nine authors** | 20 May 2026, **04:46:35** | "A short, digested, **human-verified** version of the recent OpenAI-generated counterexample" ``` 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. ```figure:sheet?key=scoreboard&placement=wide label: erdosproblems.com, checked 3 August 2026 head: Problem | Belongs to | Status | Page last edited align: center | left | left | left row: **#90** | the May 2026 result | **DISPROVED (LEAN)**, and the page names "an internal model at OpenAI" | **20 May 2026**, the same day row: #92 | fell as a corollary of #90 | DISPROVED | 21 May 2026 row: #146 | **this release**, Chapter 10 | OPEN | **18 January 2026** row: #180 | **this release**, Chapter 10 | OPEN | **18 January 2026** row: #183 | **this release**, Chapter 9 | OPEN | **10 April 2026** row: #575 | **this release**, Chapter 10 | OPEN | **18 January 2026** ``` {.payoff: The canonical record moved inside a day for the May result and has not been opened for this one. That measures digestion rather than quality.} 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. > **Interactive figure:** Ten results falling out at the layer where they stop. 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](claim:forks-faithful), 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. ```figure:tally?key=states label: What changed, and when anybody could have seen it axis x: hours after the repository was created from: 06:10 UTC to: 01:30 UTC next day axis y: how the state was recovered from: seen by polling to: recovered only from a fork item s01: The released artifact x: 0 y: 0 tag: released note: 842,760 lines, 40 declared theorems, 10 of 12 challenges enabled for the independent kernel check. item s02: Statement strengthened x: 3.9 y: 0 tag: upward note: The Connes rigidity challenge is replaced. 41 declared theorems. The loophole in the released statement is closed. The tree is also restructured in this window, from 4,319 Lean files down to 23, holding 545,947 lines. item s03: Independent checking completed x: 5.2 y: 8 tag: upward note: 11:21:53. A three-line change turns on the two challenges that were not being re-checked by a second kernel. 12 of 12 from here on, and nothing announces it. item s04: A real commit, with a parent x: 5.6 y: 8 tag: history note: 11:46:12. Message: "Remove unused Connes rigidity proof declarations." 14,989 deletions, 378 insertions, no claim touched. This state had a history for 24 minutes. item s05: Consolidation x: 10 y: 4 tag: upward note: Between 15:57 and 17:11 the declared theorem count falls from 41 to 38, and the count of unproved gaps in the statement files falls from 45 to 42 in the same move. item s06: Build defect repaired x: 17.3 y: 0 tag: upward note: 23:29. A manifest had declared thirteen challenge roots against twelve files since release, so the project did not build as declared for seventeen hours. Fixed silently. note: Sort by the vertical axis. Five of the fourteen states were never visible to anyone watching the repository directly. ``` {.trick: Every observed change made the artifact better. The count fell because three claims and three unproved gaps left together, which is the artifact getting smaller by getting more honest.} 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.[^2] 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. ```figure:unfold?key=prompt label: What the human actually wrote step: Two pages of instructions, for a different result, containing no mathematics at all. step: "Use multiagent v2 aggressively and dynamically. You have up to 64 concurrent agents available. Do not use a fixed assignment such as 'N agents for strategy X.'" step: The visible human contribution is search-portfolio management. Keep approach families independent, maintain a registry, do not let an elegant reduction dominate the pool. step: "Spend at least 8 hours on this before even thinking of returning or giving up." step: Sixty-four agents times eight hours is the shape of the compute being purchased. It is also the denominator the cost figure is missing. step: "Return only when a complete affirmative proof has been found and survives adversarial audit." step: The adversarial specification is unusually concrete, naming failure modes to hunt: "repeated-edge closed trails masquerading as cycles, parallel-edge 2-cycles, circular use of an equivalent CDC statement." step: "Assume for purposes of this task that a complete affirmative proof exists." step: This one cannot have been used across the ten. Chapters 3, 4 and 10 produce counterexamples, so whatever ran on those had to be free to conclude the conjecture was false. Whatever "the same method" means, it is not uniform. step: There is no mathematics anywhere in the document. Not a definition, not a lemma, not a hint about where to look. ``` Then there is the `$2,000`, which was the most repeated number in the coverage and is the easiest one to misuse. At published Sol rates of five dollars per million input tokens and thirty per million output, two thousand dollars buys **66.7 million tokens** on the most conservative assumption, or about 6.7 million per problem. The paper itself is roughly 164 thousand tokens. So on that assumption the search consumed something like **four hundred times the tokens of the document it produced**. That ratio is mine, not OpenAI's. {.aside: The cost figure is a numerator. The denominator, how many attempts each success took, is not disclosed anywhere.} But attempts per problem, failure rate and harness cost are all undisclosed. The $2,000 is a numerator with an undisclosed denominator. Whether it represents one attempt per problem or a thousand changes what it means by three orders of magnitude, and nothing published answers that. Put those pieces beside each other and the shape of the gap is clear. The model is named as something that does not appear in the company's own public record, in an internal version nobody outside can run, driven by a harness that is described only in a document about a different problem, at a cost whose denominator is missing, with no human named at any step. Every individual omission is defensible. Labs do not publish frontier model details, and nobody owes the public their prompt library. The aggregate is that the single most-cited fact about this release, that it cost two thousand dollars, is the only quantitative claim about the process anybody outside the company can repeat, and it cannot be checked. Hold that next to the previous section instead of as a separate complaint. **The mathematics is the most checkable object in the release and the process is the least.** The proofs come with 842,760 lines of Lean and an axiom allowlist. The method comes with a model name that returns one false positive in a search of the company's own newsroom. Those are not the same standard of disclosure, and the gap between them is not accidental: the results are the thing being offered and the method is the thing being kept. ## Credit and responsibility come apart On 2 June 2026, three thousand three hundred and five mathematicians signed the Leiden Declaration on AI and Mathematics, which the International Mathematical Union endorsed. The signatories include Terence Tao, Peter Scholze, Kevin Buzzard and Jeremy Avigad. Its relevant clause binds two things together in one sentence: "Credit **and** responsibility continue to belong to humans within the mathematical community and should not be given to automated systems." This release separates them. Credit goes to the system, in the form of an author line reading `OpenAI` with no human named. Responsibility goes to the company: "we take responsibility for their correctness." ```figure:tally?key=credit label: Who is credited, against who is responsible axis x: who is credited from: named humans to: the system axis y: who answers when it is wrong from: named humans to: the machine quadrant bl: both to people, which is the Leiden position quadrant br: credit to the machine, and people still answer for it item leiden: The Leiden Declaration x: 0 y: 0 tag: norm note: 3,305 signatories, IMU-endorsed. Binds credit and responsibility in a single clause and puts both on humans. item openai: This release x: 10 y: 5 tag: artifact note: Sole author OpenAI, no human named. Responsibility explicitly claimed by the company for correctness of the formal statements. item feige: pengzhang91/Feige x: 6 y: 0 tag: artifact note: Lists the model as a co-author in CITATION.cff while the human authors hold responsibility. A third position, held as policy by nobody. note: The whole top half of this grid is empty, and that emptiness is the point. The company sits mid-scale because an institution is not a person and is not a machine. Nothing here puts the machine on the vertical axis at all. ``` I want to quote OpenAI's own reasoning rather than paraphrase it, because the usual summary of "OpenAI rejects Leiden" is too coarse and the actual argument is more considered than that: "claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of genuine human intellectual work." The disagreement is real and it is principled on both sides. Leiden's position is that authorship is a social institution and giving it to a system corrodes what it is for. OpenAI's position is that pretending a human wrote this would be a lie about a document. Both of those are true statements, which is why the question is hard. The practical test is what happens when something turns out to be wrong. Under Leiden, a named person answers for it, and the mechanism is old and effective: reputations are durable, they are individually held, and a mathematician who signs a bad proof carries it. Under this release, a company answers for it. That is not nothing, though it is not the same thing either. Companies restructure, policies change, and no single person's standing is on the line. The clause in the declaration that binds credit and responsibility together is not decorative. It is the load-bearing part, because the reason credit works as an incentive is that responsibility is attached to it. Notice which half of that grid nobody occupies. Across all three positions, credit moves freely: the machine can be an author, a co-author, or nothing at all. Responsibility never moves. Everybody agrees a system cannot be answerable, and the whole disagreement is about whether it can be an author while somebody else is answerable. That is a narrower question than the coverage made it look, and the one worth watching. It is also going to be settled soon, empirically rather than by argument. The declaration was eight weeks old when this release landed. It has 3,305 signatories and an IMU endorsement, and it now has a high-profile artifact that honors half of it and declines the other half. Whether a norm like that holds is not a thing anybody can reason out in advance. You find out by watching what journals, arXiv moderators and hiring committees actually do, and the next year is the experiment. ## The bottleneck moved, and the shelf is finite On 13 May 2026, Terence Tao changed his personal policy on reading other people's proofs. He had been doing it because such proofs were "rare and valuable, compared to the time available to voluntarily review and explain them." His conclusion: "this is now changing… to the point where **this is no longer the bottleneck to mathematical progress.**" He named five conditions under which he would still put review first. Two of them land directly on this release: results that "have been carefully formalized in a proof assistant," and results that "exhibit exceptionally thorough efforts by the authors at digesting and presenting the proof." This release maps onto both. It has 842,760 lines of Lean and a 62-page companion document reconstructing how each proof came together, including the dead ends. Ten problems, in ten areas, most of which are nothing to do with his own work. He has not replied. His most recent post as of this writing predates the announcement by four days. ```figure:curves?key=digestion label: The two rates, and the gap between them x: t axis x: years from 2024 axis y: results per year, schematically from: 0 to: 6 curve produced: 3*2^t as: machine-generated results offered for review emphasis: yes note: schematic. The shape is the claim, not the values: this is the quantity that stopped being scarce. curve read: 3+2*t as: expert-hours available to digest them note: schematic, and generous. The number of people who can referee a result in operator algebras does not double. note: Both curves are illustrations rather than measurements, and the point is only their shapes. Nothing in this notebook depends on the numbers. ``` The two curves in that figure are schematic and I want to be blunt about it: they are shapes, not measurements. What is not schematic is the comparison from the last section. **The May result was digested by nine of the field's best inside a day. This release, with ten times the results and far more formalization, has not been digested at all.** Same lab, ten weeks apart, opposite reception, and quality does not explain the difference. {.payoff: Producing proofs got cheap. Choosing what is worth proving and digesting what has been proved did not, and neither of those is what this release automated.} Which brings me to the thing I actually think about this, and it is not about verification at all. Look back at the shelf figure. Ten questions, accumulated over sixty-two years of human attention, each one posed by somebody who thought it was worth posing, and all ten were taken down in a single document on a single day. That shelf is finite. It took six decades to build and one release to clear ten items off it, and **nobody's job was to pose the eleventh.** If producing proofs is no longer the scarce thing, then two other things become scarce, and they sit on either side of the part that got automated. Choosing what is worth proving. Digesting what has been proved. This release automated neither, and the evidence for that is the release itself, sitting undigested in a canonical record that has not been edited since April. I do not think that stays true, and I want to say which way I expect it to break so it can be wrong in public. The digestion side looks like the easier of the two, because it is a reading problem and reading is closer to what these systems already do than proving was. Something that produces a faithful, checkable exposition of a proof it did not write is a smaller ask than what this release already did. The choosing side looks much harder, and not for a technical reason: it is hard because "worth proving" is a judgment about what a field should care about next, made by people with careers and taste and a sense of where the interesting ground is. Erdős was not running a search. He was deciding what would be interesting if it were true. So the forward-looking claim is narrow. The shelf of well-posed, long-open, individually-stated problems is a finite inheritance, built by people who were doing something other than answering questions. Ten came off it in one release for about two thousand dollars. At that price the shelf empties, and what happens next depends on whether the rate of posing keeps up with the rate of answering. Nothing in this release bears on that, and that is why it is the thing to watch. ## Ten acts of reading Ten problems came off a shelf that took sixty-two years to build. Six moved by a hair and four ended outright. The mathematics held up under every check I could apply to it: the citations resolve, the attributions are accurate, the priority claims survive independent corroboration, the formal proofs use three standard axioms and no escape hatches, and two chapters accidentally verified each other by deriving the same constant along disjoint paths. And the one thing nobody automated is the reading. You have already seen what that looks like when it goes right. On 20 May 2026, nine mathematicians read one machine-generated disproof and had a human-verified digest on arXiv the same morning. That is the standard. Ten results across ten fields is ten times the reading, and as of this writing nobody has done it. That is not a complaint about the field. It is an accurate description of the work sitting in front of it, and it is the whole reason this section exists. And the release asked for exactly this. The blog post's closing sentence is a request: OpenAI hopes the mathematical community will "engage deeply with these results, place them in context." That is a request for digestion, published eleven weeks after Tao named digestion as the thing that had stopped keeping up. Two days on, the four database entries that would register an answer have not been touched. So the honest response to ten machine-generated proofs is ten acts of human reading. That is what the ten notebooks below are. I should say plainly that this section is *a* reading rather than *the* reading, and that a person who actually works in operator algebras will get further into Chapter 4 in an afternoon than I will get in a month. What they are is a demonstration that the reading is available. Every finding in this notebook came out of the paper, the repository and twenty-two cited sources, using arithmetic and attention and nothing else. The two chapters that agree on a constant, the bound that is negative below 256, the chapter that declines its own headline, the problem that is still open, the four database entries that nobody has touched: none of that needed access, credentials or a graduate degree. It needed somebody to sit down with it. That is a low bar and it has largely not been cleared, and the gap between how checkable this release is and how little of it has been checked is the most interesting fact about it. Each notebook below takes one chapter and does the same thing at closer range: what was actually asked, what was actually proved, what the number actually means, and what the chapter itself declines to claim. ```figure:tally?key=arc label: The ten, in the order I would read them axis x: how much background it assumes from: none to: a graduate course axis y: how much of the question it closes from: moves a rate to: finishes it item balanced-body: The balanced body x: 1 y: 10 tag: chapter 8 note: Which shape balancing on one lattice point holds the most volume. The most approachable result in the release, the longest-standing question, and the only exact answer. Start here. item parity-switch: The parity switch x: 3 y: 9 tag: chapter 10 note: Two Erdős conjectures die by a parity argument you can operate by hand. Even q kills one family, odd q the other, and no q kills both. item party-problem: The party problem x: 3 y: 6 tag: chapter 9 note: Multicolor Ramsey. The most famously explainable object in the set, and the one result here that is explicitly unfinished. item code-and-ball: The code and the ball x: 5 y: 4 tag: chapter 2 note: Error-correcting codes and Hamming balls. Comes before the sphere packing notebook because it builds the machinery that one needs. item spheres: How close can spheres get x: 7 y: 5 tag: chapter 1 note: The 0.89 percent that closes a method, and the second half of the accidental replication. item permanent: The permanent x: 6 y: 3 tag: chapter 5 note: The determinant's near-identical twin, and why it is so much harder. Lead with formula size, not circuits. item games: Games machines cannot win x: 8 y: 4 tag: chapter 6 note: Playing a losing game many times at once, with entanglement allowed. item encryption: This does not break your encryption x: 6 y: 5 tag: chapter 7 note: The strongest anti-hype piece in the arc, and the chapter that proves its own headline unavailable. item sofic: The sofic question x: 9 y: 8 tag: chapter 3 note: Can every group be imitated by finite shuffles? No. The hardest exposition in the arc and possibly the best human story in the release. item connes: Connes x: 10 y: 9 tag: chapter 4 note: The most famous conjecture in the set, disproved, with the best toy model in the release. Four points, two group laws. note: Sort by the horizontal axis for the gentlest path through, or by the vertical one to read the results that actually finished something first. ``` ## What this rests on Four assumptions are doing load-bearing work above, and not one of them is a fact I checked. Withdraw any of them and watch which sentences in this notebook stop standing up. ```figure:hypothesis?key=rests id: forks-faithful claim: A repository state recovered from somebody else's fork is a faithful copy of what upstream published. truth: Git object hashes make substitution detectable, and the recovered trees are internally consistent. But I did not receive them from OpenAI, and five of the fourteen states exist for me only because a stranger happened to fork at the right minute. effect: Withdraw this and every count in the artifact section becomes unsupported, including the claim that nothing was ever weakened. id: textual-audit claim: Scanning Lean source for unproved gaps and escape hatches tells you what building it would tell you. truth: It does not. I have never run lake build on this repository, because I do not have the toolchain here. Every statement I make about the formalization is textual. effect: Withdraw this and the axiom allowlist finding weakens from "verified" to "declared," which is a real difference and the one the verification section turns on. id: abstracts-suffice claim: Checking an attribution against a paper's abstract is enough to say the attribution is accurate. truth: For the 22 claims I checked it was enough to catch a mismatch, and it would not catch a subtle misreading of a result whose abstract is vague. effect: The 22 of 22 figure becomes weaker evidence than it sounds, though it stays strong evidence against the fabrication failure mode it was designed to test. id: no-independent-check claim: Nobody outside OpenAI has verified any of the ten results. truth: No such verification is public, and four topical arXiv searches turned up nothing. One second-hand report says a domain expert was shown a preprint before publication, which I could not confirm and am not repeating as fact. effect: Withdraw this and the entire digestion argument softens, because private verification would mean the reading is happening where I cannot see it. ``` --- [^1]: OpenAI, *Ten advances in mathematics and theoretical computer science*, 1 August 2026. The paper is 249 pages, its author line reads `OpenAI`, and the accompanying blog post is where the model, the cost figure and the responsibility claim appear. The paper itself contains none of them. [^2]: The states are preserved at [`chcaru/ten-proofs-archive`](https://github.com/chcaru/ten-proofs-archive), which tags every observed upstream state and records the ones recovered from third-party forks. Upstream's current head has been `94bc0feb6` since the evening of 1 August, unchanged through the most recent poll on 3 August at 05:11 UTC.