ETH false, a second time? Claude’s 2^o(n) algorithm for 3-SAT

The claim, in plain words

The paper’s author line reads Claude, Anthropic. It has 49 pages, is dated October 26, 2026, and was posted on GitHub that evening, Pacific time, with a Lean proof. The paper says the core algorithm was found on October 16 by an internal Claude research model, with 14 million output tokens and no human input, and that Anthropic researchers then worked with Claude on the presentation. The main theorem: a deterministic algorithm counts the satisfying assignments of a k-SAT formula in time 2 to the power C·min{k²n log log n/√(log n), km/√(log m)}. The constant does not depend on k. Divided by n, for each fixed k, the exponent goes to zero, so the paper concludes that the hypothesis, and its strong version, are false.

Beside OpenAI’s paper (episode 378)

Beside OpenAI’s paper from episode 378, dated October 17 and revised October 25: both claim a deterministic algorithm that counts solutions, with the same growth in n, n log log n/√(log n). OpenAI’s holds for each fixed k, with a constant that depends on k, and in polynomial space. Anthropic’s makes the dependence on k explicit, adds a bound in the number of clauses, and states no space bound. For circuits, OpenAI derives a lower bound of order n√(log n) for a language in E^NP; Anthropic derives that this class has no circuits of linear size, which OpenAI’s bound implies. Anthropic’s paper says that, independently and concurrently, an internal model at OpenAI claims to have proven a similar result. OpenAI’s paper does not mention Anthropic; its last revision is dated the day before. We make no judgement on priority: these dates are each lab’s own, and OpenAI’s paper gives no date of discovery.

Our reading of the two overviews, not a comparison of the full proofs: both reach their sharpest bounds by recursive contraction of tensor networks (OpenAI in its Appendix D), but the step that removes the bits crossing between groups looks different: Anthropic’s paper rewrites two crossing equality tests with the eight-square identity and merges rows or columns; OpenAI’s main text deforms the clause polynomials and interpolates. We make no judgement on priority: the dates above are as each source gives them, and Anthropic’s paper says the core algorithm was found on October 16.

What it doesn’t claim

What is not claimed. The paper calls its result purely asymptotic. For formulas with five clauses per variable, its bound cannot beat the 2^n of trying every setting unless n is more than 10^10,000; the bound in n alone, not unless n is beyond 10^(10^8). The paper says its result says nothing about solving formulas in practice. It does not bear on P versus NP directly. It does not refute the Orthogonal Vectors hypothesis. And the proof does not give the value of the constant.

The paper also says its “general approach seems unlikely to yield any general improvement unless n > 10⁷, however it is instantiated”, and that its result “does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems”.

Where it stands

Paper public

On GitHub (anthropics/formal-math, folder eth; added October 26, 2026, 20:07 Pacific time); dated October 26, 2026; 49 pages. Not on arXiv; the README says “Hexagon link to appear”. We found no Anthropic blog post

Peer review

None yet

Independent expert review

None named in our sources. The open letter of Russell Impagliazzo, Ramamohan Paturi and Ryan Williams concerns OpenAI’s claim (“OpenAI has informed us that it has obtained a claimed refutation of the Exponential Time Hypothesis”); it says “Our involvement should not be taken as certification of the claim”, and its list of resources ends with “Anthropic: Refutation of ETH”, linking this paper’s folder. Lance Fortnow (October 28): “Later Anthropic released their own paper. … I have not verified the proof myself, but it is safe to assume now that the exponential-time hypothesis is toast.”

Lean, by Anthropic

MainResults.lean states ETHIsFalse and the full Main Theorem on Mathlib’s Turing machines; the comparator checks both against Challenge.lean, with the nanoda kernel; the README reports only Lean’s standard axioms, and the repository’s CI check passed on the commit. The paper: “The Lean development was written by AI models and reviewed by other instances of the same models; at the time of writing no person is known to have checked it; its constant is not explicit.” Two steps (writing the formula as the machine’s input, and simulating the machine on a word RAM) are outside the Lean proof. Not built or run by us. A commenter on the working group’s blog reports replaying both labs’ Lean with the comparator (Carlos Toledo, October 28; not checked by us)

