On 6 October 2026 OpenAI published 722 mathematics manuscripts written by one of its AI models, grouped into 372 families of results. No human referee had checked them. Within a week, people working with their own AI agents had tightened the numbers in several. Here is the whole collection, the seven families our founding members built on, and how much room the first proofs left.
How to read: each bar counts the manuscripts whose folder carries that date. Below the line, each dot is one public step that improved one of six results after the collection went public, stacked by day. A half-gold, half-cyan dot is a person working with AI agents; the one all-cyan dot is OpenAI’s own follow-up. Point at a day, or focus the chart and use the arrow keys.
717 of the 722 manuscripts are dated between 22 September and 5 October.
Manuscripts written by OpenAI’s model, by folder date
A library of mathematics, written by one model, posted in one commit.
A manuscript here is a draft research paper: a claim and its proof, written out in full. OpenAI grouped its manuscripts into families, one per main result, so a family can hold a paper and the papers that build on it.
The repository says the manuscripts and their proof files were “produced by an internal OpenAI model”, and it is plain about the risk: “Some of the unformalized results could have issues.” The first commit is signed “Anonymous” and dated 6 October 2026, 14:58 Pacific time. The folder dates show how fast the writing went: 717 of the 722 manuscripts are dated between 22 September and 5 October.
What a Lean scope document is
Lean is a proof checker: a program that accepts a proof only if every step follows from the rules, taking nothing on trust. For 235 of the 372 families, OpenAI linked a scope document, a plan saying which statements in that family are to be checked in Lean. A plan is not a finished check. And a Lean proof confirms only the statement it was given; whether that statement says what the paper says is a separate question. OpenAI’s own catalogue marks its formal proofs as made by agents and not yet reviewed.
The next day, 7 October, OpenAI withdrew three manuscripts because “a sign error invalidates a stabilization-trace cancellation argument”, revised fourteen others and added formal proofs. By its own count, 300 of 719 top-line results, about 42%, were then formalized.
01//The map
Fields: OpenAI’s 17 subjects, folded into 8
All 372 families on one page.
Each cell is one family, and its area is how many manuscripts it holds. Filled cells link a Lean scope document; outlined cells do not. A red ring marks the seven families our founding members built on. OpenAI’s own overview groups the families into 17 subjects; the map folds those into 8 broader fields, and 15 families, most of them from OpenAI’s “Mathematical physics”, sit where their titles put them instead. Point at a cell to see OpenAI’s subject.
OpenAI’s 372 result families, grouped by field
How to read: big cells hold many manuscripts; the largest, family 034, holds 14. Point at a cell for its title, counts and dates, or focus the map and use the arrow keys: left and right step through families, up and down jump between fields, Enter opens the entry for a ringed family. Type in the search box to light up matching titles.
Ctrl //
Size
Snapshot
Point at a cell, or focus the map and use the arrow keys.
Ringed: the seven families our founding members built on, 107, 109, 111, 130, 160, 161 and 167.
Filled · links a Lean scope document (a plan, not a finished check)
Founding members Doug Colkitt, rohanarun, eumemic and Ryan Shea took seven of the 372 families further. Swapnil Jain, with a check from Aska, carried one of them (family 130) into arithmetic on bits. Others joined every effort and are named below where the record names them.
Since 2019, two n-digit numbers can be multiplied in about n·log n steps; back in 1971 Schönhage and Strassen had guessed that nothing could do better. OpenAI’s manuscript claims a sliver less on the simplest model of a computer, a multitape Turing machine: n·(log n)1−κ steps with κ = 2−182. A bigger κ is a bigger saving.
κ on a halvings scale, 7 to 13 October 2026
κ on a halvings scale, from the manuscript’s 2−182 to 0.001672660197076918 ≈ 2−9.22 in 25 public steps, 7–13 Oct. Every point rests on the unreviewed manuscript.
Before → afterκ: 2−182 → 0.001672660197076918 ≈ 2−9.22the maintainer-reviewed record on 13 Oct, about 1052 times larger
Doug Colkitt, founding member: opened the public race on 7 Oct and maintains it, reviewing and selecting each record.
rohanarun, founding member: its most active contributor, with 142 pull requests, and holder of the current reviewed record, PR #1094.
eumemic, founding member: 80 pull requests; on 13 Oct the record’s bit supplier still built on their PR #555.
Aska Digital: built the live race tracker that grew into this site, and submitted two small claims (PRs #464, #469) that were never reviewed and were soon overtaken.
Many others: 1,334 pull requests had been opened by 13 Oct.
2 manuscripts, dated 25 Sep 2026 · Lean scope document (for the finite circuit result only)
The discrete Fourier transform splits a list of numbers into its frequencies, the way an ear splits a chord into notes; the fast Fourier transform does it in about n·log n steps. OpenAI’s manuscript claims an exact method, with no rounding, in n·(log n)1−δ steps with δ = 10−13.
δ on a log scale
δ on a log scale: 10−13 in the manuscript, then 9 public steps to 0.0012331685 on 12 Oct, about 1.2×1010 times larger.
Before → afterδ: 10−13 → 0.0012331685checked in Lean on 12 Oct, about 12 billion times larger
Ryan Shea, founding member, with Jeremy Kothe, whose circuit it uses: δ = 0.0012331685, rebuilt from source and checked in Lean by the Big O Speedrun leaderboard, which ranks it first and credits both. By their own account, Ryan Shea’s part was converting the circuit and checking this instance of it; the Lean engine is Jacob Sussman’s, and one extension came from Nil Mamano.
eumemic, founding member: claimed δ = 607/1,250,000 ≈ 0.00049 on 9 Oct, with an exact certificate but no formal proof. It was the best claim for about six hours.
Swapnil Jain: mobius-x1 carries the same construction into arithmetic on bits, for the Möbius transform over GF(2). Aska wrote and ran the full-network check behind its Theorem 2 (merged PR #1).
Colour the numbers 1, 2, 3, … with r colours. If the row is long enough, one colour must hold k evenly spaced numbers, like 4, 9, 14, 19. The van der Waerden number is the shortest row that forces this. OpenAI’s manuscript claims to prove it is longer than kc·k·⌊log2r⌋ with c = 1/100000.
Colour the numbers: the smallest case
The smallest case, 2 colours and runs of 3: the numbers 1 to 8 can be coloured with no one-colour evenly spaced triple, but 1 to 9 cannot, so the van der Waerden number W(3;2) is 9. Below, the manuscript’s constant c on a log scale, 1/100000 → 1/9.
Before → afterc: 1/100000 → 1/9about 11,111 times larger, conditional on the manuscript
rohanarun, founding member, with Codex and Claude, started the repository on 9 Oct: c = 1/200, then 1/193, then 1/25, and a proof that this line of attack cannot pass 1/24.
artuskg, with GPT-6 Pro and Codex: 1/19, from a new construction.
DaysSky, with Claude: 1/16, then 2/25, then 1/9.
A partial Lean check of 84 statements, by rohanarun, is open for review (PR #10).
A graph is a network of dots and lines. Sidorenko’s conjecture predicted that every two-sided pattern (a bipartite graph) appears in any network at least as often as in a random network with the same number of lines. OpenAI’s manuscript claims a counterexample: a pattern on 35 dots.
The counting constant, step by step
The counting constant, step by step: 1641 in the manuscript, then 1032 and 978 on 9 Oct and 189 on 10 Oct.
Before → afterone counting constant: 1641 → 189and no smaller certificate than 35 dots inside the manuscript’s own template
rohanarun, founding member, with Codex and Claude: enumerated every candidate shape up to 12 points, killed each with an exact certificate, and found nothing smaller inside the template. Then cut the constant in one counting step from 1641 to 1032, 978 and finally 189.
The minimum holds only inside that template, not for every possible counterexample.
Scatter n points on a flat plane. How many pairs can be exactly one unit apart? OpenAI’s manuscript claims a power saving: a provably smaller maximum than the best bound before it. Its last algebra step needs a 20×5 grid: 100 selected pairs.
The last step’s grid, before and after
The last step’s grid: 20 × 5 = 100 selected pairs in the manuscript, 8 × 4 = 32 after the refinement. The unit-distance bound itself does not change.
Before → afterfinal grid: 20×5 = 100 → 8×4 = 32 pairsa simpler last step; the unit-distance bound itself does not change
rohanarun, founding member, with Codex and Claude: a 9×4 grid on 9 Oct, then 8×4 on 10 Oct, and smaller grids still when a curve in the argument is a straight line.
3 manuscripts, dated 24 Sep to 2 Oct 2026 · Lean scope document
Multiplying two n×n tables of numbers (matrices) the school way takes n3 multiplications. OpenAI’s manuscripts claim about n9/4 = n2.25 are enough.
The exponent of matrix multiplication
The exponent ω of matrix multiplication: 3 for the school method; 2.807 (Strassen, 1969); 2.371177, the best published bound before October 2026 (Dupont and others, with AlphaEvolve, August 2026); OpenAI’s claimed 9/4 = 2.25; and 2, below which no method can go, since every entry has to be read. rohanarun’s work marks where one step of the 9/4 method stops: a limit on the method, not a new bound.
What changeda limit, not a new boundone step of the method cannot go further on its own, and one lemma’s constant, 3/(2Γ(4/3)) ≈ 1.67977, is already the best possible
rohanarun, founding member, with Codex and Claude: built an explicit example that meets every constraint that step keeps, yet grows only like a4/3.
A limit on one proof method: not a new algorithm, and not a proof that 9/4 is the best exponent.
Items arrive one at a time, in an order chosen by an opponent who knows everything. You keep or drop each on the spot, may keep only sets that a fixed rule allows (a matroid, such as “at most k items”), and know just one earlier sample of each item’s value. OpenAI’s manuscript claims to prove that a strategy always earns a fixed fraction of the best possible total.
The guaranteed fraction on a log scale
The guaranteed fraction on a log scale: 2−293 from the manuscript’s own derivation, then six versions to (35/32)·2−31 ≈ 5.1×10−10, about 8×1078 times larger and still below one in a billion.
Before → afterfraction: 2−293 → more than (35/32)·2−31 ≈ 5.1×10−102−293 is what the manuscript’s own derivation gives; its headline says 2−310
Ryan Shea, founding member, with Codex: six versions in two days, from 2−36 on 10 Oct to (35/32)·2−31 on 11 Oct, each with exact certificates.
Written proof + exact certificatesNot reviewedNot formalized
A first proof only has to work. To keep it short, its author picks safe, loose numbers wherever the argument allows, much as a first route to a new place takes the roads you already know. That looseness is slack. Tightening it rarely needs a new idea at first, just patience, and people with AI agents have patience to spare.
The numbers here span a huge range, from 2−293, a decimal point followed by 88 zeros, up to 1641. So the chart uses a log scale: each step along the axis multiplies the value by ten, so the length of a line counts how many times over the value changed.
Four of the six numbers are better when bigger: a bigger saving, a bigger guaranteed fraction. Two are better when smaller: a smaller constant, a smaller grid. Their lines run leftward, from the hollow circle to the filled one.
How far six numbers moved, 6 to 14 October 2026
How to read: the hollow circle is the number in OpenAI’s manuscript; the filled circle is the best public value by the date on the slider, and the line between them is the slack people found. Drag the slider or press play to watch the week happen. Choose a row to see its own steps, on its own scale, below. In “times better” view every line starts at ×1.
Ctrl //
Before · OpenAI’s manuscript
After · best public value by that date
Sources: each row’s repository history and pull requests; the Fourier steps from the Big O Speedrun leaderboard (read 14 Oct, Pacific times converted to UTC); the κ records from certificates/selected-result.json history. Snapshot to 14 Oct 2026.Show every step
04//What “conditional” means
Read before you cite
Most of this stands on a foundation nobody has checked.
A conditional result says: if that earlier result is true, then this one is too. Here the earlier result is a machine-written preprint. A careful refinement of a flawed proof is still a refinement of a flawed proof.
Every number in section 03 began in an OpenAI manuscript that no human referee has checked. The people who improved them say so in their own repositories: “conditional”, “not peer reviewed”, “no human review”. What they checked, they checked exactly: certificates in exact arithmetic, every case of a finite search, every input of a circuit. Those checks confirm their own step. They cannot confirm the manuscript underneath.
A proof checked end to end in Lean is different. The Fourier record was rebuilt from source by an outside leaderboard and accepted by Lean’s kernel against that leaderboard’s exact statement of the problem, so it does not lean on OpenAI’s prose at all. What remains open is whether that formal statement says exactly what we mean in words, which is why human review is still listed as pending.
This is not a hypothetical worry. On 7 October, one day after release, OpenAI withdrew three manuscripts in family 032: a sign error broke one argument, and two papers that depended on it went too. The family shrank from eight manuscripts to five.
“For centuries, finding a proof was the hard part and checking it was routine. That ratio inverted on October 6.”
How to read: each row is one refinement, standing on the OpenAI manuscript beneath it. Press the button to suppose that manuscript had a gap, and see what each result would still have. Press again to put it back.
Ctrl //
OpenAI #109 · unreviewedκ = 0.00167 integer multiplicationStated as conditional on the manuscript’s framework: it would lose its footing.
OpenAI #130 · unreviewed · not needed by the Lean proofδ = 0.00123 exact Fourier transformProved end to end in Lean: still proved, if the formal statement is the right one.
OpenAI #160 · unreviewedc = 1/9 van der WaerdenImports the manuscript’s lemmas: it would lose its footing.
OpenAI #111 · unreviewed(35/32)·2−31 matroid prophetRefines the manuscript’s construction with its own unreviewed written proof: it would need checking again.
OpenAI #161 · unreviewed1641 → 189 SidorenkoThe finite search over shapes stands on its own; the 189 is one step inside the manuscript’s proof and would fall with it.
OpenAI #167 · unreviewed20×5 → 8×4 unit distancesStated as conditional on the manuscript’s lemmas: it would lose its footing.
All six stand today. Five of them stand only as long as the OpenAI manuscripts beneath them hold; the Lean-checked Fourier record does not depend on its manuscript.
Each row’s wording follows its own repository’s statement of scope; see the entries in section 02.
05//Sources
Pinned commits where we have them
Where every number comes from.
OpenAI, openai/math, Apache-2.0. First commit adc7f12 (6 Oct 2026: 722 manuscripts, 372 families); update fd4aeeb (7 Oct: 719 manuscripts); history.md for the withdrawals.