On 27 October 2026 Anthropic deposited "A 2^{o(n)} Time Algorithm for 3-SAT" on Hexagon, a math preprint site, and merged a Lean 4 formalization into its public formal-math GitHub repository. The paper claims a deterministic algorithm that counts the satisfying assignments of 3-CNF formulas (#3-SAT) in subexponential time. That would refute the Exponential Time Hypothesis (ETH), the 1999 conjecture of Impagliazzo, Paturi and Zane. According to the provenance note, an internal Claude research model found the core algorithm on 16 October using 14M output tokens with no human input, and Anthropic researchers then helped with the presentation. Hours earlier, OpenAI had posted its own AI-generated preprint, "The Exponential Time Hypothesis is False," with its own Lean proof.
This matters for AI builders for two reasons. First, if the result holds, two frontier labs independently produced a major theorem in theoretical computer science, with machine-checked proofs, on the same day. Second, the episode tests how far "verified in Lean" can carry trust in an AI-generated result. Lean can prove that the code follows from its definitions. It cannot prove that those definitions say what the paper or the field means by ETH.
What we checked
- Can independent complexity theorists inspect the Lean formalization and confirm that it proves the claimed deterministic 2^{o(n)} algorithm for #3-SAT? partly confirmed. Inspection is possible: the Lean 4 project is public under Apache 2.0, pins its toolchain, builds with lake, and is re-checked by Comparator and the independent nanoda kernel. Confirmation has not happened. The README says no machine checks that the Lean statements match the paper. Reporting says the Lean development was reviewed only by model instances, and no human is known to have checked it. [3][2][4]
- Is there a formal independent expert review under way, and does it cover Anthropic's proof? partly confirmed. Russell Impagliazzo and Ramamohan Paturi, two of ETH's original proposers, and Ryan Williams are organizing a review. Their open letter says their involvement 'should not be taken as certification of the claim.' The reporting presents the review mainly as a response to OpenAI's claim. It is unclear whether it formally covers Anthropic's separate proof. [5][4]
What we found
- The Hexagon record lists no individual human authors. It is 'Contributed by Anthropic,' marked 'Primarily AI-generated text,' with 'Human understanding: some parts.' The provenance gives 16 October as the discovery date and 14M output tokens with no human input. The record also cites OpenAI's concurrent, unverified preprint claiming a similar result. [1]
- The Lean project came in through PR #31 in anthropics/formal-math, opened and merged on 27 October 2026 (merge commit 16a5ce4). It is a self-contained Lake project pinned to Lean and Mathlib v4.33.1. The PR has no substantive review discussion beyond one approval. [2]
- The README says MainResults.lean states two propositions on Mathlib's Turing machines: ETHIsFalse, and a MainTheorem that counts satisfying assignments of k-CNF formulas in 2^{O(n log log n / √log n)} time. It says both depend only on Lean's three standard axioms (propext, Classical.choice, Quot.sound). The two 'sorry' warnings come from Challenge.lean, which states the theorems without proof for the Comparator check. CI re-checks the proofs with the independent nanoda kernel. A local build takes about 8 minutes on 24 vCPUs. [3]
- The README is explicit about the main gap. Lean checks the proofs, but 'no machine checks' that the formal statements match the paper. Checking that relies on Appendix E of the paper and on proof/PaperIndex.lean. The README also calls the result purely asymptotic, saying it 'says nothing about solving formulas in practice.' It states that the formalization was written by AI models. [3]
- Tech Times reports that Anthropic's paper says the Lean development was reviewed only by other instances of the same models, and that no person is known to have checked it by hand. Jelani Nelson, who read Claude's proof before release, is reported to say that both labs' proofs reach roughly exp(O(n/√log n)) time. Nelson joined Anthropic earlier this year, so he is not an outside reviewer. [4]
- Impagliazzo and Paturi of UC San Diego and Ryan Williams of MIT are organizing an open examination. They are reportedly unpaid and signed no NDAs. They wrote that their involvement 'should not be taken as certification of the claim.' The questions they list include whether the Lean statement matches the real ETH in input encoding, machine model and how running time is counted. [5][4]
- John D. Cook's blog notes that Shiva Kintali has posted a simplified exposition of OpenAI's proof, not Anthropic's. It also relays a comment that the Lean-formalized statement there is slightly weaker than the paper's claim but still subexponential. I could not extract the text of Kintali's PDF, so this rests on Cook's summary. Refuting ETH would not settle P vs NP. [6][7]
What it means
For now, treat the result as a strong but unconfirmed claim. Several things are solid: the artifacts are public, the proof checks in two independent kernels, and no axioms beyond Lean's standard three are used. That rules out a lot of failure modes, including hidden 'sorry's and custom axioms. The remaining risk sits in the specification: whether ETH, encoded on Mathlib's Turing machines with a particular input encoding and time accounting, is the ETH that hundreds of papers rely on. Only humans are currently in a position to answer that, and none outside Anthropic has reported doing so. Teams building AI-for-math pipelines can take away a general pattern: a public, toolchain-pinned repository, a second-kernel recheck, an axiom audit, and a statement-to-paper index (PaperIndex.lean) together make a reasonable bar for releasing machine-found theorems. A human audit of the statements is still the step that turns 'verified' into 'true.'
In practice, nothing changes for SAT solving. The bound is asymptotic, and the README says it has no practical consequence. If you depend on ETH-based hardness arguments in parameterized complexity or fine-grained reductions, mark them as pending rather than rewriting anything yet. Two independently developed proofs reportedly landing on similar bounds is suggestive, but it is not proof. Watch for output from the Impagliazzo–Paturi–Williams review, and for any explicit statement that it covers Anthropic's proof as well as OpenAI's.
Still open
- Has any complexity theorist outside Anthropic audited MainResults.lean against the standard definition of ETH, including input encoding, machine model and time accounting?
- Does the Impagliazzo–Paturi–Williams review formally include Anthropic's proof, or only OpenAI's?
- How far apart are the Lean-formalized bounds and the paper's stated bounds in Anthropic's version, as documented in Appendix E?
- Are Anthropic's and OpenAI's techniques actually distinct, or variants of one underlying idea?