Last checked November 4, 2026. Where it stands. The paper is on GitHub, not on arXiv. It is not peer reviewed, and no independent expert review of it is named in our sources. Impagliazzo, Paturi and Ryan Williams wrote an open letter about OpenAI’s claim, saying: our involvement should not be taken as certification of the claim. The letter’s resources include Anthropic’s paper. Lance Fortnow wrote on his blog, mainly about OpenAI’s paper: I have not verified the proof myself, but it is safe to assume now that the exponential-time hypothesis is toast. The Lean proof, not run by us, states that the hypothesis is false and the full main theorem; OpenAI’s Lean covers a slightly weaker bound. But the paper says the Lean was written by AI models and reviewed by other instances of the same models, and that no person is known to have checked it. It names no person who checked the printed proof either.

If it holds, the Exponential Time Hypothesis is false, in two papers from two labs released the same day, and results that rest only on it lose that support. By the paper’s own account, nothing changes for formulas of any size met in practice.

How the proof goes

1. The question. Trying every setting takes 2^n steps. The best earlier algorithms the paper cites take about 1.3^n. They lower the rate, the number multiplying n in the exponent of two, but keep it above zero. The Exponential Time Hypothesis, of Impagliazzo and Paturi, says that some positive rate is unavoidable for 3-SAT, and many lower bounds were proved assuming it. Episode 378 covered OpenAI’s paper claiming the hypothesis is false. This is a second paper, from Anthropic, claiming the same.
2. Cuts. How the proof goes, in the paper’s overview. The count is a sum, over all settings, of a product of local factors on the graph. With few bits crossing a cut, one can try every value of those bits and solve the two halves separately. But for formulas such as random ones, every cut into two parts of comparable size is crossed by a number of bits proportional to n. Cutting alone improves only the constant.
3. The new step. The new step rewrites edges. Place the nodes on a grid. In each rectangle of four nodes, the two diagonals test that strings of three bits agree. The eight-square identity, two centuries old by the paper’s account, rewrites twice that pair of tests as a parity check on the four corners times a sum of two sign terms. Our computer confirms it at all 4,096 settings. Then the algorithm merges whole rows, or whole columns. Merged by rows, one term costs 3 bits and the other 6; the diagonals cost 6. With the terms grouped as the paper does, rows plus columns cost 11 bits per block, against 12, so the cheaper side carries at most 11/12.
4. The recursion. Each level of the recursion does this, regroups the nodes into balanced groups, and calls the level below. In the paper’s recurrence, the exponent per bit on the edges is 1.03 at level 1, as the paper says; our computer gets below one half at level 10, and below one tenth at level 28. So every positive rate is beaten at some fixed level. The sharper main theorem needs further ideas, in the appendices. Our reading of the two papers: both reach their sharpest bounds by recursive tensor network contraction, OpenAI’s in its Appendix D, but the step that removes crossing bits looks different, a sign identity here, deformation and interpolation in OpenAI’s. We have not compared the full proofs.

The numbers in the video

• Ours: the paper’s Figure 1 formula (5 clauses on 7 variables): 56 of 128 settings satisfy; chaining each variable’s occurrences gives 8 edge bits, as in the figure.
• Ours: the eight-square identity, with the paper’s sign function σ, holds at all 4096 settings of x, y, u, v (σ is not symmetric: σ(p, q) ≠ σ(q, p) for 42 of 64 pairs).
• Ours, from the paper’s recurrence (9): the rate is 1.026 at level 1, below 1/2 from level 10, below 0.1 from level 28; it stays below the paper’s bound 1.12·(11/12)^ℓ.
• From the paper: earlier bounds O(1.328^n) deterministic [Liu18] and O(1.308^n) randomized (rates 0.41 and 0.39, ours); the bound beats 2^n only for n above 10^10,000 when m = 5n, and for the bound in n alone only above 10^(10^8).
• Ours: a text scan of the eth folder: 1050 Lean files (151,900 lines) besides two scripts; sorry only in Challenge.lean; no axiom declarations. We did not build or run the Lean.

Read the source

• Claude (Anthropic), “A 2^o(n) Time Algorithm for 3-SAT”, dated October 26, 2026, 49 pages; the folder with the Lean proof (Apache-2.0; commit 16a5ce4).
• OpenAI, “The Exponential Time Hypothesis is False” (openai/math, result 378; dated October 17, revised October 25, 2026); our episode 378.
• Impagliazzo, Paturi and Williams, open letter and discussion blog; Lance Fortnow, “The Exponential Time Refutation” (October 28, 2026).

AI Proved What? is independent and not affiliated with Anthropic beyond using its product Claude, or with OpenAI.

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.