> ## Content Index > Fetch the complete content index at: https://www.dailyferment.com/llms.txt > Use this file to discover other available public pages before exploring further. # Lean says OpenAI's proofs check out. Who checks they prove the right thing? - URL: https://www.dailyferment.com/openai-math-proofs-lean-what-it-checks/ - Published: 2026-10-28T01:00:00.000Z - Updated: 2026-10-28T01:00:00.000Z - Description: OpenAI says its AI disproved the Exponential Time Hypothesis and Lean verified it. Lean checks a proof against a written statement. Whether that statement is ETH is a human job. - Author: Rana Bilal Zafar - Tags: Science & Health, AI, #reframe On 26 October 2026 OpenAI said one of its models had disproved the Exponential Time Hypothesis (ETH), a conjecture about how hard it is to solve logic puzzles that hundreds of papers in computer science lean on. The argument was found on 16 October and, OpenAI says, "subsequently verified in Lean" the next day. So is ETH dead? Not settled yet. A Lean check confirms that a proof really proves the theorem as written in a file. Whether that written theorem is ETH as the field means it is a separate question, and it is a human one. Three computer scientists, Russell Impagliazzo and Ramamohan Paturi of UC San Diego and Ryan Williams of MIT, are now organizing an open examination. That second question is the one I want to look at. ## What did OpenAI actually announce? The [OpenAI post](https://openai.com/index/building-scientific-understanding-with-academic-communities/?ref=dailyferment.com) claims three results at once: Sogge's local smoothing conjecture in every dimension, which it says also settles the Kakeya and restriction conjectures; the ETH disproof; and an existence proof for quantum field theories including QCD, with pure Yang-Mills existence as a step. Yang-Mills existence is one of the Clay Millennium Prize problems. OpenAI says the Yang-Mills proof was formalized in Lean on 16 October; the post does not say the QCD part was. For ETH, the [openai/math repository](https://github.com/openai/math/blob/main/CONTENTS.md?ref=dailyferment.com) describes a deterministic algorithm that counts the satisfying assignments of any k-CNF formula in time roughly 2 to the power n divided by the square root of log n. ETH says 3-SAT needs time exponential in n. If the algorithm is right, ETH is false. Guess first: of the 373 result families OpenAI released, what share of the top-line results come with a Lean formalization? **About 42%**, by the repository's own count. The README adds that "some of the unformalized results could have issues." Source: openai/math README, read 27 Oct 2026. The repository is also honest about its limits. It holds 721 manuscripts in 373 result families, produced from about 4,000 problems posed to an unnamed internal model. Its README says "\~42% top-line results formalized" and that "some of the unformalized results could have issues." OpenAI calls the manuscripts raw research data, not papers. **721**manuscripts in the openai/math repository **373**result families **About 4,000**problems posed to the model **About 42%**of top-line results formalized in Lean Source: openai/math README, read 27 Oct 2026. ## What does "verified in Lean" cover? Lean is a proof assistant. You write a theorem in its language, and a small, trusted kernel checks every step of a proof of it. OpenAI's release uses a tool called comparator, which builds the proof in a sandbox and confirms it proves exactly the statements in a "challenge file". The [Lean reference manual](https://lean-lang.org/doc/reference/latest/ValidatingProofs/?ref=dailyferment.com) is blunt about what that buys. It separates two questions: does the theorem have a valid proof, and what does the theorem statement mean. The checker answers the first. For the second, it says the remaining risk is human error or misleading presentation in the challenge file, and that a doubtful reader should review the statement and its definitions, especially custom notation. The [ETH challenge file](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/SubexponentialSAT.lean?ref=dailyferment.com) is public. It is short, roughly 9,000 characters. To say "this runs in less than exponential time", it first has to define what a computer is and what one unit of time is. It does that itself: a "PrimitiveMachine" with a few tapes, where each step reads one cell and either answers, moves a head or writes a symbol. It defines how a formula is written as bits, with numbers in unary. Then the theorem: one fixed machine of this kind counts the solutions of every bounded-width formula, within a stated number of steps and polynomial tape space. What the ETH challenge file says, in plain words It defines a formula, an assignment of true and false to its variables, and the number of assignments that make it true. It writes a formula as a string of bits, with numbers in unary. It defines a "PrimitiveMachine": a few tapes, a finite set of states, and a step that reads one cell and then answers, moves a head or writes a symbol. The theorem says one fixed machine of this kind, for every formula whose clauses have at most k literals (k at least 2), ends with the exact count on one tape and the yes or no answer on another, within C times (bits + 1) to the power d times 2 to the power of A n (log log n)^2 / sqrt(log n) steps, using polynomially many tape cells. Allowed axioms: the three standard ones. Source: openai/math, lean/ComparatorChallenges/SubexponentialSAT.lean and its .json, read 27 Oct 2026. To a non-specialist that reads like a standard multi-tape Turing machine. Certifying it is not a job for a non-specialist, and that is the point. The proof can be perfect and the result still not be ETH if one of those definitions quietly makes something free that should cost time. Checking that is a reading job for people who know complexity theory, and the file is short enough to read line by line, which a long paper never quite is. That is a real change. ![Diagram: the proof is checked by the Lean kernel against the statement in the challenge file, which is settled; whether that statement matches the conjecture the field means, ETH, is for people who know the field and is still open](https://storage.ghost.io/c/d7/b7/d7b77195-48c5-45ab-8688-51750879d1d6/content/images/2026/10/df79-what-lean-checks.png) A Lean check settles the first arrow. The second is a reading job. Sources: Lean Language Reference; openai/math, read 27 Oct 2026. ## The rocket that did what its specification said ![A rocket lifting off from a coastal launch pad, trailing flame and a large cloud of white exhaust](https://storage.ghost.io/c/d7/b7/d7b77195-48c5-45ab-8688-51750879d1d6/content/images/2026/10/df79-launch.jpg) A launch, not Ariane 5 (illustrative). Photo by [SpaceX](https://unsplash.com/@spacex?ref=dailyferment.com) on [Unsplash](https://unsplash.com/photos/OHOU-5UVIYQ?ref=dailyferment.com) On 4 June 1996 Ariane 5 broke up about 39 seconds after ignition. The [inquiry board's report](https://www.cs.toronto.edu/~krj/courses/2307/disasters/ariane5rep.html?ref=dailyferment.com), chaired by Jacques-Louis Lions and published on 19 July 1996, traced it to the inertial reference software, reused from Ariane 4\. A value called horizontal bias overflowed when converted from a 64-bit float to a 16-bit integer. On Ariane 4's flight path the value stayed below the limit with an adequate margin. Ariane 5 built up horizontal speed about five times faster. The software did what its specification said. The trouble was in the specification: the report says "it was jointly agreed not to include the Ariane 5 trajectory data" in the requirements, and no test ran the software against that trajectory. Correct against the wrong specification #### Ariane 5 flight 501, 4 June 1996 - *What was checked* software reused from Ariane 4, sound on Ariane 4's flight path - *What was assumed* horizontal speed would stay in Ariane 4's range - *What was left out* Ariane 5 trajectory data, by joint agreement - *Result* overflow and breakup about 39 seconds after ignition #### A Lean-checked proof, Oct 2026 - *What was checked* every step, against the challenge file - *What is assumed* the file's machine, time and encoding match what the field means - *Who checks that* people who know the field, reading the file - *Result* still open for ETH Sources: Ariane 5 Inquiry Board report, 19 Jul 1996; Lean Language Reference, Validating Proofs; openai/math SubexponentialSAT.lean. A Lean proof is like that flight software at its best: correct against its specification, with no doubt about the steps. The challenge file is the specification. Everything rides on whether it describes the rocket you are actually flying. ## Has this happened already? Something close. On 8 September OpenAI announced a Lean-checked proof about the Navier-Stokes equations, another Millennium problem. As [The Batch](https://www.deeplearning.ai/the-batch/inside-the-dispute-over-a-landmark-agent-driven-mathematical-proof?ref=dailyferment.com) laid out, the proof covers fluids pushed by a smooth outside force, which Clay's problem statement allows; the harder version with no outside force is still open. Which statement got proved was the whole story, and you could only see it by reading the statement. 1. **8 Sep 2026** OpenAI announces a Lean-checked Navier-Stokes result (forced version) 2. **9 and 18 Sep** Yang-Mills and QCD proofs produced, per OpenAI 3. **16 Oct** ETH disproof found; Yang-Mills formalization finished 4. **17 Oct** ETH disproof formalized in Lean 5. **26 Oct** OpenAI announces the three results and the shepherd groups 6. **Clay rule** At least two years after publication, plus general acceptance Sources: OpenAI, 26 Oct 2026; The Batch, Sep 2026; Clay Mathematics Institute rules. The Clay Mathematics Institute did not need Lean to arrive at the same caution. Its [rules](https://claymath.org/millennium-problems/rules?ref=dailyferment.com) want a solution published in a qualifying outlet, at least two years since publication, and "general acceptance in the global mathematics community." Two years used to be time for checking steps. With a machine-checked proof, most of that time can go to the statement and to understanding why the proof works. OpenAI's shepherd setup on 26 October, with no NDAs and no academic credit claimed by OpenAI, reads to me as an answer to that. It puts the reading in the hands of the people who wrote the conjecture. Impagliazzo and Paturi proposed ETH in the first place, with Francis Zane. ## How sure am I? Established OpenAI's claims, dates and shepherds as stated on its page; the repository's 721 manuscripts, 373 families and about 42% formalized; what the Lean manual says a check does and does not cover; what the ETH challenge file defines; Clay's rules; the Ariane 5 report. Inferred That the review that matters now is of the challenge file's definitions, not the proof steps. Guess If the ETH claim fails, it will fail on a definition, not a step. I would not bet on it failing at all; I would bet on the argument being about the machine model. The claim, in one sentence A machine-checked proof moves the question from "is the proof right?" to "is this the right statement?", and only people who know the field can answer the second. Earlier on this site I wrote about [arXiv rationing submissions to save reviewers' time](https://www.dailyferment.com/arxiv-two-submissions-per-month-moderator-time/) and about an OpenAI model that [met a benchmark's rule while missing its intent](https://www.dailyferment.com/gpt-6-astra-starcraft-stardust-benchmark-checkpoints/). Both were about where human attention goes once machines do the bulk of the work. This is the same question at the top of mathematics. **More on Daily Ferment:** [An AI agent could change what its reviewer saw. The SEC had the same problem with Madoff.](https://www.dailyferment.com/metr-inspect-agent-transcript-viewer-madoff/) and [Gemini 4 Argon's 15% hallucination rate isn't how often it's wrong](https://www.dailyferment.com/gemini-4-argon-hallucination-rate-what-it-measures/) ## Sources - [OpenAI: Working with academic communities to build scientific understanding, 26 Oct 2026](https://openai.com/index/building-scientific-understanding-with-academic-communities/?ref=dailyferment.com) - [openai/math repository README](https://github.com/openai/math?ref=dailyferment.com) and [CONTENTS.md, result 378](https://github.com/openai/math/blob/main/CONTENTS.md?ref=dailyferment.com), read 27 Oct 2026 - [openai/math, ETH challenge file SubexponentialSAT.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/SubexponentialSAT.lean?ref=dailyferment.com), read 27 Oct 2026 - [Lean Language Reference: Validating Proofs](https://lean-lang.org/doc/reference/latest/ValidatingProofs/?ref=dailyferment.com) - [The Batch: Inside the dispute over a landmark agent-driven mathematical proof, Sep 2026](https://www.deeplearning.ai/the-batch/inside-the-dispute-over-a-landmark-agent-driven-mathematical-proof?ref=dailyferment.com) - [Clay Mathematics Institute: Rules for the Millennium Prize Problems (adopted 26 Sep 2018)](https://claymath.org/millennium-problems/rules?ref=dailyferment.com) - [Ariane 5 Flight 501 Failure, Report by the Inquiry Board, 19 Jul 1996](https://www.cs.toronto.edu/~krj/courses/2307/disasters/ariane5rep.html?ref=dailyferment.com)