Skip to content

The ETH refutation and what it means for algebra research in complexity

On 26 and 27 October 2026 (UTC), six hours apart, OpenAI and Anthropic each released a preprint claiming that the Exponential Time Hypothesis (ETH) is false: there is a deterministic algorithm that counts the satisfying assignments of a 3-CNF on \(n\) variables in time \(2^{o(n)}\), which refutes ETH because counting decides. Each paper was written by an internal model, each comes with a Lean 4 formalization of its theorem, and neither is refereed. This post says what the two papers claim and how, who can check what, what the Lean files state and what no machine checks, and then whether the claims, if they stand, would change anything for the algebraic approach to complexity. By that I mean the approach to constraint satisfaction built on polymorphisms and clones, the field I work in, not Valiant's algebraic complexity of circuits and tensors; the distinction turns out to matter, since the two algorithms are algebraic in Valiant's sense and not in mine. The short version: the formal theorems are checked by Lean's kernel against statement files, the prose proofs are refereed by nobody yet, and whether the statements say what the papers mean is for human readers, one of whom reports below; the algebraic theory classifies problems up to polynomial time, so almost none of it moves; its fine-grained branch loses the separations it proved under ETH and sees its open question move to a finer scale; and the form of the Strong Exponential Time Hypothesis that most fine-grained lower bounds actually use survives.

How this post was written

I prepared this post with Claude (Anthropic) as a reading assistant, two days after the second release. Claude Fable 5.1 read Sections 1, 2 and 7 and Appendices E and G of Anthropic's paper and Sections 1 and 2 and Appendices C and D of OpenAI's, read both Lean statement files whole, checked every consequence stated here against its primary source, worked the template encoding of the section on finite templates on small examples by brute force, and drafted this text and its figures. A second model instance then read the draft as a complexity theorist from outside constraint satisfaction, and its report changed the text in a dozen places. Where this post calls something checked, it means that reading. Nobody here checked either paper's proof, and as far as I know nobody outside the two labs has yet. The status of the claims is as of 29 October 2026.

The post is written in layers: a one-minute summary, the two papers and the idea of each, who can check what, the Lean files, what does not change, what changes, the question this leaves for algebra, and what would settle the claims. Stop wherever you have what you need.

The one-minute version

Two preprints claim the same theorem by different methods. OpenAI's, dated 17 October and revised 25 October, was released on 26 October; Anthropic's, dated 26 October, early on 27 October UTC, and its paper says the two results were found independently and concurrently. Both count the satisfying assignments of a \(k\)-CNF, for fixed \(k\), in time \(2^{o(n)}\), deterministically, and both prove their sharpest bounds by contracting tensor networks. Each states a theorem in Lean 4 (Anthropic its main theorem, OpenAI a weaker bound from the same paper) and checks the proof against that statement with Comparator, a tool that compares a proof's theorems with a separately written statement file. Neither has been refereed, and OpenAI's release history names a working group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams that will examine the proof.

In one line each, as the evidence stands today:

  • The formal theorems are machine-checked; the proofs in the papers are checked by nobody yet. Lean's kernel accepts both proofs against their statement files, and a second kernel accepts Anthropic's. What no machine checks is that the statement files say what the papers mean, and no referee has read either prose proof.
  • Anthropic's Lean statement of ETH is Impagliazzo and Paturi's, up to the model of computation, which is fixed so that the Lean claim is the stronger one to refute. That is my reading of the file, reported below.
  • Above polynomial time, nothing moves. The dichotomy theorems, the counting dichotomy, the NP-hardness of promise CSPs, the unconditional lower bounds against restricted models, and P versus NP are untouched.
  • Below it, the fine-grained branch moves. Every finite-template CSP, counting CSP and promise CSP becomes solvable in time \(2^{o(n)}\) times a polynomial, the separations the fine-grained theory proved under ETH are gone, and its open question moves from exponential rates to subexponential ones. The Orthogonal Vectors conjecture and the unbounded-width form of SETH survive, and most fine-grained lower bounds rest on those.
  • The algorithms are algebraic in Valiant's sense. Tensor contraction, rank and polynomial interpolation drive both; neither looks at a template's polymorphisms, the operations that preserve its relations.

The two papers and the idea of each

OpenAI Claude (Anthropic)
Paper The Exponential Time Hypothesis is False, 67 pages, dated 17 October, revised 25 October A \(2^{o(n)}\) Time Algorithm for 3-SAT, 49 pages, dated 26 October
Released 26 October 2026, 20:52 UTC 27 October 2026, 03:07 UTC (26 October in US time)
Main theorem For each fixed \(k \ge 2\), a deterministic algorithm counts the solutions of a \(k\)-CNF with \(n \ge 20\) variables and \(m\) clauses in time \((n+m)^{O(1)} \, 2^{O(n \log\log n / \sqrt{\log n})}\) and polynomial space, the constants depending on \(k\); in time \(2^{O(n/\sqrt{\log n})}\) when \(m \le Dn\). Smaller \(n\) are finitely many and searched exhaustively One deterministic algorithm, for every \(k\), counts the solutions of a \(k\)-CNF in time \(2^{O(\min\{k^2 n \log\log n / \sqrt{\log n},\; km/\sqrt{\log m}\})}\), with an absolute constant
Main argument Interpolation in an auxiliary parameter, which gives the weaker exponent \(n(\log\log n)^2/\sqrt{\log n}\) A signed expansion of two crossing equality tests into terms of low rank, the direction chosen term by term, recursed
Sharpest bounds by Tensor contraction, Appendix D Tensor contraction with operators on a polynomial ring, Appendices A, B and D
Hypotheses refuted, by its own account ETH, SETH, Gap-ETH, NSETH, #ETH ETH, SETH, NSETH, #ETH
In Lean exact_count_and_sat: one machine for each \(k\), with the weaker exponent; Comparator without a second kernel ETHIsFalse and MainTheorem over Mathlib's multi-stack Turing machines; Comparator with a second kernel, nanoda
Review A working group led by Impagliazzo, Paturi and Williams will examine the proof The Lean development was reviewed by AI models; no person is known to have checked it
What it disclaims Bounds of the form \(2^{o(n)}\) do not transfer through polynomial-time reductions The result does not bear on P versus NP directly; it is purely asymptotic and yields no practical algorithm

