OpenAI and Anthropic both say their in-house AI models have refuted the Exponential Time Hypothesis, a 1990s conjecture that much of theoretical computer science quietly leans on. Both say their models found it on the same day, October 16. Both posted machine-checked proofs. No human has finished checking either one.
Key points
- OpenAI and Anthropic each say an in-house AI model refuted the Exponential Time Hypothesis, and both date the discovery to Oct. 16.
- Both labs posted proofs formalized in Lean, but no human has finished checking either result.
- Both say the result does not settle P versus NP, and Anthropic says its bound only beats brute force at astronomically large input sizes.
- ETH co-proposers Russell Impagliazzo and Ramamohan Paturi and MIT’s Ryan Williams are reviewing OpenAI’s result and say their involvement is not certification.
OpenAI went first, on Monday, October 26, with a blog post announcing three AI-generated results: the ETH disproof, a proof touching the famous Kakeya conjecture in math, and an existence proof for the quantum field theory behind the strong nuclear force. Hours later, at 03:07 UTC on October 27, Anthropic dropped its own ETH refutation on GitHub, with the author line reading simply “Claude, Anthropic.” The math is real enough to take seriously. The rest is a story about who gets to say a result is true, and how fast.
What the Exponential Time Hypothesis actually says
Start with 3-SAT, the classic logic puzzle of computer science. You get a formula built from clauses, each an OR of up to three true-or-false variables, all joined by AND. The question: is there any assignment of true and false that makes every clause true? Checking a proposed answer is easy. Finding one, as far as anyone could prove, means grinding through something close to all 2n combinations for n variables.
Decades of clever algorithms have shaved that down. According to Anthropic’s paper, the previous records were roughly 1.328n steps for deterministic algorithms and 1.308n for randomized ones. Faster, but still exponential.
The ETH, formalized by Russell Impagliazzo and Ramamohan Paturi in their paper “On the Complexity of k-SAT”, bets that this shaving has a floor: there is some fixed constant below which no algorithm can push 3-SAT’s exponent. You can shrink the base of the exponential, but you can never escape exponential time. Researchers have treated that bet as bedrock. OpenAI says the ETH has been used in “hundreds of papers” to prove hardness results in graph theory, computational biology, databases and computational geometry. Anthropic’s paper says a Claude-run literature search turned up more than 800 papers that prove at least one result only under ETH or a stronger hypothesis that implies it.
What the two labs are claiming
In substance, the same thing. Each lab describes a deterministic algorithm that doesn’t just decide 3-SAT but counts every satisfying assignment (the harder #3-SAT problem) in “subexponential” time, meaning it eventually beats 2δn for any fixed δ, however small. That is exactly what ETH says can’t happen.
OpenAI’s manuscript is titled, without a hedge, “The Exponential Time Hypothesis is False.” The company says its model found the natural-language proof on October 16 and that the result was formalized in Lean, a proof assistant that checks every logical step by machine, on October 17. A side-by-side analysis by Papex notes that OpenAI’s paper says it also knocks out ETH’s stronger cousins, including SETH and Gap-ETH, and that OpenAI’s own Lean scope note says the formal proof gets a slightly weaker bound than the paper’s headline. Weaker, but still enough to sink ETH.
Anthropic’s paper, “A 2o(n) Time Algorithm for 3-SAT,” says the core algorithm was found on October 16 “by an internal Claude research model with 14M output tokens and no human input,” after which Anthropic researchers worked with Claude on the presentation. Its Lean 4 formalization, also written by AI models, is checked by Lean’s kernel and re-checked by a second, independently written kernel called nanoda. The paper says the two results were found “independently and concurrently” and cites OpenAI’s preprint. OpenAI’s announcement doesn’t mention Anthropic.
Two rival labs announcing the same landmark result, dated to the same day, within hours of each other. If it holds up, it’s one of the stranger coincidences in the history of science. If it doesn’t, it’s two very expensive typos.
No, this does not prove P = NP
The obvious next question is the million-dollar one: does this crack P versus NP, the open problem asking whether every puzzle that’s easy to check is also easy to solve? Both labs say no. Anthropic’s paper states its result “does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems.” Subexponential is a lot faster than exponential, but still far slower than polynomial, which is what P = NP would require.
It does shift the vibes. MIT’s Ryan Williams, who is helping run the review, told TechCrunch: “Every computer scientist should probably put a little more weight on the plausibility of P = NP, but one’s weight may vary.” He added that he doesn’t think “OpenAI’s algorithm could possibly be the best algorithm you can get.”
Your laptop’s SAT solver is safe, and so is your bank
Anthropic’s paper is blunt: “Our result is purely asymptotic.” For 3-SAT formulas with five times as many clauses as variables, it says, its proven bound doesn’t beat plain brute-force search until the number of variables exceeds 1010,000, and its general approach “seems unlikely to yield any general improvement unless n > 107.” For scale, the paper notes brute force is already impractical at n = 100. “Thus our result says nothing about solving formulas in practice.”
OpenAI is similarly careful, saying that “finding such algorithms, and turning theoretical advances into practical improvements, will require significant further research.”
Cryptography was the other immediate worry, since a lot of security rests on some problems being reliably hard. Williams told TechCrunch that one of his first questions to OpenAI science lead Dan Roberts was whether anything is now insecure, and that OpenAI had checked and was “reasonably confident” the result didn’t imply any breaks. That is OpenAI’s assessment, relayed secondhand, not an independent audit. It’s also consistent with the numbers above: an algorithm that only wins at astronomically large sizes doesn’t crack keys anyone actually uses.
The real fallout lands on theorists
Why it matters: the immediate damage is to a field’s foundations, not to anyone’s software. A huge body of “conditional” results reads like this: if ETH is true, then problem X can’t be solved faster than Y. If ETH is false, those conditions fail and those lower bounds lose their footing.
Not everything collapses. Anthropic’s paper notes its theorem does not refute the Orthogonal Vectors hypothesis, which many fine-grained complexity results also rest on, and Papex quotes OpenAI’s paper saying “some of the same lower bounds follow from weaker hypotheses that may still hold.” Sorting out which results survive falls to humans. Williams told TechCrunch that’s part of why he pushed OpenAI to fund a conference: “it’s going to affect many researchers’ works.”
The people who proposed ETH are now checking its obituary
The review setup is unusual. OpenAI asked Impagliazzo and Paturi of UC San Diego, two of ETH’s original proposers, and MIT’s Williams to “shepherd” the computer science result. Williams posted that the three signed no NDAs and receive no compensation, and that they asked OpenAI to release all its raw ETH data and sponsor a conference for the affected community. OpenAI agreed to both.
Their open letter to the community, as quoted by The Next Web and Papex, is careful on the key point: “Our involvement should not be taken as certification of the claim. A result of this significance requires careful, independent scrutiny.” It is also clear about the stakes: “If the claim is correct, it will change an important part of theoretical computer science.” According to Papex, the letter lists Anthropic’s refutation as a resource alongside OpenAI’s.
Williams isn’t a cheerleader. He previously called OpenAI’s earlier October proof dump a “DDOS attack on mathematicians,” per TechCrunch. This time he described the ETH proof as partly “routine,” with “two or three alien-looking parts” that convinced him “the whole community needs to work on together.”
The catch: Lean checks proofs, not press releases
Lean formalization is a big deal, and it deserves credit. It means a machine has verified that every step follows from the last. But it can only check the theorem as written in Lean. Anthropic’s own README states the limit plainly: “Lean checks the proofs, but no machine checks that this file says what the paper says.” If a definition of “time,” “Turing machine” or “formula” is subtly off, a flawless proof can prove a weaker statement than the headline.
Anthropic keeps its statement file short and proof-free so a reader can do that check. (Its build does print two sorry warnings, Lean’s marker for an unproven statement. The README says both come from a separate file that restates the two theorems for comparison, not from gaps in the proof.) According to Papex, Anthropic’s deposit on the Hexagon math preprint server carries two labels: “Primarily AI-generated” and “Some parts of this contribution, but not all, have been checked and understood by a human.”
Our read: two labs independently landing on the same claimed bound is either strong evidence it’s real or a sign both systems learned to fool the same checker. We can’t tell which from here; that’s what the human review is for. Until humans confirm the formal statements match the real conjecture, this is a claim with unusually good receipts.
Meanwhile, Kakeya and Yang-Mills
ETH wasn’t even OpenAI’s only big swing. The company says its models proved the local smoothing conjecture, a 1991 statement about how waves focus, in every dimension. That would also settle the Kakeya conjecture and Stein’s restriction conjecture in all dimensions. Mathematicians had previously proved local smoothing in two dimensions (Guth, Wang and Zhang, 2019) and Kakeya in three (Wang and Zahl, 2025). OpenAI posted the write-up and Lean proof publicly. Papex flags that the paper’s own wording on restriction is narrower than the blog’s “all dimensions” pitch, a nuance for specialists to settle.
The physics claim is bigger and murkier: a rigorous existence proof for four-dimensional quantum field theories including quantum chromodynamics, plus pure Yang-Mills theory. That last piece is “part of” a Clay Millennium Prize problem. Note the word “part.” The prize also requires proving a “mass gap,” which OpenAI’s announcement doesn’t claim. A group led by Nobel laureate David Gross is shepherding the work and has chosen to write it up themselves instead of releasing the AI output. Not everyone likes that: a mathematicians’ group hosted at the Institute for Advanced Study, AGMAI, called on OpenAI “to make public without delay” the outputs, arguing that with the Lean work finished, “there is no scientific reason for delaying the release any further.”
Who gets credit when the author is a model?
OpenAI says it seeks “no academic credit” for discoveries by its internal models and wants recognition to go to the human groups who explain them. It also points to a $5 million contribution to the Simons Foundation to fund workshops and conferences on AI-produced results. Anthropic took a different route: paper and proof straight onto its own GitHub, labeled a “research artifact,” no working group.
Both approaches have critics. AGMAI warned the day before OpenAI’s announcement that designating hand-picked mathematicians risks “borrowed reputation,” with experts’ names “vouching for the release.” The ETH examiners themselves note that early access “creates opportunities unavailable to others.” And there’s no neutral timestamp for either lab’s October 16 claim. The first public files are GitHub commits from October 26 and 27. Who found it first will rest on each company’s word.
The takeaway
For years, “AI does math” meant olympiad problems and benchmark scores. This week two labs claim to have knocked over a load-bearing conjecture in computer science, with formal proofs anyone can download. That’s a real shift, even with every caveat attached. It’s also a result with zero practical speedup and, so far, zero completed human verification.
What to watch next:
- The Impagliazzo-Paturi-Williams findings. They’ve promised to share progress publicly. Any word that the Lean statements faithfully match ETH is the first real verdict.
- Independent re-derivations. Anthropic claims Claude Opus 5.5 can rederive a weaker version of the refutation from a short sketch. Human-written simplifications would mean far more.
- The conference. OpenAI has committed to fund one. Who organizes it, and who gets invited, will show whether this stays community-led.
- The Yang-Mills files. Pressure to release the physics output is already building. Watch whether the Gross group holds the line.
Hype in. Signal out.
Update (Oct 29, 2026): we narrowed our description of the 1010,000 threshold to the formulas Anthropic’s paper specifies (five clauses per variable), and removed our own guess about whether the result will hold up, since it hasn’t yet been checked by independent experts.
Image: Russell Impagliazzo lecturing at the DIMACS Workshop on Cryptography and its Interactions, Rutgers University, 2016. Photo by BöhmMartin / Wikimedia Commons, CC BY-SA 4.0; cropped to 16:9.
