The OpenAI math results are too numerous to read in a day, so readers have been triaging them by which ones look like they matter. Eight keep coming up: the Unique Games Conjecture, a zero-free half-plane for the Riemann zeta function plus no Landau-Siegel zeros, integer multiplication and the Fourier transform below n log n, a matrix multiplication exponent of at most 9/4, Barnette's conjecture, the five-coloring of the plane, and three-machine scheduling. By the repo's own CONTENTS.md, seven of the eight link to a Lean formalization. Integer multiplication does not. Nothing we found says any of them has been refereed.
Our first post on the release covered what is in the repository. This one is the second look: what each headline result says in plain English, what its Lean entry actually claims to prove, and how mathematicians and developers reacted in the Hacker News thread, which had about 600 points and 540 comments when we read it.
TL;DR: the questions people are asking
| Question | Short answer |
|---|---|
| Which results do experts single out? | Quasi-Riemann and Landau-Siegel (number theorists), Unique Games (complexity theorists), the sub n log n algorithms (commenters called them surprising). OpenAI ranks nothing |
| Which of the eight have a Lean entry? | Seven per CONTENTS.md. Integer multiplication below n log n is the exception |
| Does a Lean entry mean the whole manuscript is checked? | Not always. The Fourier transform entry covers a weaker statement than the manuscript, and the quasi-Riemann entry excludes later applications |
| Did we compile the Lean code? | No. Everything below about Lean is from the repo's docs, challenge files and catalogue |
| Does any of this change code I ship? | No. The algorithm results are asymptotic with astronomical constants |
| What is the loudest skepticism? | Nobody has reviewed this much mathematics, and a Lean theorem only helps if it states the right thing |
The eight results at a glance
Every row below is checked against CONTENTS.md, the matching lean/docs/NNN.md file and the preprint's own abstract. "Lean entry" means the repo lists a formalization. It does not mean we ran it.
| Result (family) | One-line claim | Lean entry in the repo | Scope note |
|---|---|---|---|
| Quasi-Riemann hypothesis, Landau-Siegel zeros (003) | No zeta zeros with real part above 7/8; no exceptional real zeros | Yes | Later applications excluded; constant c not explicit |
| Unique Games Conjecture (102) | NP-hardness gap for unique games | Yes | Gap reduction from binary 3SAT |
| Integer multiplication (109) | n-bit product in time n times log n to the power 1 minus kappa | No | Single preprint, kappa is 2 to the minus 182 |
| Fourier transform (130) | Exact DFT below n log n | Yes | Lean states a weaker, subsequential result |
| Matrix multiplication (107) | Exponent omega at most 9/4 over the complex numbers | Yes | Arithmetic complexity only |
| Barnette's conjecture (180) | Every such graph has a Hamiltonian cycle | Listed | Not in the machine-readable catalogue |
| Five-coloring of the plane (158) | Five colors cannot work, so the answer is 6 or 7 | Yes | Also formalizes the classical 7-coloring |
| Three-machine scheduling (124) | Polynomial-time optimal schedule | Listed | Exponent 150020; not in the catalogue |
Read the table as three tiers of evidence:
- Checked by us: only what the repo itself says. We read the README, CONTENTS.md, the Lean docs and the preprint abstracts, and we read one Lean challenge statement (Barnette). We compiled nothing.
- Lean entry listed: seven results. For two of them (Fourier transform, quasi-Riemann) the Lean statement is narrower than the headline, and for two (Barnette, scheduling) the machine-readable catalogue does not list the formalization.
- Preprint claim only: integer multiplication below n log n. Every one of the eight is also unrefereed as far as we can tell.
The eight results in plain English
OpenAI's overview says its entry numbers "do not indicate a ranking", so the order below is ours: the two results the thread treated as most consequential first, then the algorithms, then the combinatorics.
Quasi-Riemann hypothesis and Landau-Siegel zeros (family 003)
The Riemann hypothesis says every non-trivial zero of the zeta function has real part exactly 1/2, and it controls how evenly primes are spread. What has been provable is much weaker: the standard zero-free region narrows toward the line with real part 1 as you climb higher. The Landau-Siegel manuscript describes that classical region and notes it excludes zeros "except for a possible simple real zero" tied to a real character.
The quasi-Riemann hypothesis asks for something in between: a fixed zero-free half-plane, with real part above some constant below 1. OpenAI's manuscript, dated September 30, claims 7/8 for zeta, for every Dirichlet L-function, and for finite-order Hecke L-functions over the field generated by the square root of minus 3. An alternate proof dated October 5 claims 11/12. A second, short manuscript dated October 1 claims a uniform exclusion of Landau-Siegel zeros: a constant c such that every real zero beta of a primitive real character of conductor q satisfies (1 minus beta) times log q at least c. Before this, the manuscript says, Page's theorem left at most one exception below any bound, and Siegel's 1935 estimate has an ineffective constant.
Lean: yes. The doc lists four challenge files (zeta 7/8, Dirichlet 7/8, Hecke 7/8, Siegel zeros). Its scope paragraph says the paper's later applications are not included, that no explicit value of c is given, and that real zeros elsewhere in the interval from 0 to 1 are not ruled out. The 11/12 alternate proof is not among the papers it lists. Remember that 7/8 is not the Riemann hypothesis: that would be 1/2.
Unique Games Conjecture (family 102)
Picture a network where each link carries a rule: if my label is x, yours must be pi(x), where pi is a one-to-one relabeling. The manuscript's own opening line is that "a permutation constraint prescribes exactly one label at one endpoint for each label at the other." The conjecture, due to Khot, says that even when a labeling satisfying almost every rule exists, finding one that satisfies more than a sliver is NP-hard.
OpenAI's September 23 manuscript claims, for every fixed epsilon and delta below 1/2, a deterministic polynomial-time reduction from 3SAT to unique games where satisfiable formulas give value at least 1 minus epsilon and unsatisfiable ones give value at most delta. enoether noted why that matters: the conjecture is an assumption underneath many inapproximability results. The same family also claims direct NP-hardness proofs for Max-Cut beyond the Goemans-Williamson ratio, Vertex Cover below factor two, Min-UnCut and directed feedback vertex set, which CONTENTS.md says use established PCP and Label Cover hardness results.
Lean: yes. The doc formalizes the gap reduction from binary 3SAT (with translation constraints over a fixed binary alphabet) and the four direct hardness reductions. The repo also ships an abridged reasoning summary for this family.
Integer multiplication below n log n (family 109)
Schoolbook multiplication of two n-bit numbers takes about n squared steps. Schönhage and Strassen reached n log n log log n in 1971 and guessed n log n was optimal. The manuscript's own history says Harvey and van der Hoeven later reached n log n. The new claim is a power saving in the log factor: time O(n (log n)^(1-κ)) with κ = 2^-182, on one fixed multitape Turing machine, which would disprove the 1971 optimality conjecture in that model.
How small is that kappa? About 1.6 times 10 to the minus 55, by our arithmetic. For a trillion-bit input the saving factor, the logarithm raised to the power kappa, differs from 1 by roughly 6 parts in 10 to the 55. The manuscript says the constants are "extremely large" and that the algorithm exists to settle a bit-complexity bound. It is a theory result, not a faster library.
Lean: none. Family 109 has no Lean link in CONTENTS.md and no entry in the Lean catalogue. This is the claim with the longest history behind it and, among the eight, the thinnest verification trail: one preprint.
Fourier transform below n log n (family 130)
The fast Fourier transform computes a length-n discrete Fourier transform in about n log n operations, and it sits under signal processing and under fast multiplication. The manuscript dated September 25 claims O(n (log n)^(1-δ)) operations at every length with δ = 10^-13, in a model with exact complex arithmetic and unrestricted coefficients. It notes that known n log n lower bounds depend on which operations are allowed.
Lean: a doc exists, but read its scope. The formalized result is subsequential. For every c above 0 and every cutoff, some length n at or beyond the cutoff has a circuit with fewer than c times n times log2 n gates. The doc says there is "no all-length, bounded-coefficient, conditioning, or bit-complexity claim." That is a real and interesting statement, but it is not the all-length 10 to the minus 13 saving in the manuscript headline.
Matrix multiplication exponent at most 9/4 (family 107)
Let omega be the exponent such that n-by-n matrices can be multiplied in about n to the omega operations. Naive multiplication is 3, Strassen showed it is below 3, and omega cannot be below 2. The October 2 manuscript's own survey lists omega below 2.371177 as the most recent bound it cites. The new claim is omega at most 9/4, which is 2.25, over the complex numbers. CONTENTS.md also lists omega below 2.371054886006746 over every fixed field.
Matrix multiplication is the core operation of neural networks, so this is the result a builder is most likely to ask about. But the manuscript says its proof "does not specify a competitive finite matrix size," and the Lean doc says the result concerns arithmetic complexity rather than bit complexity or practical crossover sizes.
Lean: yes, for the complex bound of 9/4, a dual-exponent bound, a rectangular bound and the every-field bound. The doc names the two September 24 manuscripts as its sources, and says the square bound implies their weaker 2.258 headline.
Barnette's conjecture (family 180)
Take a polyhedron-like graph where every vertex has exactly three edges, the vertices split into two groups with edges only across groups, and deleting any two vertices leaves it connected. Barnette's conjecture, recorded by Grünbaum in 1969, says there is always a loop through every vertex exactly once, a Hamiltonian cycle. Partial results covered limited face sizes, such as faces with at most eight sides.
The September 24 manuscript, short at roughly 5,800 words in our text extraction, builds an acyclic edge set in the dual triangulation whose complement is the cycle. Its argument sums weights over pairs of "states", shows that terms containing a cycle cancel in pairs with opposite phase, and shows the total is nonzero so a cycle-free pair must remain.
Lean: CONTENTS.md and lean/docs/180.md list one, with a challenge file BarnetteHamiltonian.lean and a solution module under OAI/Combinatorics/Hamiltonian. That folder holds 31 files and about 8,900 lines, and our text search found no sorry or axiom keyword in it. But lean/formalization.yaml has no entry for this paper, and a Hacker News commenter who knows the problem said at the time there was no Lean proof. We could not reconcile the two by reading, and we did not build it.
Five-coloring of the plane (family 158)
The Hadwiger-Nelson problem asks for the fewest colors needed to color every point of the plane so that no two points exactly one unit apart share a color. The lower bound was four until de Grey's 2018 construction raised it to five. Seven is classical. The September 23 manuscript claims five colors are impossible for any coloring, with no assumption that color classes are measurable, which leaves six or seven.
Lean: yes. The doc formalizes both directions: five colors do not suffice, and seven do, with no measurability or continuity assumption.
Three-machine unit-job scheduling (family 124)
You have n jobs that each take one time unit, some must finish before others start, and three identical machines. What is the shortest schedule? Garey and Johnson listed this as an open problem in 1979. The two-machine case was solved long ago, and with the machine count as part of the input it is NP-complete.
The September 24 manuscript claims a deterministic polynomial-time algorithm, with running time O((L + 2)^150020) on a multitape Turing machine, where L is the binary input length. The manuscript says "no practical running-time claim is made."
Lean: a doc and a challenge file ThreeMachine.lean are listed, with a solution module under OAI/Computability/Scheduling. Like Barnette, the entry is absent from lean/formalization.yaml.
What a Lean entry tells you, and what it does not
The repo is built around a checker. Each Comparator configuration we opened names a challenge module (the readable statement), a separate solution module, the theorem to compare and the only axioms allowed. The setup follows the Advisory Group's request for a challenge file for comparator and a formalization.yaml, and the AGMAI rules post explains why those matter.
That design makes statement-checking cheap. We read the Barnette challenge file: it defines planarity as a crossing-free drawing, three-vertex-connectivity as at least four vertices that stay connected after deleting any two, and a Hamiltonian cycle as one spanning cycle, "not a possibly disconnected spanning 2-factor." To our reading that is the textbook statement. It is our reading, not an audit, but it is a few dozen lines, not 8,900.
Four things still need care:
- Scope drift. The doc's Scope paragraph is the real claim. Family 130 shows it can be weaker than the abstract.
- Catalogue lag. CONTENTS.md marks 235 of 372 families (63%, our count) with Lean links.
lean/formalization.yamllists 162 source papers and 178 distinct comparator configs, marks its scope "Partial progress," sets review status to "unchecked" and records the method as "agent." The 235 Lean docs name 405 distinct challenge files, and 227 of them, including Barnette and three-machine scheduling, are absent from the catalogue. - Preprint-only headliners. Besides integer multiplication, CONTENTS.md shows no Lean link for the full Birch and Swinnerton-Dyer formula in low Selmer corank (002), Hilbert's tenth problem over the rationals (004) or Goldfeld's conjecture (006).
- No human names. Every manuscript we opened lists "OpenAI" as author rather than named people, which is the situation the Advisory Group's section on papers "not yet understood by anybody" was written for.
What developers and mathematicians on Hacker News are saying
The thread opened at about 22:17 UTC on October 6. All numbers and claims below are commenters' own reports, not verified facts. Where they disagree, we say so.
Two number theorists disagree about how big the zeta result is
adgjlsfhk1 said that if it holds up it is the biggest result in number theory in 200 years. JoshuaZ, writing as a number theorist, pushed back: this would likely be Fields-Medal-level for a human, but not bigger than the 1896 prime number theorem it strengthens, Riemann's 1859 paper or Dirichlet's theorem on primes in arithmetic progressions. They added it would tighten Rosser-Schoenfeld-type bounds and cut three pages from one of their own 2018 papers. In a later reply they said the generalized Riemann hypothesis would matter more.
gavagai691, who also described themselves as an analytic number theorist, disagreed: Fields Medals have been given for far less, and proving quasi-RH together with no Siegel zeros would rank above the prime number theorem. They said the analytic number theorists they had talked to thought removing Siegel zeros plausible but unlikely in our lifetimes and RH-style progress basically hopeless, and recalled that when a Siegel-zero result was once rumored for Yitang Zhang, experts rated it far above his bounded-gaps theorem. Neither commenter claimed to have checked the whole proof.
A hobbyist who spent 24 years on Barnette
jboggan wrote that Barnette's conjecture occupied them on and off for 24 years and that the claimed proof (problem 180) looks, on the surface, like an approach they considered and abandoned long ago. In a follow-up they described the key idea as constructive: instead of building the cycle, it picks the edges that are not in it, in line with earlier dual attempts, via a complex-valued exponential sum on the edges. That is consistent with the weighted cancellation argument in the manuscript. Later they reported that their old test suite from earlier attempts agrees with the new algorithm, and said they were waiting for a Lean proof. As noted above, the repo does list one, so the gap is worth resolving by someone who builds it.
The galactic exponents
NotOscarWilde, who described themselves as a TCS and scheduling person, called the scheduling result of lesser importance than Unique Games but open since 1979, quoted the theorem and called the exponent of 150020 crazy. They hoped it was true "purely for the exponent." mFixman reacted to kappa equal to 2 to the minus 182 as the smallest number they had seen in a CS result. kingstnap replied that any improvement below n log n is wild, and wondered whether the Fourier transform result and the multiplication result share an underlying redundancy, which matches the manuscript's own "companion application" framing. Their first comment also picked out the five-coloring result: only 6 and 7 remain.
The notation is hard to read
amluto said they were glad OpenAI formalizes because they doubted its internal models write math well in English. They quoted the opening of section 1.1 of the Unique Games manuscript and spent a long comment untangling the symbols for constraints, labelings and indexes, arguing a clearer definition was easy. We checked: the quoted passage appears verbatim in the manuscript. A plain-language statement does sit one paragraph earlier, in the introduction, so the definition is unpacked for readers who start there, but the objection about the formal section stands.
Is anyone checking?
mathisfun123 predicted that with this many results in this many areas at least one would turn out wrong and that the release would backfire, adding that Lean only certifies a result if the theorem is stated correctly. Told that the README already warns some unformalized results could have issues, they replied that they had read it and that their point was exactly that one wrong result would backfire. Responding to a comment that papers should carry the names of human reviewers, procedurecall said that, judging by the writing in the papers on problems they had worked on, they did not think humans reviewed them. orlp argued that even if 80 percent were wrong it would still be over a hundred results. These three differ on whether errors would sink the release, but share a premise: review capacity, not generation, is the bottleneck.
schleck8 claimed that most papers are formalized in Lean, "about 80% of what I checked." Unverified. Our own count of Lean links in CONTENTS.md is 63 percent of families, and a commenter's sample is not the repo.
The "top 500" count
zone411 reported that the list claims to fully solve 90 of the "top 500" open problems on a site called ProofAtlas, and in a second comment added a category table with 45 partial matches, 135 of 500 in total. magicalist objected that the ranking comes from LLMs comparing pairs of problems. We checked the page: it says so, calls the ranking a model-based assessment "not an expert consensus," and describes its weights as "modeling choices." Treat the 90 as a count against an LLM-made list, not against a canonical one. A similar "90 of the 500" phrase has circulated on social media; we cannot confirm it traces to this comment, but the numbers match, and nothing in the repo makes that claim.
What does "three hours of ChatGPT Pro" mean?
foota quoted the README's average of about three hours of ChatGPT Pro thinking per result as "pretty crazy," and later agreed with another commenter that it is almost nothing. orlp wanted a compute-scaled number such as GPU-hours or kilowatt-hours, recalling (from memory) the AlphaZero headline that left out how many chips ran for four hours, and pressed again when others repeated the README line. The README says each result averaged three hours with the unreleased model and that about 4,000 problems were posed, but not whether failed attempts are in the average. Our first post covers how to read that figure.
PhD students getting scooped
open592 asked what a PhD student half-way through a thesis should do if one of these preprints overlaps theirs. dekhn said their own PhD was made obsolete by CRISPR and that it was a wonderful thing. aaraujo002 added that being scooped happens all the time without AI, and binlog suggested using the published results as the new base for the research. That is a pivot you can survive and an old risk made faster, with no evidence either way yet.
The Advisory Group and the request to stop
aaraujo002 also quoted the Advisory Group on Mathematics and Artificial Intelligence's request that labs "stop testing advanced mathematical problems on proprietary models" and called it a stance against progress. Another commenter supplied the fuller context: the group wrote that its recommendations assume labs already do this, and that ideally they would not. binlog argued that this was inconsistent: in their telling OpenAI announced an advisory group of renowned academics, promised to listen to it on review and communication of results, and a week later dumped everything on GitHub. Buzzard, for his part, calls the group an independent committee, and our earlier post covers how OpenAI announced it on September 21. OpenAI's stated account of consulting the group is summarized in the October 7 update of our first post.
What Terence Tao and Kevin Buzzard had said before the release
Two prominent voices predate the repository, so treat them as context rather than reactions. Kevin Buzzard's Xena Project post, To grieve, or not to grieve?, is dated October 1 and was written while OpenAI's results were still unpublished. He argued that OpenAI should "simply dump" its theorems so humans can see what is claimed, called continued secrecy "akin to censorship," and wrote that "you cannot fool Lean." He also admitted he is in the minority in valuing the theorem tally over human understanding.
Terence Tao's Mastodon thread, posted at 18:00 UTC on October 6, about four hours before the repository's first commit, described a "Math 1.0" mindset of pointing an AI at open problems. He argued solutions were being harvested "in an unsustainable fashion" and that some open directions were being withheld from fear of being scooped. A commenter linked it in the thread. We found no reaction from either to the repository itself as of this writing.
What this means for people who build with or teach AI
Nothing in these eight results changes what you will run tomorrow. Matrix multiplication and the Fourier transform are primitives in machine learning and signal processing, but the exponents and constants here are theoretical, and the integer multiplication, matrix multiplication and scheduling manuscripts all say so. What does carry over is how to read a claim like this:
- Find the statement before the proof. Open the short challenge file, not the 8,900-line solution.
- Read the Scope paragraph. The Lean doc is the claim; the abstract is the hope.
- Ask for the denominator. About 4,000 problems posed produced 372 catalogued families, under a significance filter the README describes only as "an appropriate level" of significance.
- Distrust ranking lists made by LLMs. A count against a model-made top 500 says little about significance.
- Separate "listed" from "compiled." The repo's own instructions show how to check:
# from lean/, with comparator, landrun and lean4export on PATH
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json
We have not run this. If you do, report discrepancies publicly so the fix is visible, in the spirit of how to read AI benchmarks and the checklist for mass releases. Other labs' math releases this month are worth scoring the same way: Gemini's Cogentic harness, Meta's Muse Spark papers and Claude's 3SUM and APSP claim.
What is still unverified
- That any of the eight results has been independently refereed.
- Whether the Lean code for Barnette and three-machine scheduling builds, and why the machine-readable catalogue omits them.
- The correctness of anything in the quasi-Riemann manuscript beyond what its Lean doc says is formalized. The manuscript runs to roughly 119,000 words in our text extraction, and the doc says the later applications are not included.
- schleck8's "80 percent" Lean figure, and every commenter's identity and credentials, which are self-described.
- OpenAI's own account of significance. We could not load the announcement page (it returned an access error), so we rely on the repository, which is the primary artifact.
Related reading
- OpenAI's 722 math manuscripts: what the repo contains
- OpenAI "400 math papers" rumor: what is verified
- AGMAI's rules for releasing AI-generated mathematics
- OpenAI's advisory group and the 100-plus problems claim
- 25 Fields Medalists on AI and math
- No, AI did not just solve Navier-Stokes
- Are labs hoarding solved math problems?
- Lean 4 and the collapse in formal proof cost
Primary sources: openai/math repository (README, CONTENTS.md, lean/docs, preprints), Hacker News thread, AGMAI recommendations, September 29, 2026, Buzzard, Xena Project, ProofAtlas open problems ranking.
Details are accurate as of October 7, 2026. The repository is being updated, so counts, Lean links and catalogue entries may change.