Why both papers count rather than decide

Both algorithms compute the number of satisfying assignments and read off satisfiability as "is the count positive". The count is a sum over all \(2^n\) assignments of a product of clause indicators, and a sum of products is the object these methods rearrange, as a polynomial to interpolate or as a tensor network to contract. Deciding is a disjunction over the same assignments, and for these methods it is no cheaper than the exact sum. Counting costs the papers one thing: the sparsification lemma of Impagliazzo, Paturi and Zane, which both use to reduce to formulas with linearly many clauses, has to be taken in the version of Dell, Husfeldt, Marx, Taslaman and Wahlén that partitions the satisfying assignments, so that counts add rather than overlap.

E1 = (x1 ∨ x2 ∨ ¬x3) E2 = (¬x1 ∨ x3 ∨ x4) E3 = (x2 ∨ ¬x4 ∨ x5) E4 = (x5 ∨ x6 ∨ ¬x7) its graph: a node per clause, an edge per shared variable E1 E2 E3 E4 x1, x3: 2 bits x2: 1 bit x4: 1 bit x5: 1 bit a cut: 2 bits cross it The count is a sum of products count = Σ over assignments Π over clauses [clause true] a tensor per clause, an equality test per edge: a network, and the count is its contraction deciding asks whether the count is positive Divide and conquer, the classical way fix the bits crossing the cut, here x2 and x4: 4 cases count = Σ over the cases of Nleft · Nright cost 2crossing bits times the two halves, recursively on an expander every balanced cut is crossed by Ω(n) bits, so a fixed tree of cuts costs 2Ω(n); both papers do more
A formula as a graph, and why both papers count. Each clause is a node and each shared variable an edge carrying one bit, which is Anthropic's picture; OpenAI's tensor network puts a tensor at each clause and an equality tensor on each variable, and the two are the same object. The count is the contraction of the network. Cutting the graph and enumerating the bits that cross is the classical divide and conquer, and on expander formulas every balanced cut carries Ω(n) bits; that is the wall both papers get around, one by interpolation and one by a signed expansion of crossing edges.

OpenAI's idea: interpolate, then contract

Write the count as \(\sum_{x \in \{0,1\}^n} \prod_e \Phi_e(x)\), where \(\Phi_e\) is the clause polynomial that is \(1\) on satisfying assignments of clause \(e\) and \(0\) otherwise. After sparsification and Tovey's variable-copying trick, every variable occurs in at most three clauses; each occurrence contributes degree one, so the product has degree at most \(3n\). If the variables could be split into groups with no clause crossing a group, the sum would factor and each group could be enumerated separately. They cannot be, so the paper interpolates in an auxiliary parameter: it replaces each variable occurrence by a linear form, depending polynomially on the parameter, in a few shared integer measurements, arranged so that at special parameter values, once the measurements are fixed, the summand does factor over groups; the count is then recovered from Taylor coefficients at those values by Hermite interpolation. That is the shape of Sections 3 to 6, and it gives the exponent \(n(\log\log n)^2/\sqrt{\log n}\). Appendix D abandons the global interpolation for a recursion on the wires of a Boolean tensor network. Its Theorem D.1 is a general statement, and a headline of its own if it holds: a bipartite network on at most \(Cs\) edges, with vertex degree at most \(\lceil s^{9/10} \rceil\), polynomially many vertices, and entries in a fixed truncated ring, each computable from the network's description, of length \(L\), in time \((s+L)^{O(1)} \, 2^{O(s^{9/10})}\) and space polynomial in \(s + L\), contracts in time \((s+L)^{O(1)} \, 2^{O(s/\sqrt{\log s})}\) and space polynomial in \(s + L\). The paper's Corollary 1.3 draws from it what such a theorem must give: the number of independent sets and of proper \(q\)-colorings of a graph in time \(2^{o(v)}\), and the number of perfect matchings in time \(2^{o(v+e)}\).

