On October 26, OpenAI announced that an internal model had disproved the Exponential Time Hypothesis and that the proof had been checked in Lean. ETH, proposed by Russell Impagliazzo, Ramamohan Paturi and Francis Zane in 1999, formalizes the belief that brute-force search is close to the best possible for SAT: no algorithm solves 3-SAT in time subexponential in the number of variables. The same day, Anthropic posted a paper credited to Claude claiming the same result. Neither claim has been peer reviewed, so the useful questions are what would change if one holds, and what a Lean check does not certify.
Two labs, one hypothesis, one date
OpenAI says its model produced the argument on October 16 and the Lean formalization followed the next day (TNW; Interesting Engineering). Per OpenAI's Lean scope note, as relayed by AiCybr and a public GitHub issue, the formal statement is stronger than deciding satisfiability: one deterministic machine that exactly counts the satisfying assignments of k-CNF formulas, for every fixed k of at least 2, in time (L+1)^O_k(1) · 2^O_k(n (log log n)^2 / sqrt(log n)) for n variables and an encoded input of length L. The coefficient on n in that exponent does go to zero. It takes its time.
Anthropic's paper, A 2^o(n) Time Algorithm for 3-SAT, lists Claude as its author and is dated October 26 (Decrypt). An unnamed internal research model found the algorithm on October 16, using 14 million output tokens and no human input into the discovery, and Anthropic researcher Levent Alpoge announced it on X, OfficeChai reports. The files sit in Anthropic's formal-math repository. Same hypothesis, same reported day.
OpenAI's announcement had two siblings. It claims a proof of Christopher Sogge's 1991 local smoothing conjecture in every dimension, which would also settle the Kakeya and Stein restriction conjectures (TNW), generated on October 18 and formalized the next day (Interesting Engineering); Alex Iosevich, a harmonic analyst at Rochester, told Al Jazeera it looked historic. The physics claim, rigorous existence proofs for four-dimensional quantum field theories including quantum chromodynamics and pure Yang-Mills, part of a Clay Millennium problem, remains unreleased: the examining group, led by Nobel laureate David Gross, chose to write up the work itself first (TNW). Digit's Vyom Ramani objected that whoever picks these groups, which OpenAI calls shepherds, decides who interprets the results, and of the physics wrote: "At the moment there is nothing to verify."
What breaks if ETH breaks: lower bounds, not locks
ETH is a floor under other theorems, not under production code. A 2011 EATCS survey by Marek Cygan and seven co-authors catalogs lower bounds in exact and parameterized algorithms that rest on ETH and on its stronger sibling, the Strong Exponential Time Hypothesis. Since SETH implies ETH, a refutation takes SETH down too, and with it results engineers have used without naming them: the proof that textbook dynamic programs over tree decompositions cannot be improved even slightly in the base of the exponent for Independent Set, Dominating Set and q-Coloring (Lokshtanov, Marx and Saurabh), and Backurs and Indyk's 2015 argument that the classic edit-distance algorithm is essentially optimal, which holds only if SETH does.
What would not follow matters as much. Those results would not flip into faster algorithms; they would lose the assumption they stood on. The claimed algorithms are subexponential only in the most literal sense: Anthropic's repository calls its result asymptotic and silent on practical solving (Decrypt), and OfficeChai's reading of the paper puts the point where it beats brute force on a typical formula beyond roughly 10^10,000 variables (OfficeChai). SAT solvers will not notice, and P versus NP stays open, since subexponential is still far from polynomial. Nor is RSA in the blast radius: it rests on factoring, a different problem.
Lean checks the proof, not the question
Lean's kernel certifies that a proof proves its formal statement. It cannot certify that the statement says what ETH says, and in complexity theory the gap is wide, because time itself has to be defined. OpenAI's comparator file defines its own primitive machine, CNF encoding, execution traces and running-time budget (AiCybr); the theorem is exactly as meaningful as that machine is honest. A model that charged unit cost for arithmetic on enormous numbers, or an encoding that smuggled work into the input, could make a subexponential theorem true and irrelevant. Nobody has shown either lab did this; reviewers must rule it out. AiCybr adds that a result about a restricted encoding needs a reduction from ordinary CNF, with acceptable overhead, before it counts against ETH.
Both labs have shrunk what a human must read. Anthropic's statement file imports only Mathlib and, per its README as quoted in the same GitHub issue, relies on nothing beyond Lean's three standard axioms; the development spans 1,050 modules, checked by Lean's kernel and by the independent checker nanoda (OfficeChai). Yet the paper's appendix says the Lean was written by AI models and reviewed by other instances of the same models, and that "at the time of writing no person is known to have checked it."
OpenAI's own record argues for patience. It released 722 manuscripts on October 6. A day later its changelog withdrew three manuscripts after a sign error was found in one of them, revised 14 others, and counted 300 of 719 top-line results as formalized, about 42%. Prose carries the rest.
Impagliazzo and Paturi, both at UC San Diego, and MIT's Ryan Williams are leading an independent examination, unpaid and without NDAs; at their request OpenAI agreed to release all raw data and fund a community conference, and it has given $5 million to the Simons Foundation for workshops on AI-produced results (TNW). Their open letter is careful: "Our involvement should not be taken as certification of the claim." Williams told Al Jazeera his group is working to verify the proof and see whether it holds up, and called it "a shocking development."
The 30,000-foot read
Extraordinary claims now arrive with machine-checked proofs attached, which is progress, and with press releases attached, which is not new. Lean turns is the proof right? into is the statement right?, a smaller question that still needs people; by Anthropic's own account, nobody has yet answered it for Claude's proof. What can be controlled here is process: public statement files, raw data, reviewers who signed nothing. Whether ETH is true cannot be controlled, and no blog post settles it.
Watch the Impagliazzo, Paturi and Williams group's findings, whether both labs' machine models survive a hostile reading, and the first named human who says they checked the Lean. If ETH does fall, it will be a beautiful result with almost no practical consequence for years, which is how the deepest results tend to arrive.
Sources: OpenAI announcement (primary; see CAVEATs); OpenAI, openai/math changelog (primary: October 7 withdrawals and revisions, 300 of 719 results formalized); The Next Web (claims, dates, Lean check, review group, open letter, raw-data and conference commitments, $5 million Simons gift, physics group, 722 manuscripts); Al Jazeera (Williams and Iosevich reactions, the shepherd label); Interesting Engineering (October 16 to 19 dates); The Kyunghyang Shinmun (ETH's 1999 origin, Yang-Mills scope); Decrypt (Anthropic's paper, title, date and repository wording); OfficeChai on Anthropic's paper (discovery date, token count, Alpoge announcement, Lean module count, nanoda, review status, crossover estimate, SETH); OfficeChai ETH explainer (plain-language definition); AiCybr (OpenAI's Lean scope note and comparator file, encoding caveat); GitHub issue jsboige/CoursIA #23139 (quotations from both repositories: bounds, statement files, axioms); Anthropic formal-math repository (location of Anthropic's release); Digit (shepherd criticism, physics quote); Cygan et al., EATCS Bulletin survey (ETH- and SETH-based lower bounds); Lokshtanov, Marx and Saurabh (SETH-based treewidth bounds); Quanta, republished by the World Economic Forum (edit distance and SETH); The Quantum Insider (P versus NP context). CAVEATs: every result described here is unreviewed and company-reported, and the physics material is unreleased. OpenAI's announcement page, the openai/math README, The Verge's report, and Anthropic's repository and paper could not be opened by our fetcher; OpenAI's claims are taken from reputable outlets that report them (The Next Web, Al Jazeera, The Kyunghyang Shinmun, Interesting Engineering), and the technical details of both Lean statements come from secondary write-ups (AiCybr and a third-party GitHub issue) that we could not check against the files. The token count and the 10^10,000 crossover are single-source (OfficeChai). The line on RSA and factoring is standard background, not linked. Corrections to our leads: the 3-SAT paper was not merely credited to an Anthropic model on X; Anthropic published it in its own GitHub repository, dated October 26, an Anthropic researcher announced it, and coverage followed on October 27. The physics material was withheld by the examining group's choice, per TNW and Al Jazeera, and the criticism we found came from press commentary, not named physicists. The October 19 Lean date for local smoothing is inferred from Interesting Engineering's report that formalization followed the October 18 proof by a day.