Exponential Time Hypothesis Refutation From a Claude Model Comes With a Proof a Machine Can Check

Anthropic says an internal research Claude model has refuted the Exponential Time Hypothesis, and on October 27, 2026 it published the paper together with a Lean 4 proof that a computer can check. OpenAI had released its own refutation hours earlier. Neither claim has been through peer review, and Anthropic’s release shows exactly where human checking is still required.

Two AI Labs Say Their Models Refuted the Exponential Time Hypothesis

OpenAI and Anthropic each claim an algorithm that solves 3-SAT, a standard class of logic puzzle, faster than the Exponential Time Hypothesis allows. Russell Impagliazzo and Ramamohan Paturi of UC San Diego proposed the hypothesis in 1999. It says the time any algorithm needs to solve 3-SAT must grow exponentially as the number of variables grows. Researchers have used it for decades as a working assumption when proving that other problems are hard. TechCrunch reported that OpenAI released solutions to three long-standing problems, one of them a refutation of the hypothesis. Anthropic mathematician Levent Alpöge suggested OpenAI’s solution leaned on existing work, and Anthropic then posted its own refutation to its formal-math repository on GitHub. Anthropic’s README states the result as a deterministic algorithm that decides 3-SAT on n variables in 2^o(n) time and counts all satisfying assignments within a stated sub-exponential bound. It adds that the result is purely asymptotic and says nothing about solving formulas in practice.

Anthropic’s Lean Proof Compiles in About Eight Minutes

Anthropic’s claim can be checked by running a build. The repository contains the paper and a formalization in Lean 4, a proof assistant, which Anthropic says AI models wrote. According to the README, building it took about eight minutes on 24 virtual CPUs, and the largest process used about 7 GB of memory. A final command prints the axioms each main theorem depends on, and Anthropic says these are only Lean’s three standard axioms, so the proofs do not rest on any hidden assumption. The repository’s automated checks go further. A tool called Comparator confirms the theorems match a separate challenge file, and a second, independently written Lean kernel named nanoda re-checks every proof. Lean and its Mathlib library are pinned to version 4.33.1, so anyone running the build checks the same artifact Anthropic did.

No Machine Checks That the Lean Statement Says What the Paper Says

A compiling proof only shows that the theorem written in Lean is true. Anthropic’s README states plainly that no machine checks whether that theorem matches the claim in the paper. To close the gap, Anthropic put both claims in one file, MainResults.lean, which holds definitions only and imports nothing beyond Mathlib, and kept it short so a person can read it. The paper’s Appendix E prints the file and lists where it differs from the printed statements. A separate index maps every numbered result in the paper to its Lean counterpart. The file also leaves some steps outside the proof. It models algorithms as one kind of Mathlib stack machine, and it treats the simulation of that machine on an ordinary computer as a standard fact the Lean code does not prove. Checking those choices is the job left for human reviewers, and it is a far smaller job than reading the full proof.

Computer Scientists Are Organizing the Review Themselves

MIT professor Ryan Williams is coordinating his field’s response, TechCrunch reported. Earlier in October he had criticized OpenAI’s practice of releasing proofs in bulk. He agreed to help interpret the new result alongside Impagliazzo and Paturi, and the three issued an open letter asking researchers for feedback and for a discussion of norms around AI contributions. Williams told TechCrunch that parts of OpenAI’s proof look routine and two or three parts looked alien to him. He also said many papers built on the hypothesis over the past decade will need to be revisited if the result holds. His first question to OpenAI science lead Dan Roberts was whether any cryptosystem was now insecure. Williams said OpenAI had checked and was reasonably confident nothing was broken.

Why This Matters for Engineering Leadership

Anthropic’s repository is a working example of how to review output that is too large for any person to read. The proof itself is checked by two independent kernels. Human attention goes to one short file that states what is being claimed, and the paper lists every place that file differs from the prose. The same split applies to AI-generated code. Tests, type checks and policy engines can confirm that the code meets a specification, but they cannot confirm that the specification describes what the business needed. Teams adopting coding agents should keep the specification short, readable and separately reviewed, record where it departs from the original requirement, and treat a passing build as proof of conformance to that specification and nothing more. Williams’s question about cryptography is the second lesson. When a dependency’s core assumption changes, the first task is to list what relied on it, before anyone debates whether the change is real. We made a related argument about verifying that an AI agent actually finished its task.

FAQ