Start: the count as a sum over all assignments each clause is a polynomial Φe: 1 on the assignments that satisfy it, else 0; the count is Σx Πe Φe(x), a product of degree at most 3n, since every variable occurs in at most three clauses. Split the variables into r groups of at most 2n/r each: the clauses that cross groups stop the sum from factoring Deform: a parameter T replace each occurrence of Xv in clause e by a linear form ⟨Pe,v(T), X⟩ with coefficients polynomial in T of degree at most R, equal to Xv at T = 0; then H(T) = Σx Πe Φe(the forms) has H(0) = count and degree at most 3nR; at T ≠ 0 a form need not be 0 or 1, and the clause polynomials stop being indicators Separate: at each point t = 1, …, Q the forms are built so that groups interact only through a few shared integer measurements y = C x; fix y and the summand factors over the groups: H(t) = Σy Πg Ng(t, y), each Ng a sum over 22n/r local assignments; the Taylor coefficients of H at t come the same way, O(1 + n R/Q) of them per point Recover: Hermite interpolation a polynomial of degree below Q·J is fixed by J Taylor coefficients at each of Q points, since the Hermite matrix is invertible; solving it gives H(0), the count; balancing r, Q and R gives the exponent n (log log n)2 / √log n. Appendix D replaces the global expansion by a recursion on the wires of a tensor network groups; dashed: a crossing clause Xv → ⟨Pe,v(T), X⟩ T = 0: the formula itself T = 1, …, Q: easier points y H(0) t = 1, …, Q
OpenAI's argument in four steps, after Sections 2.2 to 2.5 of its paper. The sum over assignments cannot be split into groups because clauses cross them; the parameter T deforms each variable occurrence into a linear form that returns the variable at T = 0; at the points t = 1, …, Q the forms are designed so that, once a few shared measurements are fixed, the sum factors over groups and each factor is a small exhaustive search; and Hermite interpolation from the Taylor coefficients at those points recovers the value at 0. The design of the forms, through a matrix M0 whose rank bounds the number of measurements, is the paper's Sections 2.7 and 4.

Anthropic's idea: a signed expansion of the swap, chosen term by term

View the formula as a graph: a node per clause, an edge per shared variable, each edge carrying one bit per variable shared. Cutting the graph and enumerating the bits that cross the cut, then recursing on the halves, is the classical divide and conquer, and on expander formulas every balanced cut is crossed by \(\Omega(n)\) bits, so any algorithm that fixes one tree of cuts takes time \(2^{\Omega(n)}\). The new move is algebraic. Place the nodes on a \(g \times g\) grid; the rows and the columns are two partitions of the nodes. Two edges that join opposite corners of a rectangle of the grid are two equality tests that cross: with \(x, y\) the strings the upper corners hold for those edges and \(u, v\) the strings the lower corners hold, the two tests read \([x = v]\,[y = u]\). On three-bit strings (eight values, the size for which the identity exists) the eight-square identity of Degen and Graves, two centuries old, gives

\[ 2\,[x = v]\,[y = u] \;=\; [x \oplus y \oplus u \oplus v = 0]\, \bigl(\sigma(x,y)\,\sigma(v,u) + \sigma(x,u)\,\sigma(v,y)\bigr), \]

with \(\sigma\) a sign taken from the multiplication table of the octonions. Merge the rows of the grid into single nodes and the first term costs three bits between the two rows where the two edges cost six; merge the columns and the second term is the cheap one. So expand the product over all rectangles, and in each term merge whichever is cheaper. Grouping the terms by how many blocks take the column choice keeps their number polynomial in the number of bits, at the price of one more bit per block in each direction: the count per block is \(3 + 6 + 1 + 1 = 11\) bits in the two directions together against \(12\), and that is the factor \(11/12\) by which each level shrinks the edge bits. Balancing the merged groups so that every edge carries about the average is proved possible by Chebyshev's inequality and done by trying every grouping, which is what forces a level to start with \(9K^{16}\) nodes and end with \(K\). For the sharpest bounds the octonion signs are replaced by operators on a graded polynomial ring, where one order of multiplication raises the degree and the other lowers it; the bits a piece costs are then logarithms of partition numbers, about \(\sqrt{\text{weight}}\) by the Hardy–Ramanujan formula, and that concavity is what brings the two directions down to \(2\sqrt{2}\,\lambda\) bits in place of \(4\lambda\). With the better balancing of Appendix A the exponent per bit then falls like \(1/\sqrt{\log K}\), and letting \(K\) grow to a power of \(m\) puts \(\sqrt{\log m}\) in the denominator. Appendix G says the paper knows no earlier use of an exact signed low-rank expansion of a crossing with a separate choice of direction for each term, combined with recursion.

The grid x y u v clause nodes on a g × g grid, placed by the algorithm; the diagonals of one rectangle test x = v and y = u: 6 bits The identity, on 3-bit strings 2 [x = v] [y = u] = [x ⊕ y ⊕ u ⊕ v = 0] · ( σ(x,y) σ(v,u) + σ(x,u) σ(v,y) ) x y u v x y u v row choice column choice σ(x,y) σ(v,u) σ(x,u) σ(v,y) the sign σ comes from the octonion multiplication table; the hyperedge, drawn as a dot, is [x ⊕ y ⊕ u ⊕ v = 0] on all four Bits a rectangle costs rows merged columns merged two diagonals 6 6 row choice 3 6 column choice 6 3 Expand over all rectangles; in each term merge the rows if row choices are the majority, else the columns. Then no rectangle costs more than 6 bits and half cost 3: 6|R| falls to at most 4.5|R|. Grouping the terms by their number of column choices keeps them polynomial, at one more bit per block each way: 11 bits in place of 12, the factor each level gains.
Anthropic's move, after Sections 2.4 and 2.5 of its paper. The algorithm places the clause nodes on a grid of its own choosing; the two diagonals of a rectangle are two equality tests that cross, and the eight-square identity of Degen and Graves writes twice their product as a hyperedge on the four corners times a sum of two signed terms. Merging the rows makes the row-choice term cost three bits where the diagonals cost six, and merging the columns does the same for the column-choice term; expanding over all rectangles and merging each term the cheaper way cuts the edge bits by a constant factor at every level, which no fixed tree of cuts can do on an expander. The table is the case of 3-bit strings; longer strings are handled in blocks of three.

Who can check what

  • A complexity theorist, in a few days: the statements, the consequences (Anthropic's Section 7, OpenAI's Appendix C), the sparsification steps, and the application of Williams's theorem. All of it is standard material applied once.
  • A specialist in algebraic algorithms or tensor networks, in weeks: OpenAI's Sections 3 to 6 and Appendix D, and Anthropic's Sections 3 to 6 and Appendices A, B and D. Anthropic's Appendix C, the sparsification step with a parameter that tends to zero, is marked a proof sketch; its Lean counterpart proves that step in full by its own analysis, so the gap is in the prose, not in the formal theorem.
  • A Lean reader, in a day: the two statement files, each a page or so of definitions. This is the one check that needs no expertise in the proofs, and the reading reported below is of that kind.
  • The working group: whatever it reports. Its three leaders have said, in an open letter reported in the press, that their involvement should not be taken as a certification of the claim.

What the Lean files state, and what no machine checks

The two releases share a discipline. A short statement file fixes the claim; the proof lives elsewhere and is checked against the statement by Comparator, which matches a challenge file, in which the theorems carry sorry, against the solution's theorems of the same names and types, and re-checks the proof under the permitted axioms. Both permit only Lean's three standard axioms, propext, Quot.sound and Classical.choice. Anthropic's configuration also enables nanoda, a kernel written independently of Lean's; OpenAI's does not.

The object Who checks it Where it is The paper: a prose proof 67 and 49 pages, written by a model; neither is refereed Nobody yet a working group will examine OpenAI's; Anthropic's names none the preprint in openai/math paper.pdf in formal-math The proof: Lean 4 files every step is a term the kernel checks; OpenAI's: the weaker bound only Lean's kernel, and Comparator Comparator matches each theorem's name and type to the challenge and allows three axioms; Anthropic adds nanoda, a second kernel OAI/Algorithms/SubexponentialSAT Solution.lean and the proof tree The statement file definitions, then the claims as theorems whose proofs are sorry A human reader does the file say what the paper means? No machine can check this; one reading is reported below SubexponentialSAT.lean (challenge) MainResults.lean and Challenge.lean formalized as checked against
What is checked, and by whom. The kernel checks the proof files against the statement file, Comparator checks that the theorems proved carry the names and types of the challenge and that only the three standard axioms were used, and nanoda, for Anthropic, repeats the kernel's check in an independent implementation. Whether the statement file says what the paper means is the one link no machine checks, and the paper's prose proof, which the Lean proofs formalize, Anthropic's whole and OpenAI's for its weaker bound, has no referee yet. In the right column the first line of each box is OpenAI's file, in openai/math, and the second Anthropic's, in its formal-math repository; the Sources give the paths.

Anthropic's file. MainResults.lean imports Mathlib and nothing else and contains definitions only. A literal is a pair in Fin n × Bool, a clause a list of literals, a formula a list of clauses with no clause written twice and each clause of length at most \(k\). An algorithm is one of Mathlib's deterministic multi-stack machines, Turing.FinTM2, with every stack alphabet finite; time is the number of steps. InTime k δ says that one machine and one constant \(c\) decide \(k\)-SAT within \(\lfloor c \cdot 2^{\delta n} \rfloor\) steps for every \(n\), on an input word that writes \(n\) in unary and then each clause in \(k\) fixed-width slots. Then \(s_k\) is the infimum of the \(\delta\) with InTime k δ, taken in the extended nonnegative reals, ETH is \(0 < s_3\), and ETHIsFalse is its negation. MainTheorem asks for one machine and one constant \(C\), chosen before \(k\), such that for every \(k \ge 1\), every \(n \ge 4\), every \(m \ge 2\) and every such formula in which every variable occurs, the machine outputs the count within \(2^{C \min\{km/\sqrt{\log m},\; k^2 n \log\log n/\sqrt{\log n}\}}\) steps. Challenge.lean states both as theorems with sorry, and comparator.json names them.

OpenAI's file. SubexponentialSAT.lean defines its own machine, a multitape Turing machine over the alphabet Option Bool whose states each scan one tape, with a located configuration that tracks the cells visited, so that the space bound can be stated. A formula is a Finset of Finsets of literals, so a repeated clause cannot occur. The theorem, exact_count_and_sat, quantifies over \(k \ge 2\) first and asks for a machine second: one machine for each \(k\), as in the paper. It outputs the count in binary and the decision bit, runs within \(C (L+1)^d \, 2^{A \, n (\log\log(n+16))^2/\sqrt{\log(n+16)}}\) steps with \(L\) the input length and natural logarithms, and visits at most \(S (L+1)^e\) cells at every prefix of its run. That is the paper's weaker exponent, from the interpolation argument, with the polynomial-space clause included; the sharper bounds of Appendix D, and the circuit lower bound drawn from them below, are not in Lean. The full proof is in the repository, under OAI/Algorithms/SubexponentialSAT.

A reading of my own: is the Lean ETH Impagliazzo and Paturi's?

Impagliazzo and Paturi define \(s_k\) as the infimum of the \(\delta\) for which some algorithm solves \(k\)-SAT in time \(O(2^{\delta n})\), and ETH as \(s_k > 0\) for \(k \ge 3\); their Theorem 1 makes this equivalent to \(s_3 > 0\). I compared that with MainResults.lean clause by clause.

  • The number. Lean's \(s_3\) is the same infimum, over \(\delta \ge 0\), with the \(O(\cdot)\) written out as one constant \(c\) and the bound asked of every \(n\). Since no clause is written twice, a \(k\)-CNF on \(n\) variables has at most \((2n+1)^k\) clauses, so there are finitely many formulas for each \(n\) and a free \(c\) makes "every \(n\)" the same as "all large \(n\)". The infimum is taken in \([0, \infty]\), so with no such algorithm at all it is \(\infty\) and Lean's ETH holds, as it should.
  • The model of computation. Impagliazzo and Paturi say "algorithm"; Lean says a multi-stack machine with finite alphabets, and counts the reading of the input. A random-access machine simulates such a machine with a bounded number of operations per step, and rewrites a 3-CNF into the input word in polynomial time, so the usual \(s_3\) is at most Lean's. Hence Lean's \(s_3 = 0\) gives the usual \(s_3 = 0\): the model is fixed in the direction that makes the Lean claim the stronger one to refute. The reverse simulation, of a random-access machine by a multi-stack machine, is standard too, but its polynomial overhead turns a time of \(2^{\delta n}\) into \(2^{O(\delta n)}\), so it shows that the two numbers vanish together, not that they agree. Neither simulation is in Lean, and the file's head comment argues only the direction the refutation needs.
  • The formula. Lean's clauses are lists, so a clause may be empty, may repeat a literal, and the same literals in another order make another clause; the only restriction is that no clause is written twice. Every 3-CNF in the usual sense is such a formula after removing repeats, in polynomial time. The variables are \(x_0\) to \(x_{n-1}\), any number of clauses, and \(k\) is fixed outside the input, which is how the paper reads "3-SAT on \(n\) variables".
  • Determinism. Impagliazzo and Paturi do not say whether their algorithms may be randomized; Lean's machine is deterministic. Refuting the deterministic form refutes the randomized one.
  • What the Main Theorem leaves out. Its hypotheses are a promise: \(k \ge 1\), \(n \ge 4\), \(m \ge 2\), every variable occurring, no clause repeated. The file explains each threshold (\(\log\log n\) vanishes at \(n = 2\); \(\sqrt{\log m}\) vanishes at \(m = 1\)) and says that nothing is claimed about other inputs. Each excluded case is finite or trivial, and ETHIsFalse is derived from MainTheorem inside Lean, so the exclusions do not reach the ETH statement.

What I conclude from the file: ETHIsFalse is the negation of ETH as Impagliazzo and Paturi state it, up to a model of computation whose choice goes the safe way. What this reading cannot do is check the proof behind it, and the paper's Appendix E says the limit plainly: whether the two definitions say what they are meant to say, no machine can check, and no person is known to have checked the development.

What does not change

The algebraic approach to constraint satisfaction classifies problems up to polynomial-time reductions, and ETH enters none of its theorems.

  • The dichotomy theorem. Bulatov's and Zhuk's theorem says that the CSP of a finite template is in P or NP-complete, and the template's polymorphisms say which. It is a statement about polynomial time.
  • The counting dichotomy. Bulatov, and Dyer and Richerby, proved that each finite-template counting CSP is in FP or #P-complete. Same scale.
  • The hardness of promise CSPs. Barto, Bulín, Krokhin and Opršal prove NP-hardness through minion homomorphisms, which are polynomial-time reductions, and approximate graph coloring stays open.
  • Lower bounds against restricted models. Bounded width, levels of the Sherali–Adams and affine hierarchies, and proof systems such as resolution keep their unconditional lower bounds. A fast algorithm need not yield short refutations, and OpenAI's paper says so for a reader who might expect otherwise: its result does not conflict with the exponential lower bounds for regular resolution.
  • P versus NP. Both papers prove bounds that are superpolynomial, so neither puts 3-SAT in P. Anthropic's paper says the result does not bear on P versus NP directly; OpenAI's says that bounds of the form \(2^{o(n)}\) do not transfer through polynomial-time reductions, so NP as a whole gains no subexponential algorithm. What does transfer is anything with a linear-size reduction to fixed-width SAT: Anthropic's Corollary 7 lists Independent Set, Clique, Vertex Cover, Dominating Set and \(k\)-Coloring on \(n\) vertices, counts included, in time \(O(2^{\delta n})\) for every \(\delta > 0\). A caution for the reader who meets this for the first time: every polynomial is itself \(2^{o(n)}\), so "\(2^{o(n)}\)" by itself says nothing about being superpolynomial. It is the proved bounds, with \(\sqrt{\log n}\) in the denominator of the exponent, that are.

What changes

Every finite template becomes subexponential

Neither paper says anything about templates; both encode graph colorings with one Boolean variable per vertex and color. The step from Boolean SAT to a finite template is a binary encoding, tighter than one-hot. Let \(A\) be a template on \(d\) elements whose relations have arity at most \(r\), and let an instance have \(n\) variables. Give each variable \(\lceil \log_2 d \rceil\) Boolean bits, forbid each unused code with one clause per variable, and for each constraint forbid each tuple outside its relation with one clause on the bits of its scope. The result is a CNF on \(n \lceil \log_2 d \rceil\) variables, of width \(r \lceil \log_2 d \rceil\), whose satisfying assignments correspond one to one with the solutions of the instance; I confirmed the correspondence by brute force on a few small instances, 3-colorings and a ternary relation over five elements. So if either theorem stands, \(\mathrm{CSP}(A)\) and its counting version take time \(2^{o(n)}\) times a polynomial for every finite template, and so does every promise CSP \(\mathrm{PCSP}(A, B)\), which reduces to \(\mathrm{CSP}(A)\) by the identity on instances. For Boolean templates no encoding is needed: OpenAI's Corollary C.2 counts the preimages of a Boolean map each of whose outputs reads a bounded number of inputs, and a Boolean CSP instance is such a map with one output per constraint. The corollary states the weaker exponent, though its proof applies Theorem 1.1.

A variable over d = 3 values 0 → 00 1 → 01 2 → 10 the code 11 is forbidden by one clause: (¬v1 ∨ ¬v0) v w z the instance: a triangle to 3-color A constraint v ≠ w one clause per pair outside the relation: (0,0): (v1 ∨ v0 ∨ w1 ∨ w0) (1,1): (v1 ∨ ¬v0 ∨ w1 ∨ ¬w0) (2,2): (¬v1 ∨ v0 ∨ ¬w1 ∨ w0) width r ⌈log2 d⌉ = 2 · 2 = 4 a solution of the instance ↔ a satisfying assignment of the formula, one to one the triangle: 6 Boolean variables, 3 + 9 = 12 clauses of width at most 4, 6 satisfying assignments for 6 colorings (checked by brute force) In general n ⌈log2 d⌉ Boolean variables width r ⌈log2 d⌉ solutions and assignments in bijection If either theorem stands CSP(A) and its counting version, for every finite template A, in time 2o(n) times a polynomial and every PCSP(A, B) with them, by the identity map on instances
The binary encoding of a finite template, on the smallest example. A domain of d elements takes ⌈log2 d⌉ bits per variable, one clause forbids each unused code, and each constraint becomes one clause per tuple outside its relation, so the formula has n⌈log2 d⌉ variables and width r⌈log2 d⌉, and its satisfying assignments match the instance's solutions one to one. The box on the right is the only consequence this post draws for templates, and it holds only if a theorem does.

The clone theory of exact complexity

Three words first. A polymorphism of a template is an operation on its domain that preserves every relation of the template; the polymorphisms form a clone, a set of operations closed under composition and containing the projections, and the smaller the clone the more relations the template can express, so the harder its CSP. That is the Galois connection the whole algebraic approach rests on, and it classifies up to polynomial time. A strong partial clone is the same thing for partial operations, and it is finer: it classifies up to reductions that keep the number of variables.

Jonsson, Lagerkvist, Nordh and Zanuttini studied the exact complexity of Boolean \(\mathrm{SAT}(S)\), the CSP of a finite set \(S\) of Boolean relations, under reductions that add a constant number of variables (CV-reductions) or multiply it by a constant (LV-reductions). Write \(T(S)\) for the infimum of the \(c\) such that \(\mathrm{SAT}(S)\) is solvable in time \(O(2^{cn})\); \(\mathrm{SAT}(S)\) is subexponential when \(T(S) = 0\), and ETH says that \(T(\Gamma_{3\mathrm{SAT}}) > 0\). Their Theorem 14 is the algebra: if every partial polymorphism of \(S_2\) is one of \(S_1\), then \(S_1\) expresses no more than \(S_2\) without new variables, so \(\mathrm{SAT}(S_1)\) CV-reduces to \(\mathrm{SAT}(S_2)\) and \(T(S_1) \le T(S_2)\). The lattice of strong partial clones thus orders the NP-complete problems by \(T\), and they found its least element, a problem they call strictly easier than 1-in-3-SAT. Their Theorem 51, proved by sparsification between languages, says that ETH is false if and only if one, or equivalently every, NP-complete \(\mathrm{SAT}(S)\) with \(S\) finite is subexponential, degree-bounded versions included.

If ETH fails, read that theorem forward: \(T(S) = 0\) for every NP-complete finite \(S\). Three things follow for the theory.

  • The order survives. Theorem 14 is a reduction, and a reduction that adds a constant number of variables bounds the rates one way whatever the rates are. The strong partial clone lattice still orders the problems; it no longer separates them at this scale.
  • The strict separations go. The paper's "strictly easier", \(T(S) < T(S')\), needs a problem that is not subexponential, as it notes itself after its Definition 3, so every strict separation it proves is conditional on ETH, the abstract's "strictly easier than 1-in-3-SAT" included. All of them collapse to \(0 = 0\).
  • The question moves. The paper remarks that the complexity of \(\mathrm{SAT}(S)\) is already determined by the frozen partial clones of Nordh and Zanuttini, a coarser lattice in which only variables whose value is forced may be introduced, and it asks for strict separations among the easiest NP-complete problems. Posed at exponential rates, that question is now answered with "none". Posed one scale down it is open: do distinct frozen partial clones force different subexponential rates, in the sense that some \(\mathrm{SAT}(S)\) is solvable in time \(2^{f(n)}\) and some \(\mathrm{SAT}(S')\) is not, for an \(f\) that LV-reductions preserve up to a constant factor in \(n\)? The papers give one upper bound that every NP-complete Boolean \(S\) now shares: exponent \(O(n \log\log n/\sqrt{\log n})\) in general, and \(O(n/\sqrt{\log n})\) when the number of constraints is linear in \(n\).
The order by strong partial clones harder every other NP-complete SAT(S), S finite; k-SAT and monotone 1-in-k-SAT are a clone for each k 1-in-3-SAT the easiest NP-complete SAT(S): a single 6-ary relation of 3 tuples reduces to Under ETH T(S) 0 T(easiest) > 0 T(1-in-3-SAT) = 2 T(easiest) a strict separation the rest: ordered along reductions, T(S1) ≤ T(S2) If ETH is false (Theorem 51) T(S) every NP-complete SAT(S) has T(S) = 0 the order stays, as reductions; the question moves down a scale: rates f with time 2f(n), f(n) = o(n); do distinct frozen partial clones force different f? the papers' shared upper bound: f(n) = O(n log log n / √log n), O(n/√log n) at O(n) constraints
The fine-grained theory before and after. Jonsson, Lagerkvist, Nordh and Zanuttini order the NP-complete Boolean SAT(S) problems by their strong partial clones (Theorem 14: inclusion of clones gives a reduction that adds a constant number of variables, hence T(S1) ≤ T(S2), where T(S) is the infimum of the c with SAT(S) solvable in time O(2c·n)), find a least element, a single six-ary relation with three tuples, and show that 1-in-3-SAT has exactly twice its rate, a strict separation as long as that rate is positive. If ETH fails, their Theorem 51 puts every T(S) at zero: the order remains, as reductions, and the question of separating the problems moves to the subexponential scale, where the two papers hand everything the same upper bound.

The hypotheses, and which SETH survives

NSETH k-UNSAT: no nondeterministic 2(1−ε)n SETH for every ε, some k-SAT needs 2(1−ε)n Gap-ETH gap 3-SAT needs 2Ω(n) ETH 3-SAT needs 2Ω(n): s3 > 0 #ETH counting 3-SAT solutions needs 2Ω(n) CNF-SAT, any width needs 2(1−δ)n poly(n, m) Orthogonal Vectors no N2−ε poly(d) algorithm 3SUM and APSP a separate claim of October 5 refuted by both papers, if they stand (Gap-ETH: named by OpenAI's paper only) survives: neither paper refutes it, and a result proved under it stays conditional claimed refuted by another paper, not assessed here an arrow A → B means A implies B, so refuting B refutes A; dashed arrows lead out of the refuted set
The hypotheses the papers name. SETH implies ETH (Impagliazzo and Paturi, Theorem 1, with the sparsification lemma); Gap-ETH implies ETH, since deciding 3-SAT solves the gap problem; ETH implies #ETH, since counting decides; NSETH implies SETH, since a deterministic algorithm is a nondeterministic one (Anthropic's Section 7); SETH implies its unbounded-width form, since a k-CNF is a CNF; and that form implies the Orthogonal Vectors conjecture, because Williams's 2005 reduction takes a CNF of any width to vectors of dimension m (OpenAI's paper states the implication from SETH). Both papers refute the lowest box of the middle column directly, by counting.

OpenAI's paper says it refutes ETH, SETH, Gap-ETH, NSETH and #ETH; Anthropic's states ETH, SETH, NSETH and #ETH, and reports that a literature search run by the model itself found more than 800 papers that prove at least one result only under ETH or a hypothesis that implies it. Here the fine-grained reader should ask which SETH. Impagliazzo and Paturi's is a statement about \(k\)-SAT as \(k\) grows: for every \(\varepsilon > 0\) some fixed \(k\) has no \(2^{(1-\varepsilon)n}\) algorithm. Much of the fine-grained literature uses instead the hypothesis that CNF-SAT with clauses of unbounded width and polynomially many clauses has no \(2^{(1-\delta)n}\) algorithm, often under the same name. The first implies the second, and the two papers refute only the first: OpenAI's theorem fixes the width, and Anthropic's bound, which holds for every \(k\), passes \(2^n\) once the width and the number of clauses both grow fast enough (its paper says that for \(k\) well above \((\log n)^{1/4}\) the bound in \(n\) is no better than trying all assignments). Williams's 2005 reduction from SAT to Orthogonal Vectors takes a CNF of any width, so the unbounded-width hypothesis implies the Orthogonal Vectors conjecture, and every lower bound proved from either of them stays conditional on a live hypothesis; both papers say that Orthogonal Vectors survives. So the fine-grained edifice built on CNF-SAT and Orthogonal Vectors, which is most of it, stands as before; what falls is what was proved from ETH, Gap-ETH or #ETH, or from SETH in its \(k\)-SAT form. The 3SUM and APSP hypotheses, which neither paper touches, are claimed refuted by a separate paper of 5 October 2026, by Josh Alman and Virginia Vassilevska Williams, whose five headline statements Anthropic formalized in Lean the next day; I have not assessed it.

Near this theory, two results lose their hypothesis. Marx's theorem that, under ETH, treewidth-based algorithms are optimal up to a logarithmic factor in the exponent for CSPs whose domain is part of the input stays a theorem, but its conclusion loses its support. Manurangsi and Raghavendra's hardness of approximating dense CSPs was proved under Gap-ETH. Both conclusions may still be true; they are now unsupported.

A circuit lower bound, proved by an algorithm

Theorem 6.1 of Williams's paper, in the numbering of his full version of May 2010, which both papers follow, reads: "If the Exponential Time Hypothesis is false, then \(\mathrm{E}^{NP}\) does not have linear size circuits." Here \(\mathrm{E}^{NP}\) is the class of languages decided in time \(2^{O(n)}\) with an NP oracle. Both papers draw the corollary, and OpenAI's Corollary 1.4 makes it quantitative: a language in \(\mathrm{E}^{NP}\) needing \(c\,n\sqrt{\log n}\) gates for infinitely many \(n\). That bound uses the fixed-density exponent \(n/\sqrt{\log n}\) of Appendix D, not the weaker one in OpenAI's Lean file. For scale, Anthropic's paper puts the best bound known before for a language in \(\mathrm{E}^{NP}\), over the full binary basis, at \(3.1n - o(n)\), by Li and Yang, and notes that the larger class \(\mathrm{S}_2\mathrm{E}\) already needs circuits of near-maximum size, by Chen, Hirahara and Ren, and by Li, both at STOC 2024. Whether an infinitely-often \(n\sqrt{\log n}\) bound for \(\mathrm{E}^{NP}\) itself is new against that 2024 work is a question for the circuit-complexity reader; I report the papers' framing and have not checked it. This is the one consequence that goes up rather than down: an algorithm for one problem becomes a lower bound for another, which is Williams's program.

Infinite templates, in a sentence

The theory's second front is infinite-domain CSPs, where what transfers depends on how an instance is written in Boolean variables, and neither paper says anything. My own arithmetic, checked against no source: for reducts of \((\mathbb{Q}, <)\) a variable per ordered pair gives only \(2^{o(n^2)}\), worse than enumerating the \(n!\) orderings, while encoding each variable's rank in \(\lceil \log_2 n \rceil\) bits with a comparator circuit per constraint gives \(2^{O(n\sqrt{\log n})}\) on instances with \(O(n)\) constraints; for reducts of the random graph the pair encoding gives \(2^{o(n^2)}\) against the \(2^{\Theta(n^2)}\) of enumerating graphs. Whether these are the right bounds for any infinite template I leave to someone who works on them.

The question for algebra

The two algorithms are algebraic, and it is worth being precise about which algebra. OpenAI's interpolates polynomials and bounds the rank of a matrix; Anthropic's expands the crossing \([x = v]\,[y = u]\), a permutation matrix of order \(N^2\) when \(x, y, u, v\) range over \(N\) values, as a signed sum of terms of low rank in one of two directions, and its Appendix H traces the search for that expansion to Hurwitz's problem on sums of squares and then to the Heisenberg algebra. This is algebraic complexity in Valiant's sense: rank, tensors, polynomials. The algebraic approach to constraint satisfaction means polymorphisms, the clones they generate, and the Galois connection between a clone and the relations its template can express. Neither paper looks at a polymorphism, and no theorem of either kind says anything about the other. The two fields share a word, not a theory, and a method moves from one to the other only across a bridge that is itself a theorem.

The claim: #k-SAT in time 2o(n), every fixed k so every finite-template CSP, #CSP and PCSP too, by encoding Up to polynomial time the dichotomy theorem the counting dichotomy PCSP hardness via minions P versus NP unchanged Exponential rates, between poly and 2n the order by strong partial clones: stands the strict separations under ETH: gone every NP-complete SAT(S) has T(S) = 0 Marx's conclusion, Gap-ETH hardness: unsupported the question moves to subexponential rates Restricted models bounded width (Datalog) Sherali–Adams; affine hierarchy resolution, other proof systems unconditional lower bounds unchanged
Where the algebraic theory's statements sit relative to the claim. The claim is a statement about exponential rates, so it reaches only the middle column. The left column is stated up to polynomial time and the right column holds against restricted algorithms and proof systems unconditionally; ETH enters neither. The one question the claim opens is in the middle: do distinct frozen partial clones force different subexponential rates?

So the question the claims leave for algebra is the one the fine-grained theory already posed, one scale down. Jonsson and his coauthors showed that the complexity of \(\mathrm{SAT}(S)\) is determined by its frozen partial clone, and the two papers hand every NP-complete finite Boolean \(S\) the same upper bound. Do distinct frozen partial clones force different subexponential rates, or does everything NP-complete collapse to one rate? The smallest templates that could test it are the ones Jonsson and his coauthors already singled out at the bottom of their lattice. And a question one step out, which I am not aware of anyone having asked: what plays the part of the frozen partial clone for templates on more than two elements, where the encoding above costs a factor \(\lceil \log_2 d \rceil\) in the exponent that a direct algorithm might not pay?

One more claim from the same season belongs in the record without a verdict. The paragraph introducing OpenAI's Corollary 1.2 cites OpenAI's preprint The Unique Games Theorem of 23 September 2026, a separate claim; the stated objective of Barto's CoCoSym project names the Unique Games Conjecture, and P versus NP, among the problems the algebraic theory may reach. I have assessed neither the preprint nor its bearing on promise CSPs.

What would settle it

  • The working group's report. Impagliazzo, Paturi and Williams have said they will examine and explain OpenAI's proof. Anthropic's paper names no reviewer, and a report on one proof does not cover the other, though the two share their sparsification steps and their tensor-contraction endgame.
  • A second reading of the two statement files. Each is a page of definitions. The reading above is one such; another, by someone who did not help write this post, costs an afternoon and is the cheapest check anyone can add. With it, and an independent build, the formal claims are as settled as a formal claim gets; what the working group settles is the exposition, and with it our understanding.
  • An independent build. Anthropic's README gives three commands and says the build took about eight minutes on 24 virtual CPUs, with the largest process near 7 GB, and prints the axioms both theorems depend on. OpenAI's Comparator challenge and its full proof are in the openai/math repository. A build on a machine the labs do not control confirms that the proofs check against the statements; it does not read the statements.
  • Nothing experimental. Anthropic's paper says that for formulas with \(5n\) clauses its bound beats exhaustive search only past \(n = 10^{10\,000}\), and that its bound in \(n\) alone does so only past \(n = 10^{10^8}\). No run of either algorithm on a formula anyone can write down will tell us anything.

I will add a short update to this post when the working group reports.

Sources