The Exponential Time Hypothesis Fell Twice. The Way Through Was a Minus Sign
On 26 October two papers appeared within hours of each other. One, from OpenAI, is titled The Exponential Time Hypothesis is False. The other, from Anthropic, is credited to "Claude" and titled A 2^o(n) Time Algorithm for 3-SAT. Both say the same thing: the reference hard problem of computer science, which I explain below with a dinner party, can be solved faster than anyone believed possible, and a conjecture that hundreds of results were built on is false. Both come with a proof checked line by line by Lean, a program that verifies mathematics mechanically. Both were found by an AI model the labs have not released. Anthropic's paper dates its discovery to 16 October, "with 14M output tokens and no human input"; OpenAI's manuscript is dated 17 October.
The headlines went for the AI-cracks-a-decades-old-puzzle angle and stopped there. That leaves out the part I find most interesting, which is how. I read both papers, and the answer is not two unrelated tricks. Both algorithms run into the same wall that every SAT algorithm since the 1980s has run into, and both get through it the same way: by solving a harder problem than the one asked, and letting negative numbers cancel. One of them does it with an identity a Danish mathematician wrote down in 1818.
None of this makes any real software faster, and none of it settles P vs NP, the famous million-dollar question. I'll get to why. First, the problem, in plain words, because without it nothing else in this story makes sense.
The problem: a dinner party with conditions
Say you are organising a dinner and your friends have sent conditions. "I'll come if Ana comes or Bea doesn't." "At least one of Carlos and Diego." "Not Ana, Bea and Carlos all together, please." Each friend is a yes/no decision, and each condition mentions at most three friends. The question: is there any guest list that meets every condition at once?
That is 3-SAT. "SAT" stands for satisfiability: can all the conditions be satisfied together? The "3" is because each condition, called a clause, involves at most three yes/no variables. Written the way computer scientists write it, a clause looks like {% katex inline %}(x_1 \lor \lnot x_2 \lor x_5){% endkatex %}: "friend 1 comes, or friend 2 doesn't, or friend 5 comes".
It looks like a parlour puzzle, and it is the puzzle. In 1971 Stephen Cook showed that a huge family of problems (timetables, delivery routes, verifying that a chip has no bugs, Sudoku, and thousands more) can be translated into it. Solve 3-SAT fast and you solve all of them fast. That is why it is the reference hard problem of computer science.
What makes it hard is an asymmetry. If someone hands you a guest list, checking it is trivial: go through the conditions one by one. Finding one is another matter. With {% katex inline %}n{% endkatex %} friends there are {% katex inline %}2^n{% endkatex %} possible lists: with 30 friends, about a billion; with 100, so many that a million computers each checking a billion lists per second would need some 40 million years to go through them. The question since the 1970s has been how much better than "try them all" you can do.
!The asymmetry behind 3-SAT. On the left, checking one proposed guest list against three conditions takes one pass and three ticks. On the right, finding a valid list by trying them all means 2 to the n lists: 1,024 for 10 friends, about a billion for 30, and a 31-digit number for 100.
The asymmetry behind 3-SAT. Checking a proposed answer is quick; finding one by trying them all doubles in cost with every friend you add.
What the hypothesis said
The best algorithms don't try everything; they prune, guess cleverly, and backtrack. But their running time still grows exponentially: each extra variable multiplies the work by a fixed factor, the base. For trying everything the base is 2 (one more friend, twice the lists). Schöning's random walk brought it to {% katex inline %}1.334{% endkatex %} in 1999, PPSZ with Hertli's analysis to {% katex inline %}1.308{% endkatex %}, Liu's deterministic algorithm to {% katex inline %}1.328{% endkatex %}. That sounds like a small gain and it is an enormous one: {% katex inline %}2^{100}{% endkatex %} is a 31-digit number, {% katex inline %}1.308^{100}{% endkatex %} a 12-digit one. But forty years of very clever work never brought the base close to 1.
In 1999 Russell Impagliazzo and Ramamohan Paturi turned that experience into a conjecture, the Exponential Time Hypothesis (ETH): the base can be lowered but never to 1. Put precisely: there is some number {% katex inline %}c{% endkatex %} greater than 1 such that no algorithm solves every 3-SAT instance faster than {% katex inline %}c^n{% endkatex %}. However clever the algorithm, each extra variable will always cost at least that fixed multiplier. Its stronger sibling, SETH, says that when conditions can mention many variables, you cannot even lower the base much.
Papers usually write the same thing with the base fixed at 2 and the change moved into the exponent. Any base {% katex inline %}c{% endkatex %} is a power of 2, {% katex inline %}c = 2^{\delta}{% endkatex %}, so {% katex inline %}c^n = 2^{\delta n}{% endkatex %}: trying everything is {% katex inline %}\delta = 1{% endkatex %}, and {% katex inline %}1.308^n{% endkatex %} is about {% katex inline %}2^{0.39n}{% endkatex %}. Lowering the base towards 1 and lowering {% katex inline %}\delta{% endkatex %} towards 0 are the same thing. In that language ETH says {% katex inline %}\delta{% endkatex %} can never go below some fixed positive number.
An algorithm that breaks this is called subexponential, written {% katex inline %}2^{o(n)}{% endkatex %}: its exponent grows more slowly than {% katex inline %}\delta n{% endkatex %} for every {% katex inline %}\delta > 0{% endkatex %}. In the language of bases, the multiplier you pay per extra variable keeps shrinking towards 1 as the problem grows. It is still not fast in any everyday sense, but it is a different kind of growth, and ETH said it was impossible.
!Bar chart of the best known running time for 3-SAT written as base to the n: brute force 2, Schöning 1999 1.334, Liu 2018 deterministic 1.328, PPSZ with Hertli 2014 randomized 1.308. The 2026 algorithms have an effective base that tends to 1 as n grows, which is what refutes the Exponential Time Hypothesis.
Forty years of progress on 3-SAT lowered the base of the exponent. ETH bet that it could never reach 1. The new algorithms take time 2^o(n): their effective base slides to 1 as n grows. (The axis is compressed between 1.5 and 2.)
That bet was not idle. Anthropic's paper reports a literature search, carried out by Claude, that found more than 800 papers proving at least one result only under ETH or something that implies it. ETH is the reason we "know" that k-Clique has no {% katex inline %}n^{o(k)}{% endkatex %} algorithm, that many parameterized algorithms are optimal, that dynamic programming over tree decompositions cannot be improved. In 2019 Ryan Williams gave two separate estimates: a 70% chance that ETH was true, and a 25% chance that SETH was true. They are not slices of one pie and are not meant to add up to 100%: SETH is the stronger claim (if it holds, ETH holds too), so it can only be the less likely of the two. Most of the field would have put both numbers higher.
Both papers now give a deterministic algorithm that runs in {% katex inline %}2^{o(n)}{% endkatex %}: for every {% katex inline %}\delta > 0{% endkatex %} it is eventually faster than {% katex inline %}2^{\delta n}{% endkatex %}, which is to say it eventually beats every base above 1. That refutes ETH, SETH, Gap-ETH and the counting version #ETH in one go.
The wall
Here is the intuition for why the base never reached 1, and it is the same picture in both papers.
Go back to the dinner. Draw each condition as a dot, and join two dots with a line when they mention the same friend. Anthropic's paper says each line "carries bits", one per shared yes/no decision. The natural shortcut is divide and conquer: split the drawing in two halves, try every possible answer for just the friends whose lines cross the split, and for each of those, solve each half on its own. If your friends form two groups that barely know each other, only a few decisions cross the split, and this is enormously faster than trying every list.
The problem is that you don't get to choose the friends. Random sets of conditions, and the hard instances generally, look like expander graphs, where every way of splitting the nodes into two halves of comparable size is crossed by a constant fraction of all the edges. In the paper's words, "any algorithm that fixes one tree of cuts in advance and enumerates the crossing bits of each cut takes time {% katex inline %}2^{\Omega(n)}{% endkatex %}. Thus earlier divide and conquer ideas only improved the constant in the exponent."
!Two graphs side by side. On the left, a formula whose clause graph has two loosely connected clusters: a cut between them is crossed by only two edges, so divide and conquer is cheap. On the right, an expander-like graph where every balanced cut is crossed by many edges, so enumerating the crossing bits costs exponential time whatever cut is chosen.
Divide and conquer pays for the bits that cross the cut. On hard formulas every balanced cut is crossed by a constant fraction of the bits, so any fixed plan of cuts costs 2^Ω(n). This is the wall.
To go through the wall you have to stop paying for every crossing bit. And there is no way to do that if every quantity you handle means "number of solutions of something", because counts of solutions are non-negative and cannot cancel.
Count, don't decide
So both papers do something that sounds backwards. They don't ask "is there a valid guest list?". They ask "how many valid guest lists are there?" and compute the exact number, which is the #3-SAT problem and is in principle much harder (the previous best for counting was around {% katex inline %}1.64^n{% endkatex %}, worse than for deciding). Testing whether the count is zero then decides satisfiability for free.
Why make your life harder? Because a count is a sum, and a sum is algebra. The number of satisfying assignments is
{% katex %}
\#F = \sum_{x \in \{0,1\}^n} \prod_{\text{clauses } e} \Phi_e(x)
{% endkatex %}
where each {% katex inline %}\Phi_e{% endkatex %} is 1 if clause {% katex inline %}e{% endkatex %} is satisfied and 0 otherwise. A sum of products can be rearranged, rewritten, expanded and regrouped, and nothing forces the intermediate terms to be 0 or 1 or even positive. Once negative numbers are allowed in the middle of the computation, two expensive pieces can cancel into a cheap one. Branching algorithms, which ask "what if {% katex inline %}x_1{% endkatex %} is true?", can't do this: every branch is a real sub-question with a real non-negative answer.
Where do negative numbers come from, if every list either works or doesn't? From subtraction, the same as at school. Take the condition "Ana comes, or Bea doesn't". Counting the lists that meet it directly is awkward, because an or ties the two friends together. Count instead all lists, minus the lists that break it. A list breaks it only when Ana stays home and Bea comes, and an and splits cleanly, one friend at a time. With just Ana and Bea there are 4 lists, exactly one of them breaks the condition, so the count is 4 − 1 = 3. In the formula above that is {% katex inline %}\Phi = 1 - (1 - x_{\text{Ana}})\,x_{\text{Bea}}{% endkatex %}.
Do that for every condition and multiply out, and the count becomes a long sum of simpler terms with plus and minus signs. No single term is the number of valid lists of anything; some are negative; only the total is the count. What you gain is that each term is easy to split into independent pieces. Done naively there are far too many terms, so the work of both papers is in choosing which signed pieces to write, so that the ones linking far-apart parts of the problem cancel.
That is the common move. The two papers then implement it in completely different ways.
If you only want the idea, you have it: the wall is that hard problems can't be split cleanly, and the way through is to count with numbers that can be negative, so the expensive parts cancel. The next two sections show how each lab did it, with a bit more mathematics; you can skip to [What changes, and what doesn't](#what-changes-and-what-doesnt) without losing the thread.
Claude's route: an identity from 1818
Anthropic's algorithm stays with the graph picture and attacks the bits that cross.
Take the clause graph and merge clauses into a modest number {% katex inline %}K{% endkatex %} of big nodes, so that every pair of big nodes is joined by an edge carrying the same number {% katex inline %}\lambda{% endkatex %} of bits. The quantity to beat is the total number of crossing bits, {% katex inline %}S{% endkatex %}. Now place the nodes on a {% katex inline %}g \times g{% endkatex %} grid. Most edges are diagonals: they join two nodes in different rows and different columns. Every diagonal belongs to exactly one rectangle, and each rectangle has two diagonals: the top-left corner holds a string {% katex inline %}x{% endkatex %} that must equal the bottom-right's {% katex inline %}v{% endkatex %}, and the top-right holds {% katex inline %}y{% endkatex %}, which must equal the bottom-left's {% katex inline %}u{% endkatex %}. That pair of equality checks, {% katex inline %}[x = v]\,[y = u]{% endkatex %}, the paper calls a crossing.
If you merge each row into one node, a crossing costs 6 bits per block of 3: the top row has to tell the bottom row both {% katex inline %}x{% endkatex %} and {% katex inline %}y{% endkatex %}. Here comes the identity. For blocks of 3 bits there is a sign function {% katex inline %}\sigma{% endkatex %} such that
{% katex %}
2\,[x = v]\,[y = u] = [x \oplus y \oplus u \oplus v = 0]\,\big(\sigma(x,y)\,\sigma(v,u) + \sigma(x,u)\,\sigma(v,y)\big)
{% endkatex %}
and it can be checked by brute force on all 4,096 settings of the 12 bits. Read the right-hand side as two terms. In the first, the row choice, each {% katex inline %}\sigma{% endkatex %} depends only on one row, and the two rows only need to agree on the single 3-bit string {% katex inline %}x \oplus y = u \oplus v{% endkatex %}. That costs 3 bits, half of the 6. The second term, the column choice, is still expensive if you merged rows, but it costs only 3 bits if you merge columns instead. Neither term means anything combinatorially, they take negative values, and only their sum is a count. But each term is cheap in one direction.
!A rectangle of the grid with corners holding strings x, y on top and u, v below. Its two diagonals test x equals v and y equals u, which costs six bits per block when rows are merged. The eight-square identity rewrites twice this crossing as a four-corner parity check times the sum of a row choice, whose sign functions each live in one row and cost three bits, and a column choice, which costs six bits with rows merged but three with columns merged.
The eight-square identity for one rectangle. Two diagonal checks become a four-corner parity check times a signed sum of two terms. Each term is cheap along one direction of the grid, so whichever direction you merge, a share of the bits disappears.
The rest is bookkeeping, done carefully. Strings are split into blocks of 3, and the expansion is grouped by how many blocks took the column choice, which keeps the number of terms polynomial. For each term the algorithm merges rows or columns, whichever is cheaper. Per block, the two directions together cost {% katex inline %}3 + 6 + 1 + 1 = 11{% endkatex %} bits against the {% katex inline %}12{% endkatex %} of two crossings, so the cheaper direction pays at most {% katex inline %}11/12{% endkatex %} of what was there before. Then it groups the merged rows into {% katex inline %}K{% endkatex %} balanced super-nodes and recurses.
The paper writes the running time as {% katex inline %}2^{e S}{% endkatex %}, where {% katex inline %}S{% endkatex %} is the number of bits on the edges, proportional to the size of the formula. So {% katex inline %}e{% endkatex %} plays the role of {% katex inline %}\delta{% endkatex %} above, and {% katex inline %}2^e{% endkatex %} is the base, paid per bit instead of per variable. One level shrinks {% katex inline %}e{% endkatex %} by a factor of {% katex inline %}11/12{% endkatex %}. Repeat it and {% katex inline %}e{% endkatex %} goes to zero, which is the base going to 1: the paper's bound is {% katex inline %}e_\ell \le 1.12\,(11/12)^\ell{% endkatex %}. The price is that each level needs vastly more nodes, {% katex inline %}K_\ell = 9K_{\ell-1}^{16}{% endkatex %} starting from 64, which is why all of this only matters for astronomically large formulas.
!Chart of the running-time exponent at each level of the recursion in Anthropic's algorithm. Level 0 is brute force with exponent 1. Level 1 is slightly worse, about 1.03, because the first grid is small. From level 2 on, the exponent falls by a factor of eleven twelfths per level, bounded by 1.12 times eleven twelfths to the level, reaching under 0.47 by level 10 and tending to zero.
Each level of the recursion multiplies the exponent (the δ of 2^δn, so the base is 2^δ) by about 11/12. It never reaches zero at any fixed level, but it gets below any δ you name, which is exactly what refuting ETH requires.
The identity is the beautiful part. Its classical form says that the product of two sums of eight squares is again a sum of eight squares. Ferdinand Degen presented it to the St Petersburg Academy in 1818, and John Graves found it again in 1843 while showing that the norm of the octonions, the eight-dimensional cousin of the complex numbers, is multiplicative. The sign function {% katex inline %}\sigma{% endkatex %} in the algorithm is, in the paper's words, "the table of signs of the multiplication of the octonions, with the basis elements renamed". Hurwitz proved in 1898 that such identities exist only for 1, 2, 4 and 8 squares. The paper has an appendix explaining why the search for a cheaper decomposition of a crossing leads straight to Hurwitz's problem, and why, under the simple bit count it uses, only eight leaves a gain: two squares break even, four break even, eight give 11 out of 12.
So the thing that broke ETH is the multiplication table of the octonions, used to cut bits on a grid.
OpenAI's route: deform the problem, then interpolate back
OpenAI's algorithm uses the same "count, and let terms cancel" idea through a different door: interpolation.
Start from the same formula for {% katex inline %}\#F{% endkatex %}. Now introduce a parameter {% katex inline %}T{% endkatex %} and replace each variable occurrence inside each clause by a linear combination of variables whose coefficients are polynomials in {% katex inline %}T{% endkatex %}. At {% katex inline %}T = 0{% endkatex %} every replacement is the original variable, so the deformed sum {% katex inline %}H(T){% endkatex %} satisfies {% katex inline %}H(0) = \#F{% endkatex %}. At the points {% katex inline %}T = 1, \dots, Q{% endkatex %}, the replacements are designed so that the variables split into small groups that interact only through a few shared "measurements", small integer linear combinations of each group's bits. Fix the values of those measurements and the sum factorizes group by group, exactly the way the clustered formula of the earlier figure would. At those points the expensive problem becomes cheap.
!Sketch of OpenAI's interpolation strategy. A polynomial H of T is drawn as a curve. At T equals zero, its value is the exact number of satisfying assignments, which is hard to compute directly. At the points T equals one to Q, the problem splits into groups and is cheap, so the algorithm computes the value and a few Taylor coefficients there, drawn as short tangent marks. Because the degree of H is known, these determine H, and therefore H of zero.
OpenAI's strategy: deform the counting problem into a polynomial H(T) of known degree. At T = 0 it is the count; at T = 1…Q it splits into independent groups. A few Taylor coefficients at each easy point pin down the polynomial, and with it the count.
Because {% katex inline %}H{% endkatex %} is a polynomial of known degree, its values and a few derivatives at the easy points determine it completely, and you read off {% katex inline %}H(0){% endkatex %}. Interpolation here is not an approximation: it is exact rational arithmetic. The whole difficulty is in a tension between two costs. The replacements must have low degree in {% katex inline %}T{% endkatex %}, or you need too many Taylor coefficients per point. And they must respect a different grouping at each of the {% katex inline %}Q{% endkatex %} points, which naively costs degree {% katex inline %}Q{% endkatex %}.
The construction that resolves it is where the minus sign comes back. It is built out of swaps: permutation matrices {% katex inline %}\Pi_s{% endkatex %} that exchange two group labels at position {% katex inline %}s{% endkatex %}, each with eigenvalues {% katex inline %}+1{% endkatex %} and {% katex inline %}-1{% endkatex %}. A basis vector with {% katex inline %}j{% endkatex %} of its positions in the {% katex inline %}-1{% endkatex %} eigenspace gets multiplied by {% katex inline %}(-1)^j{% endkatex %} under the full swap. OpenAI chooses a polynomial {% katex inline %}f{% endkatex %} that interpolates {% katex inline %}(-1)^j{% endkatex %} only on a short window of {% katex inline %}j{% endkatex %} values, centred where a binomial distribution puts almost all of its mass. Inside the window the construction is exact; the few directions outside it are paid for with explicit measurements. The window only needs to be about as wide as the binomial's standard deviation, {% katex inline %}\sqrt{Q}{% endkatex %}, and with {% katex inline %}Q \approx \log n{% endkatex %} that is where the {% katex inline %}\sqrt{\log n}{% endkatex %} in the final bound comes from.
Multiply out the three costs (Taylor data, measurements, one group at a time) and each one is {% katex inline %}2^{o(n)}{% endkatex %}. The algorithm also runs in polynomial space, which Anthropic's does not claim.
Same wall, same minus sign
Side by side:
| | OpenAI | Anthropic (Claude) |
|---|---|---|
| Date on the paper | 17 October, revised 25 October | 26 October; core found 16 October |
| Length | 67 pages | 49 pages |
| What it computes | exact #k-SAT, deterministic | exact #k-SAT, deterministic |
| Bound, sparse formulas | {% katex inline %}2^{O(n/\sqrt{\log n})}{% endkatex %} | {% katex inline %}2^{O(m/\sqrt{\log m})}{% endkatex %} in the clause count |
| Bound, any formula | {% katex inline %}2^{O(n \log\log n/\sqrt{\log n})}{% endkatex %} | {% katex inline %}2^{O(k^2 n \log\log n/\sqrt{\log n})}{% endkatex %} |
| Bound proved in Lean | weaker: {% katex inline %}(\log\log n)^2{% endkatex %} in place of {% katex inline %}\log\log n{% endkatex %} | the main theorem as stated |
| Key device | deformation + Hermite interpolation; swap matrices, {% katex inline %}f(j) = (-1)^j{% endkatex %} | grid + eight-square identity; recursion with factor 11/12 |
| Space | polynomial | not claimed |
The bounds land in the same place, which is either a coincidence or a hint about where the natural barrier for this family of techniques sits. Neither paper knows how to remove the {% katex inline %}\log\log n{% endkatex %} for general formulas.
And the mechanisms rhyme more than they look. OpenAI's construction is literally built from swap operators with eigenvalues {% katex inline %}\pm 1{% endkatex %}. Anthropic's README compresses its own key idea into a paragraph that includes "Per bit, SWAP = I − 2·singlet", the physicist's way of writing a swap as the identity minus a signed correction. Both papers solve a harder problem so they can work with signed quantities, and both get their saving from writing an exchange of two things as a combination of cheaper things with signs. The non-negative world, where every intermediate number counts solutions of something, is exactly where ETH was true.
What changes, and what doesn't
Nothing changes in practice. Anthropic's paper is unusually blunt about it. For a 3-CNF with {% katex inline %}m = 5n{% endkatex %} clauses its bound beats the {% katex inline %}2^n{% endkatex %} of brute force only once {% katex inline %}n > 10^{10\,000}{% endkatex %}, and the bound in {% katex inline %}n{% endkatex %} alone only once {% katex inline %}n > 10^{10^8}{% endkatex %}. The authors add that their general approach "seems unlikely to yield any general improvement unless {% katex inline %}n > 10^7{% endkatex %}, however it is instantiated", while brute force is already impossible at {% katex inline %}n = 100{% endkatex %}. Your SAT solver, your scheduler, your verification tool are exactly as fast as last week.
P vs NP is untouched. P vs NP asks whether problems like 3-SAT can be solved in polynomial time, with work growing like {% katex inline %}n^2{% endkatex %} or {% katex inline %}n^3{% endkatex %}, which is far faster than anything in these papers. ETH was a stronger bet than P ≠ NP, so losing it says nothing about the weaker one. And a {% katex inline %}2^{o(n)}{% endkatex %} bound for 3-SAT does not transfer to every NP problem, because polynomial-time reductions can blow up the number of variables polynomially, and {% katex inline %}2^{o(n)}{% endkatex %} composed with a polynomial is no longer subexponential. For problems with reductions that keep the size linear, it does transfer: OpenAI derives subexponential counting of independent sets, proper colourings and perfect matchings; Anthropic lists Independent Set, Clique, Vertex Cover and Dominating Set in {% katex inline %}O(2^{\delta n}){% endkatex %} for every {% katex inline %}\delta > 0{% endkatex %}.
A shelf of theorems changed status. Everything proved "under ETH" or "under SETH" has lost its hypothesis. Some of it survives on weaker foundations: the quadratic lower bounds for edit distance and longest common subsequence also follow from the Orthogonal Vectors conjecture, which neither paper refutes. Much of it, the 800-odd papers' worth, now needs a new reason to be true or turns out to be false.
And there is one genuinely unconditional gain. Through Ryan Williams's programme, which turns slightly-faster-than-brute-force SAT algorithms into circuit lower bounds, both papers get that the class {% katex inline %}E^{NP}{% endkatex %} has no Boolean circuits of linear size. OpenAI's version gives a lower bound of order {% katex inline %}n\sqrt{\log n}{% endkatex %}. The best known before, over the full binary basis, was {% katex inline %}3.1n{% endkatex %}. Circuit lower bounds are one of the most stuck areas of complexity theory, and this one came out as a side effect.
What Lean checks, and what it doesn't
Both results are formalized, and both teams are careful about what that means. Anthropic's README says it in one line I wish every formalization carried: "Lean checks the proofs, but no machine checks that this file says what the paper says; the file is kept short so that a reader can check this." OpenAI's Lean scope note is similarly precise: the machine-checked bound is the weaker one with {% katex inline %}(\log\log n)^2{% endkatex %}; the sharper bound in the paper is not.
That is the gap I wrote about in Proved, Certified, Swept, Sampled: a green check is a statement about a specific claim, and the work is knowing which claim. Here it is handled well. The statements are short, they are printed in the papers, and the differences from the prose are listed. As I write this, human review is still under way: according to the coverage, OpenAI handed its result to outside reviewers that include Impagliazzo and Paturi themselves. A Lean proof of a correctly stated theorem leaves them very little to find, but "correctly stated" is the part they are there for.
The proof that fits in a prompt
One more detail, and for someone who builds with these models it is the one that stays with me. At the end of Anthropic's README there is a section titled "The key idea, in condensed form interpretable by AI models". It is a single paragraph. It starts "The exponential time hypothesis is false!", states a recursion for the cost of contracting tensor networks on a complete graph, mentions the grid, the swap, the grouping by number of singlets, and ends "Prove it." The README says that Claude Opus 5.5 at high effort can rederive the refutation, in its weaker {% katex inline %}O(2^{\delta n}){% endkatex %} form, from that paragraph alone.
That is a new kind of mathematical object. For centuries a proof has been written for a human reader, at whatever level of detail that reader needs. Here there are three layers: a 49-page paper for people, a Lean development for the kernel, and a one-paragraph hint for a model, which is enough because the model can fill in the rest. When I wrote about the Navier–Stokes blow-up, the bottleneck was the opposite one: the machine's drafts were close to unreadable, and turning them into a paper a person could follow was weeks of work. Seven weeks later, the most compressed description of a major result is the one written for a machine.
What to take from it
- ETH is false, twice, independently, with formal proofs, pending the human review that is now under way. SETH, Gap-ETH and #ETH go with it.
- The wall was the expander, and the way through was a minus sign. Both algorithms count instead of decide, so that terms can be negative and cancel. That is the one-sentence intuition, and it is the same for both.
- Claude's version runs on the octonions. A 1818 identity for sums of eight squares turns two crossing equality checks into terms that are each cheap in one direction, and a recursion multiplies the exponent by 11/12 per level until it is as small as you like.
- OpenAI's version deforms and interpolates. A polynomial that equals the count at 0 and splits into independent groups at {% katex inline %}1, \dots, Q{% endkatex %}, held together by swap matrices and a polynomial that imitates {% katex inline %}(-1)^j{% endkatex %} on a window under a bell curve.
- No practical consequence. The crossover is beyond {% katex inline %}10^{10\,000}{% endkatex %} variables. The consequences are for theory: hundreds of conditional lower bounds lose their hypothesis, and a circuit lower bound moved for free.
- Two labs, the same week, the same bound. Whatever this says about the problem, it says something about the models: the frontier of what they can find now includes a result that one of the field's leading experts, in 2019, put at 70-to-30 against.
---
Sources: Anthropic's paper and Lean formalization (A 2^o(n) Time Algorithm for 3-SAT, by Claude), OpenAI's Lean scope note and paper (The Exponential Time Hypothesis is False).
On the eight-square identity and the octonions: John C. Baez, "The Octonions", Bulletin of the AMS 39 (2002), 145–205; J. H. Conway and D. A. Smith, "On Quaternions and Octonions", A K Peters, 2003; A. Hurwitz, "Über die Composition der quadratischen Formen von beliebig vielen Variabeln", Nachr. Ges. Wiss. Göttingen (1898), 309–316; and Degen's eight-square identity on Wikipedia.
---
Originally published on javieraguilar.ai
Want to see more AI agent projects? Check out my portfolio where I showcase multi-agent systems, MCP development, and compliance automation.
Две лаборатории против одной гипотезы: что происходит вокруг ETH
OpenAI и Anthropic сообщили, что их исследовательские модели нашли алгоритмы, опровергающие гипотезу экспоненциального времени — ETH. На этом предположении построены многочисленные оценки сложности вычислительных задач. Если результат выдержит проверку, исследователям придётся пересмотреть часть представлений о том, какие алгоритмы вообще возможны.
Масштаб последствий зависит от того, какое ускорение обещают новые алгоритмы. Для этого нужно разобраться в связи ETH с проблемой P против NP.
Что опубликовали лаборатории
26 октября 2026 года OpenAIобъявила о результатах в трёх областях: математическом анализе, теории вычислительной сложности и квантовой теории поля. Заявление об ETH относится ко второй. Компания выложила текст доказательства и его формализацию в Lean — системе проверки математических доказательств.
Вскоре собственные материалыпредставила Anthropic. Компания приписывает результат внутренней исследовательской модели Claude. Заявленный алгоритм решает задачу 3-SAT за субэкспоненциальное время. Он также должен подсчитывать число удовлетворяющих формуле наборов значений.
За внешнее изучение результата OpenAI взялись Райан Уильямс из MIT, Рассел Импальяццо и Рамамохан Патури из Калифорнийского университета в Сан-Диего. Воткрытом письме исследователи подчеркнули: их участие не означает, что заявленное опровержение уже получило научное подтверждение.
Какую границу устанавливает ETH
ETH касается задачи выполнимости булевых формул. В варианте 3-SAT формула состоит из условий, соединённых оператором «И». Каждое условие содержит до трёх переменных или их отрицаний, связанных через «ИЛИ». Нужно подобрать значения «истина» и «ложь», при которых вся формула окажется истинной.
Простой пример:
(x ИЛИ y ИЛИ НЕ z) И (НЕ x ИЛИ z ИЛИ w).
Если x, z и w истинны, а y ложно, оба условия выполнены. Проверить предложенный набор значений нетрудно: достаточно пройти по условиям. При поиске подходящего набора готовой подсказки уже нет.
У n булевых переменных есть 2ⁿ возможных наборов значений. Полный перебор проверяет их один за другим; добавление одной переменной удваивает число комбинаций. ETH утверждает более тонкую вещь: даже при другом подходе в худшем случае нельзя полностью избавиться от экспоненциальной зависимости.
Пример представления булевой формулы графом и объединения групп узлов. Фрагмент иллюстрации из работы Anthropic
СогласноETH, для 3-SAT нет алгоритма со временем 2^(o(n)), с точностью до полиномиальных множителей по размеру входа.
Обозначение o(n) означает, что показатель растёт медленнее n: отношение этих величин стремится к нулю. Поэтому 2^(√n) — пример субэкспоненциальной зависимости, а 2^(0,01n) — всё ещё экспоненциальная. Маленький постоянный коэффициент сам по себе гипотезу не опровергает.
Быстро решить много удачно подобранных формул недостаточно: нужна доказанная оценка для худшего случая. Именно такую гарантию заявляют лаборатории.
Почему вопрос P против NP остаётся открытым
Проблема P против NP проводит другую границу. Класс P включает задачи с ответом «да» или «нет», которые можно решить за полиномиальное время. В классе NP для положительного ответа существует свидетельство, которое можно проверить за полиномиальное время.
Для 3-SAT таким свидетельством служит подходящий набор значений переменных. Если его предоставить, проверить формулу можно быстро. Вопрос в том, существует ли столь же эффективный общий способ определить, есть ли решение. «Быстро» здесь означает полиномиальную зависимость от длины входных данных, например квадрат или куб этой длины.
Разницу между оценками удобно увидеть на трёх выражениях:
Зависимость
Тип роста
Что происходит при увеличении n
n³
Полиномиальный
Размер входа возводится в фиксированную степень
2^(√n)
Субэкспоненциальный, но сверхполиномиальный
Растёт быстрее любой фиксированной степени n
2ⁿ
Экспоненциальный
Каждая дополнительная единица n удваивает значение
Таблица иллюстрирует типы роста функций. Она не описывает измеренную скорость новых алгоритмов.
Полиномиальная, субэкспоненциальная и экспоненциальная зависимости растут с разной скоростью. По вертикали показан двоичный логарифм значения функции; обе оси имеют логарифмический масштаб
3-SAT — NP-полная задача: полиномиальный алгоритм для неё дал бы полиномиальные алгоритмы для всех задач NP.
ETH — более сильное предположение, чем P ≠ NP. Её истинность влечёт P ≠ NP, но опровержение ETH само по себе не устанавливает P = NP. У 3-SAT может существовать субэкспоненциальный алгоритм, который всё равно работает дольше любого полинома.
Что подтверждает проверка в Lean
Lean проверяет, что утверждение следует из заданных определений и аксиом. Человеку остаётся убедиться, что формализованная теорема соответствует исходной задаче. Безошибочное доказательство более слабого утверждения не подтверждает более сильное.
Вописании формализации OpenAI уже видна существенная деталь. Рукопись заявляет время:
2^(O(n · log log n / √log n)).
В документе о границах проверки Lean указана более слабая оценка:
2^(O(n · (log log n)² / √log n)).
Оценки приведены для фиксированного k — максимальной длины условия; полиномиальные множители по размеру входа опущены. Дополнительный множитель log log n ухудшает верхнюю оценку времени. При этом обе зависимости остаются субэкспоненциальными и, если доказаны для нужной задачи, достаточны для опровержения ETH.GitHub
Anthropic отдельно отмечает этот предел вREADME проекта: машина проверяет доказательства, но соответствие формальных утверждений тексту статьи требует человеческого прочтения. Для этого компания вынесла основные формулировки в отдельный короткий файл MainResults.lean.raw.githubusercontent.com
Что изменится для алгоритмов и криптографии
ETH использовали как исходное предположение для условных нижних оценок. Логика таких работ выглядит примерно так: «Если ETH верна, задача X не может решаться быстрее определённой границы».
Опровержение предположения не делает условную теорему ошибочной, но лишает её основания для вывода о реальном пределе скорости. Сведения задач друг к другу, методы и промежуточные результаты сохраняют ценность.
Здесь есть ещё одна тонкость. Из нового алгоритма для 3-SAT нельзя автоматически получить одинаковое ускорение для любой NP-полной задачи. При сведении одной задачи к другой размер входа может вырасти. Поэтому последствия нужно рассчитывать для каждого конкретного сведения, учитывая, по какому параметру измеряется сложность.
Для разработчиков ПО важен следующий вопрос: при каких размерах данных новый алгоритм начинает выигрывать? Асимптотика описывает рост затрат при увеличении входа. Она скрывает постоянные коэффициенты и не сообщает, будет ли реализация полезна на доступном оборудовании. Anthropic прямо характеризует свой результат как асимптотический, без утверждений о практической скорости решения формул.
По той же причине заявление об ETH не даёт оснований объявлять существующее шифрование взломанным. Для такого вывода нужен конкретный способ атаки, оценка его затрат и применимость к используемым параметрам криптосистемы. Общего утверждения об ускорении 3-SAT для этого недостаточно.
Уильямс рассказал, что спросил OpenAI о возможных последствиях для криптографии. По его словам, компания проверила этот вопрос и не обнаружила оснований считать, что результат приводит к взлому криптосистем. Этопересказ ответа лаборатории в TechCrunch, а не независимый аудит безопасности.
Как учёные собираются проверять результат
Ранее Уильямс сравнил массовую публикацию ИИ-доказательств с DDoS-атакой на математиков: их проверка требует времени специалистов, которого новые тексты не прибавляют.
Теперь OpenAI согласилась открыть материалы по ETH и профинансировать конференцию для обсуждения последствий. Участники внешней группы работают без вознаграждения от компании и без обязательств о неразглашении. Они могут публиковать собственные выводы, включая критику.openai.com
Внешняя группа предлагает совместно разбирать доказательство, публиковать объяснения и изучать последствия для других задач. Отдельный вопрос — как признавать вклад тех, кто проверяет и упрощает результат, и кому предоставлять ранний доступ к материалам.
Следить за проверкой можно насайте рабочей группы. В новых публикациях стоит обращать внимание на четыре вещи:
Точную задачу: алгоритм находит решение, проверяет его существование или считает все решения.
Параметры оценки: что обозначают n и размер входа, какие величины считаются фиксированными.
Объём формальной проверки: совпадает ли доказанная теорема с главным утверждением рукописи.
Практические результаты: есть ли реализация и измерения, позволяющие говорить о скорости на реальных данных.
Если опровержение подтвердится, следующим шагом станет поиск более простых и эффективных алгоритмов. Для этого потребуется понять, какие идеи обеспечили ускорение и где ещё их можно применить.
В блоге Спешу АИI мы разбираем новые исследования, возможности нейросетей и события вокруг их разработчиков. Подписывайтесь, чтобы следить за развитием ИИ и понимать, что стоит за громкими заявлениями. А познакомиться с разными ИИ-моделями на собственных задачах можно в speshu.ai — нашем сервисе, который объединяет их в одном месте.
Почему скорость написания кода не то же самое, что скорость разработки
AI-агенту не нужен отдых. Это понятно. Но порой из этого делают куда менее полезный вывод: разработка теперь может идти без пауз. Один агент пишет код, другой проверяет, третий обновляет документацию, четвёртый что-то ищет в web, пятый осуществляет сведение общего плана и тд. Закончили задачу - берём следующую, и так аж до самой технологической сингулярности.
Казалось бы, кожаные наконец избавились от необходимости иногда прекращать делать новое и возвращаться к уже сделанному - можно просто гнать вперёд. Но здесь, как водится, есть нюанс: что именно получится после нескольких месяцев такой работы - консистентная система или коллекция условно успешно закрытых задач?
Попробуем таки подумать об этот вопрос…
Как лиса сыр делила
В сказке “Два жадных медвежонка”, соответственно - два жадных медвежонка нашли головку сыра, но поделить её не смогли - каждый боялся, что другому достанется больше. На помощь пришла лиса и разломила сыр на два неравных куска, а затем принялась исправлять: откусила от большего - теперь больше другой, откусила от другого - опять не поровну. Так и выравнивала, пока медвежатам не остались два почти что ничего.
С кодом вот примерно то же самое. Подправили один сервис, подогнали под него второй, потом побежали к следующему - там теперь тоже надо кое-что подправить и так далее. Каждый раз есть конкретная задача и вполне конкретный результат. А вся цепочка потиху обрастает костылями, пока очередной фикс не поделит её на ноль.
И тут дело в том, что агент быстрее пишет код…но также и быстрее косячит. Причём даже не в плане каких-то банальных ошибок, а в плане консистентности кодовой базы и документации. И если время от времени не останавливаться и не разбираться (при помощи AI-агентов, разумеется, а как вы думали - 2026 год на дворе), как эти части вообще должны работать вместе, то вместо системы получим конгломерат.
Код не стирается, но система меняется
Код сам по себе не стирается. Зато требования меняются, зависимости обновляются, нагрузка растёт. Также со временем даже сами разработчики (это не точно) начинают лучше понимать, что они вообще строят. Временный костыль от этого, правда, сам не исчезает.
Ещё Уорд Каннингем, вводя метафору технического долга, писал о необходимости возвращаться к реализации с учётом нового понимания задачи: сделали, разобрались лучше - теперь надо переделать. AI ускоряет первый шаг, но вот второй и третий - всё равно придётся делать.
Также при исследовании внедрения Cursor рост активности разработки оказался кратковременным, а вот рост сложности кода и предупреждений анализатора - продолжительным. Удивительно, да? Хотя, это наблюдательное исследование открытых репозиториев, так что с обобщениями надо всё же аккуратнее. Но сам вопрос открыт: разработка ускорилась или же просто код стал писаться быстрее?
Ну…кто ж его знает, да? Может у агентов спросим и пусть сами разбираются? С математикой же у них вроде что-то получается.
Обслуживать придётся и тех, кто обслуживает (рекурсия, ага)
Теперь ещё один нюанс: у агентов есть модели, тулзы, скиллы, MCP, AGENTS.md, MEMORY.md и тд, и тп - вся та обвязка, которую принято называть харнессом. И она тоже устаревает - да каждый день летят стоящие апдейты! Модель обновили, а старые инструкции оставили. Когда-то десять промежуточных шагов были нужны, потому что иначе агент терял контекст. Теперь справляется за, условно, три, но по инструкции послушно делает десять. Или инструмент уже отвечает иначе, а агент всё ещё трактует ответ по старым правилам. Память у него есть, вот только помнит он уже не то, что нужно.
Кстати, у BAntropic есть разбор такой переработки харнесса: возможности модели изменились, часть обвязки удалось убрать. Правда, попытка разом всё сильно упростить сначала ухудшила результат - пришлось проверять, что именно можно удалять.
То есть обслуживать придётся ещё и тех, кто обслуживает. Поставить над ними ещё одного агента можно, но у него тоже будут инструкции и критерии проверки. И фразу “сервис восстановлен” в любом случае надо проверять реальной операцией: красивый отчёт клиентский запрос не обработает.
Получается, теперь нужно иногда останавливаться и “смазывать AI-станок”?
Вкратце - получается, что таки да.
Обслуживание легко оставить на потом: агент не устал, новая фича почти готова, а там ещё одна - можно пока не отвлекаться. Только это абстрактное “потом” - в реальное потом - обернётся упавшим продом.
Ну и вообще, хорошо бы (хотя бы гипотетически) делить dev-timeline на три куска:
Разобрать накопившееся - найти причины сбоев, закончить миграции, выкинуть отжившие костыли, согласовать изменения между сервисами.
Делать новое - сразу вместе с интеграцией и проверками, пока ещё понятно, что и зачем поменяли.
Проверить готовность - испытать именно ту систему и тех агентов, которые будут работать под нагрузкой. И оставить время что-то исправить, если вдруг выяснится, что что-то опять решило “уйти погулять”.
То есть, при агентной разработке порой придётся просто остановливаться и разбираться с тем, что имеем - даже ценой задержки очередной фичи.
Что значит “готовность”
“Всё готово” - это вообще к чему? К обычному дню, десятикратной нагрузке, отказу зависимости? Зелёные тесты мало что объясняют, пока мы не уточнили, что именно проверяли (и пока не увидели красные, конечно).
Ну вот например у Shopify, например, к Black Friday/Cyber Monday готовятся отдельно: проверяют запас мощности, гоняют нагрузку и отказы, заранее заканчивают крупные архитектурные изменения. При том, что над надёжностью работают круглый год. Вполне понятная логика: выяснять, что система не вывозит, лучше до распродажи. А с AI-разработкой это соотносится следующим образом: иногда - особенно перед наиболее критичными событиями/ситуациями/периодами - внедрять новых фич при помощи агентов - вообще лучше не надо. А насчёт “ручного ревью” кода, написанного AI-агентами, то…если у вас реально есть на это время - вроде как лучше сразу руками и писать, а то весь профит теряется. И да, бэкапы тоже лучше делать, чем не делать, а также обязательно попробовать восстановить их. Чисто на всякий случай, ага…
Ну короче, агентам отдых действительно не нужен, а вот агентной разработке - очень даже. Иными словами, при текущем подходе порой придётся переставать разрабатывать и заниматься “смазкой AI-станка”.
Mentions
@tomcruise824458 your bots stole my stuff: formal-math#33
okay, anthropic says an internal claude model refuted the exponential time hypothesis too. claude wrote the paper, AI wrote the Lean proof. their readme: purely asymptotic, says nothing about practice. two labs, one week. no peer review on either yet. github.com/anthropics/formal-math/tree/16a5ce4130…
The Exponential Time Hypothesis Fell Twice. The Way Through Was a Minus Sign On 26 October two papers appeared within hours of each other. One, from OpenAI, is titled The Exponential Time Hypothesis is False. The other, from Anthropic, is credited to "Claude" and titled A 2^o(n) Time Algorithm for 3-SAT. Both say the same thing: the reference hard problem of computer science, which I explain below with a dinner party, can be solved faster than anyone believed possible, and a conjecture that hundreds of results were built on is false. Both come with a proof checked line by line by Lean, a program that verifies mathematics mechanically. Both were found by an AI model the labs have not released. Anthropic's paper dates its discovery to 16 October, "with 14M output tokens and no human input"; OpenAI's manuscript is dated 17 October. The headlines went for the AI-cracks-a-decades-old-puzzle angle and stopped there. That leaves out the part I find most interesting, which is how. I read both papers, and the answer is not two unrelated tricks. Both algorithms run into the same wall that every SAT algorithm since the 1980s has run into, and both get through it the same way: by solving a harder problem than the one asked, and letting negative numbers cancel. One of them does it with an identity a Danish mathematician wrote down in 1818. None of this makes any real software faster, and none of it settles P vs NP, the famous million-dollar question. I'll get to why. First, the problem, in plain words, because without it nothing else in this story makes sense. The problem: a dinner party with conditions Say you are organising a dinner and your friends have sent conditions. "I'll come if Ana comes or Bea doesn't." "At least one of Carlos and Diego." "Not Ana, Bea and Carlos all together, please." Each friend is a yes/no decision, and each condition mentions at most three friends. The question: is there any guest list that meets every condition at once? That is 3-SAT. "SAT" stands for satisfiability: can all the conditions be satisfied together? The "3" is because each condition, called a clause, involves at most three yes/no variables. Written the way computer scientists write it, a clause looks like {% katex inline %}(x_1 \lor \lnot x_2 \lor x_5){% endkatex %}: "friend 1 comes, or friend 2 doesn't, or friend 5 comes". It looks like a parlour puzzle, and it is the puzzle. In 1971 Stephen Cook showed that a huge family of problems (timetables, delivery routes, verifying that a chip has no bugs, Sudoku, and thousands more) can be translated into it. Solve 3-SAT fast and you solve all of them fast. That is why it is the reference hard problem of computer science. What makes it hard is an asymmetry. If someone hands you a guest list, checking it is trivial: go through the conditions one by one. Finding one is another matter. With {% katex inline %}n{% endkatex %} friends there are {% katex inline %}2^n{% endkatex %} possible lists: with 30 friends, about a billion; with 100, so many that a million computers each checking a billion lists per second would need some 40 million years to go through them. The question since the 1970s has been how much better than "try them all" you can do. !The asymmetry behind 3-SAT. On the left, checking one proposed guest list against three conditions takes one pass and three ticks. On the right, finding a valid list by trying them all means 2 to the n lists: 1,024 for 10 friends, about a billion for 30, and a 31-digit number for 100. The asymmetry behind 3-SAT. Checking a proposed answer is quick; finding one by trying them all doubles in cost with every friend you add. What the hypothesis said The best algorithms don't try everything; they prune, guess cleverly, and backtrack. But their running time still grows exponentially: each extra variable multiplies the work by a fixed factor, the base. For trying everything the base is 2 (one more friend, twice the lists). Schöning's random walk brought it to {% katex inline %}1.334{% endkatex %} in 1999, PPSZ with Hertli's analysis to {% katex inline %}1.308{% endkatex %}, Liu's deterministic algorithm to {% katex inline %}1.328{% endkatex %}. That sounds like a small gain and it is an enormous one: {% katex inline %}2^{100}{% endkatex %} is a 31-digit number, {% katex inline %}1.308^{100}{% endkatex %} a 12-digit one. But forty years of very clever work never brought the base close to 1. In 1999 Russell Impagliazzo and Ramamohan Paturi turned that experience into a conjecture, the Exponential Time Hypothesis (ETH): the base can be lowered but never to 1. Put precisely: there is some number {% katex inline %}c{% endkatex %} greater than 1 such that no algorithm solves every 3-SAT instance faster than {% katex inline %}c^n{% endkatex %}. However clever the algorithm, each extra variable will always cost at least that fixed multiplier. Its stronger sibling, SETH, says that when conditions can mention many variables, you cannot even lower the base much. Papers usually write the same thing with the base fixed at 2 and the change moved into the exponent. Any base {% katex inline %}c{% endkatex %} is a power of 2, {% katex inline %}c = 2^{\delta}{% endkatex %}, so {% katex inline %}c^n = 2^{\delta n}{% endkatex %}: trying everything is {% katex inline %}\delta = 1{% endkatex %}, and {% katex inline %}1.308^n{% endkatex %} is about {% katex inline %}2^{0.39n}{% endkatex %}. Lowering the base towards 1 and lowering {% katex inline %}\delta{% endkatex %} towards 0 are the same thing. In that language ETH says {% katex inline %}\delta{% endkatex %} can never go below some fixed positive number. An algorithm that breaks this is called subexponential, written {% katex inline %}2^{o(n)}{% endkatex %}: its exponent grows more slowly than {% katex inline %}\delta n{% endkatex %} for every {% katex inline %}\delta > 0{% endkatex %}. In the language of bases, the multiplier you pay per extra variable keeps shrinking towards 1 as the problem grows. It is still not fast in any everyday sense, but it is a different kind of growth, and ETH said it was impossible. !Bar chart of the best known running time for 3-SAT written as base to the n: brute force 2, Schöning 1999 1.334, Liu 2018 deterministic 1.328, PPSZ with Hertli 2014 randomized 1.308. The 2026 algorithms have an effective base that tends to 1 as n grows, which is what refutes the Exponential Time Hypothesis. Forty years of progress on 3-SAT lowered the base of the exponent. ETH bet that it could never reach 1. The new algorithms take time 2^o(n): their effective base slides to 1 as n grows. (The axis is compressed between 1.5 and 2.) That bet was not idle. Anthropic's paper reports a literature search, carried out by Claude, that found more than 800 papers proving at least one result only under ETH or something that implies it. ETH is the reason we "know" that k-Clique has no {% katex inline %}n^{o(k)}{% endkatex %} algorithm, that many parameterized algorithms are optimal, that dynamic programming over tree decompositions cannot be improved. In 2019 Ryan Williams gave two separate estimates: a 70% chance that ETH was true, and a 25% chance that SETH was true. They are not slices of one pie and are not meant to add up to 100%: SETH is the stronger claim (if it holds, ETH holds too), so it can only be the less likely of the two. Most of the field would have put both numbers higher. Both papers now give a deterministic algorithm that runs in {% katex inline %}2^{o(n)}{% endkatex %}: for every {% katex inline %}\delta > 0{% endkatex %} it is eventually faster than {% katex inline %}2^{\delta n}{% endkatex %}, which is to say it eventually beats every base above 1. That refutes ETH, SETH, Gap-ETH and the counting version #ETH in one go. The wall Here is the intuition for why the base never reached 1, and it is the same picture in both papers. Go back to the dinner. Draw each condition as a dot, and join two dots with a line when they mention the same friend. Anthropic's paper says each line "carries bits", one per shared yes/no decision. The natural shortcut is divide and conquer: split the drawing in two halves, try every possible answer for just the friends whose lines cross the split, and for each of those, solve each half on its own. If your friends form two groups that barely know each other, only a few decisions cross the split, and this is enormously faster than trying every list. The problem is that you don't get to choose the friends. Random sets of conditions, and the hard instances generally, look like expander graphs, where every way of splitting the nodes into two halves of comparable size is crossed by a constant fraction of all the edges. In the paper's words, "any algorithm that fixes one tree of cuts in advance and enumerates the crossing bits of each cut takes time {% katex inline %}2^{\Omega(n)}{% endkatex %}. Thus earlier divide and conquer ideas only improved the constant in the exponent." !Two graphs side by side. On the left, a formula whose clause graph has two loosely connected clusters: a cut between them is crossed by only two edges, so divide and conquer is cheap. On the right, an expander-like graph where every balanced cut is crossed by many edges, so enumerating the crossing bits costs exponential time whatever cut is chosen. Divide and conquer pays for the bits that cross the cut. On hard formulas every balanced cut is crossed by a constant fraction of the bits, so any fixed plan of cuts costs 2^Ω(n). This is the wall. To go through the wall you have to stop paying for every crossing bit. And there is no way to do that if every quantity you handle means "number of solutions of something", because counts of solutions are non-negative and cannot cancel. Count, don't decide So both papers do something that sounds backwards. They don't ask "is there a valid guest list?". They ask "how many valid guest lists are there?" and compute the exact number, which is the #3-SAT problem and is in principle much harder (the previous best for counting was around {% katex inline %}1.64^n{% endkatex %}, worse than for deciding). Testing whether the count is zero then decides satisfiability for free. Why make your life harder? Because a count is a sum, and a sum is algebra. The number of satisfying assignments is {% katex %} \#F = \sum_{x \in \{0,1\}^n} \prod_{\text{clauses } e} \Phi_e(x) {% endkatex %} where each {% katex inline %}\Phi_e{% endkatex %} is 1 if clause {% katex inline %}e{% endkatex %} is satisfied and 0 otherwise. A sum of products can be rearranged, rewritten, expanded and regrouped, and nothing forces the intermediate terms to be 0 or 1 or even positive. Once negative numbers are allowed in the middle of the computation, two expensive pieces can cancel into a cheap one. Branching algorithms, which ask "what if {% katex inline %}x_1{% endkatex %} is true?", can't do this: every branch is a real sub-question with a real non-negative answer. Where do negative numbers come from, if every list either works or doesn't? From subtraction, the same as at school. Take the condition "Ana comes, or Bea doesn't". Counting the lists that meet it directly is awkward, because an or ties the two friends together. Count instead all lists, minus the lists that break it. A list breaks it only when Ana stays home and Bea comes, and an and splits cleanly, one friend at a time. With just Ana and Bea there are 4 lists, exactly one of them breaks the condition, so the count is 4 − 1 = 3. In the formula above that is {% katex inline %}\Phi = 1 - (1 - x_{\text{Ana}})\,x_{\text{Bea}}{% endkatex %}. Do that for every condition and multiply out, and the count becomes a long sum of simpler terms with plus and minus signs. No single term is the number of valid lists of anything; some are negative; only the total is the count. What you gain is that each term is easy to split into independent pieces. Done naively there are far too many terms, so the work of both papers is in choosing which signed pieces to write, so that the ones linking far-apart parts of the problem cancel. That is the common move. The two papers then implement it in completely different ways. If you only want the idea, you have it: the wall is that hard problems can't be split cleanly, and the way through is to count with numbers that can be negative, so the expensive parts cancel. The next two sections show how each lab did it, with a bit more mathematics; you can skip to [What changes, and what doesn't](#what-changes-and-what-doesnt) without losing the thread. Claude's route: an identity from 1818 Anthropic's algorithm stays with the graph picture and attacks the bits that cross. Take the clause graph and merge clauses into a modest number {% katex inline %}K{% endkatex %} of big nodes, so that every pair of big nodes is joined by an edge carrying the same number {% katex inline %}\lambda{% endkatex %} of bits. The quantity to beat is the total number of crossing bits, {% katex inline %}S{% endkatex %}. Now place the nodes on a {% katex inline %}g \times g{% endkatex %} grid. Most edges are diagonals: they join two nodes in different rows and different columns. Every diagonal belongs to exactly one rectangle, and each rectangle has two diagonals: the top-left corner holds a string {% katex inline %}x{% endkatex %} that must equal the bottom-right's {% katex inline %}v{% endkatex %}, and the top-right holds {% katex inline %}y{% endkatex %}, which must equal the bottom-left's {% katex inline %}u{% endkatex %}. That pair of equality checks, {% katex inline %}[x = v]\,[y = u]{% endkatex %}, the paper calls a crossing. If you merge each row into one node, a crossing costs 6 bits per block of 3: the top row has to tell the bottom row both {% katex inline %}x{% endkatex %} and {% katex inline %}y{% endkatex %}. Here comes the identity. For blocks of 3 bits there is a sign function {% katex inline %}\sigma{% endkatex %} such that {% katex %} 2\,[x = v]\,[y = u] = [x \oplus y \oplus u \oplus v = 0]\,\big(\sigma(x,y)\,\sigma(v,u) + \sigma(x,u)\,\sigma(v,y)\big) {% endkatex %} and it can be checked by brute force on all 4,096 settings of the 12 bits. Read the right-hand side as two terms. In the first, the row choice, each {% katex inline %}\sigma{% endkatex %} depends only on one row, and the two rows only need to agree on the single 3-bit string {% katex inline %}x \oplus y = u \oplus v{% endkatex %}. That costs 3 bits, half of the 6. The second term, the column choice, is still expensive if you merged rows, but it costs only 3 bits if you merge columns instead. Neither term means anything combinatorially, they take negative values, and only their sum is a count. But each term is cheap in one direction. !A rectangle of the grid with corners holding strings x, y on top and u, v below. Its two diagonals test x equals v and y equals u, which costs six bits per block when rows are merged. The eight-square identity rewrites twice this crossing as a four-corner parity check times the sum of a row choice, whose sign functions each live in one row and cost three bits, and a column choice, which costs six bits with rows merged but three with columns merged. The eight-square identity for one rectangle. Two diagonal checks become a four-corner parity check times a signed sum of two terms. Each term is cheap along one direction of the grid, so whichever direction you merge, a share of the bits disappears. The rest is bookkeeping, done carefully. Strings are split into blocks of 3, and the expansion is grouped by how many blocks took the column choice, which keeps the number of terms polynomial. For each term the algorithm merges rows or columns, whichever is cheaper. Per block, the two directions together cost {% katex inline %}3 + 6 + 1 + 1 = 11{% endkatex %} bits against the {% katex inline %}12{% endkatex %} of two crossings, so the cheaper direction pays at most {% katex inline %}11/12{% endkatex %} of what was there before. Then it groups the merged rows into {% katex inline %}K{% endkatex %} balanced super-nodes and recurses. The paper writes the running time as {% katex inline %}2^{e S}{% endkatex %}, where {% katex inline %}S{% endkatex %} is the number of bits on the edges, proportional to the size of the formula. So {% katex inline %}e{% endkatex %} plays the role of {% katex inline %}\delta{% endkatex %} above, and {% katex inline %}2^e{% endkatex %} is the base, paid per bit instead of per variable. One level shrinks {% katex inline %}e{% endkatex %} by a factor of {% katex inline %}11/12{% endkatex %}. Repeat it and {% katex inline %}e{% endkatex %} goes to zero, which is the base going to 1: the paper's bound is {% katex inline %}e_\ell \le 1.12\,(11/12)^\ell{% endkatex %}. The price is that each level needs vastly more nodes, {% katex inline %}K_\ell = 9K_{\ell-1}^{16}{% endkatex %} starting from 64, which is why all of this only matters for astronomically large formulas. !Chart of the running-time exponent at each level of the recursion in Anthropic's algorithm. Level 0 is brute force with exponent 1. Level 1 is slightly worse, about 1.03, because the first grid is small. From level 2 on, the exponent falls by a factor of eleven twelfths per level, bounded by 1.12 times eleven twelfths to the level, reaching under 0.47 by level 10 and tending to zero. Each level of the recursion multiplies the exponent (the δ of 2^δn, so the base is 2^δ) by about 11/12. It never reaches zero at any fixed level, but it gets below any δ you name, which is exactly what refuting ETH requires. The identity is the beautiful part. Its classical form says that the product of two sums of eight squares is again a sum of eight squares. Ferdinand Degen presented it to the St Petersburg Academy in 1818, and John Graves found it again in 1843 while showing that the norm of the octonions, the eight-dimensional cousin of the complex numbers, is multiplicative. The sign function {% katex inline %}\sigma{% endkatex %} in the algorithm is, in the paper's words, "the table of signs of the multiplication of the octonions, with the basis elements renamed". Hurwitz proved in 1898 that such identities exist only for 1, 2, 4 and 8 squares. The paper has an appendix explaining why the search for a cheaper decomposition of a crossing leads straight to Hurwitz's problem, and why, under the simple bit count it uses, only eight leaves a gain: two squares break even, four break even, eight give 11 out of 12. So the thing that broke ETH is the multiplication table of the octonions, used to cut bits on a grid. OpenAI's route: deform the problem, then interpolate back OpenAI's algorithm uses the same "count, and let terms cancel" idea through a different door: interpolation. Start from the same formula for {% katex inline %}\#F{% endkatex %}. Now introduce a parameter {% katex inline %}T{% endkatex %} and replace each variable occurrence inside each clause by a linear combination of variables whose coefficients are polynomials in {% katex inline %}T{% endkatex %}. At {% katex inline %}T = 0{% endkatex %} every replacement is the original variable, so the deformed sum {% katex inline %}H(T){% endkatex %} satisfies {% katex inline %}H(0) = \#F{% endkatex %}. At the points {% katex inline %}T = 1, \dots, Q{% endkatex %}, the replacements are designed so that the variables split into small groups that interact only through a few shared "measurements", small integer linear combinations of each group's bits. Fix the values of those measurements and the sum factorizes group by group, exactly the way the clustered formula of the earlier figure would. At those points the expensive problem becomes cheap. !Sketch of OpenAI's interpolation strategy. A polynomial H of T is drawn as a curve. At T equals zero, its value is the exact number of satisfying assignments, which is hard to compute directly. At the points T equals one to Q, the problem splits into groups and is cheap, so the algorithm computes the value and a few Taylor coefficients there, drawn as short tangent marks. Because the degree of H is known, these determine H, and therefore H of zero. OpenAI's strategy: deform the counting problem into a polynomial H(T) of known degree. At T = 0 it is the count; at T = 1…Q it splits into independent groups. A few Taylor coefficients at each easy point pin down the polynomial, and with it the count. Because {% katex inline %}H{% endkatex %} is a polynomial of known degree, its values and a few derivatives at the easy points determine it completely, and you read off {% katex inline %}H(0){% endkatex %}. Interpolation here is not an approximation: it is exact rational arithmetic. The whole difficulty is in a tension between two costs. The replacements must have low degree in {% katex inline %}T{% endkatex %}, or you need too many Taylor coefficients per point. And they must respect a different grouping at each of the {% katex inline %}Q{% endkatex %} points, which naively costs degree {% katex inline %}Q{% endkatex %}. The construction that resolves it is where the minus sign comes back. It is built out of swaps: permutation matrices {% katex inline %}\Pi_s{% endkatex %} that exchange two group labels at position {% katex inline %}s{% endkatex %}, each with eigenvalues {% katex inline %}+1{% endkatex %} and {% katex inline %}-1{% endkatex %}. A basis vector with {% katex inline %}j{% endkatex %} of its positions in the {% katex inline %}-1{% endkatex %} eigenspace gets multiplied by {% katex inline %}(-1)^j{% endkatex %} under the full swap. OpenAI chooses a polynomial {% katex inline %}f{% endkatex %} that interpolates {% katex inline %}(-1)^j{% endkatex %} only on a short window of {% katex inline %}j{% endkatex %} values, centred where a binomial distribution puts almost all of its mass. Inside the window the construction is exact; the few directions outside it are paid for with explicit measurements. The window only needs to be about as wide as the binomial's standard deviation, {% katex inline %}\sqrt{Q}{% endkatex %}, and with {% katex inline %}Q \approx \log n{% endkatex %} that is where the {% katex inline %}\sqrt{\log n}{% endkatex %} in the final bound comes from. Multiply out the three costs (Taylor data, measurements, one group at a time) and each one is {% katex inline %}2^{o(n)}{% endkatex %}. The algorithm also runs in polynomial space, which Anthropic's does not claim. Same wall, same minus sign Side by side: | | OpenAI | Anthropic (Claude) | |---|---|---| | Date on the paper | 17 October, revised 25 October | 26 October; core found 16 October | | Length | 67 pages | 49 pages | | What it computes | exact #k-SAT, deterministic | exact #k-SAT, deterministic | | Bound, sparse formulas | {% katex inline %}2^{O(n/\sqrt{\log n})}{% endkatex %} | {% katex inline %}2^{O(m/\sqrt{\log m})}{% endkatex %} in the clause count | | Bound, any formula | {% katex inline %}2^{O(n \log\log n/\sqrt{\log n})}{% endkatex %} | {% katex inline %}2^{O(k^2 n \log\log n/\sqrt{\log n})}{% endkatex %} | | Bound proved in Lean | weaker: {% katex inline %}(\log\log n)^2{% endkatex %} in place of {% katex inline %}\log\log n{% endkatex %} | the main theorem as stated | | Key device | deformation + Hermite interpolation; swap matrices, {% katex inline %}f(j) = (-1)^j{% endkatex %} | grid + eight-square identity; recursion with factor 11/12 | | Space | polynomial | not claimed | The bounds land in the same place, which is either a coincidence or a hint about where the natural barrier for this family of techniques sits. Neither paper knows how to remove the {% katex inline %}\log\log n{% endkatex %} for general formulas. And the mechanisms rhyme more than they look. OpenAI's construction is literally built from swap operators with eigenvalues {% katex inline %}\pm 1{% endkatex %}. Anthropic's README compresses its own key idea into a paragraph that includes "Per bit, SWAP = I − 2·singlet", the physicist's way of writing a swap as the identity minus a signed correction. Both papers solve a harder problem so they can work with signed quantities, and both get their saving from writing an exchange of two things as a combination of cheaper things with signs. The non-negative world, where every intermediate number counts solutions of something, is exactly where ETH was true. What changes, and what doesn't Nothing changes in practice. Anthropic's paper is unusually blunt about it. For a 3-CNF with {% katex inline %}m = 5n{% endkatex %} clauses its bound beats the {% katex inline %}2^n{% endkatex %} of brute force only once {% katex inline %}n > 10^{10\,000}{% endkatex %}, and the bound in {% katex inline %}n{% endkatex %} alone only once {% katex inline %}n > 10^{10^8}{% endkatex %}. The authors add that their general approach "seems unlikely to yield any general improvement unless {% katex inline %}n > 10^7{% endkatex %}, however it is instantiated", while brute force is already impossible at {% katex inline %}n = 100{% endkatex %}. Your SAT solver, your scheduler, your verification tool are exactly as fast as last week. P vs NP is untouched. P vs NP asks whether problems like 3-SAT can be solved in polynomial time, with work growing like {% katex inline %}n^2{% endkatex %} or {% katex inline %}n^3{% endkatex %}, which is far faster than anything in these papers. ETH was a stronger bet than P ≠ NP, so losing it says nothing about the weaker one. And a {% katex inline %}2^{o(n)}{% endkatex %} bound for 3-SAT does not transfer to every NP problem, because polynomial-time reductions can blow up the number of variables polynomially, and {% katex inline %}2^{o(n)}{% endkatex %} composed with a polynomial is no longer subexponential. For problems with reductions that keep the size linear, it does transfer: OpenAI derives subexponential counting of independent sets, proper colourings and perfect matchings; Anthropic lists Independent Set, Clique, Vertex Cover and Dominating Set in {% katex inline %}O(2^{\delta n}){% endkatex %} for every {% katex inline %}\delta > 0{% endkatex %}. A shelf of theorems changed status. Everything proved "under ETH" or "under SETH" has lost its hypothesis. Some of it survives on weaker foundations: the quadratic lower bounds for edit distance and longest common subsequence also follow from the Orthogonal Vectors conjecture, which neither paper refutes. Much of it, the 800-odd papers' worth, now needs a new reason to be true or turns out to be false. And there is one genuinely unconditional gain. Through Ryan Williams's programme, which turns slightly-faster-than-brute-force SAT algorithms into circuit lower bounds, both papers get that the class {% katex inline %}E^{NP}{% endkatex %} has no Boolean circuits of linear size. OpenAI's version gives a lower bound of order {% katex inline %}n\sqrt{\log n}{% endkatex %}. The best known before, over the full binary basis, was {% katex inline %}3.1n{% endkatex %}. Circuit lower bounds are one of the most stuck areas of complexity theory, and this one came out as a side effect. What Lean checks, and what it doesn't Both results are formalized, and both teams are careful about what that means. Anthropic's README says it in one line I wish every formalization carried: "Lean checks the proofs, but no machine checks that this file says what the paper says; the file is kept short so that a reader can check this." OpenAI's Lean scope note is similarly precise: the machine-checked bound is the weaker one with {% katex inline %}(\log\log n)^2{% endkatex %}; the sharper bound in the paper is not. That is the gap I wrote about in Proved, Certified, Swept, Sampled: a green check is a statement about a specific claim, and the work is knowing which claim. Here it is handled well. The statements are short, they are printed in the papers, and the differences from the prose are listed. As I write this, human review is still under way: according to the coverage, OpenAI handed its result to outside reviewers that include Impagliazzo and Paturi themselves. A Lean proof of a correctly stated theorem leaves them very little to find, but "correctly stated" is the part they are there for. The proof that fits in a prompt One more detail, and for someone who builds with these models it is the one that stays with me. At the end of Anthropic's README there is a section titled "The key idea, in condensed form interpretable by AI models". It is a single paragraph. It starts "The exponential time hypothesis is false!", states a recursion for the cost of contracting tensor networks on a complete graph, mentions the grid, the swap, the grouping by number of singlets, and ends "Prove it." The README says that Claude Opus 5.5 at high effort can rederive the refutation, in its weaker {% katex inline %}O(2^{\delta n}){% endkatex %} form, from that paragraph alone. That is a new kind of mathematical object. For centuries a proof has been written for a human reader, at whatever level of detail that reader needs. Here there are three layers: a 49-page paper for people, a Lean development for the kernel, and a one-paragraph hint for a model, which is enough because the model can fill in the rest. When I wrote about the Navier–Stokes blow-up, the bottleneck was the opposite one: the machine's drafts were close to unreadable, and turning them into a paper a person could follow was weeks of work. Seven weeks later, the most compressed description of a major result is the one written for a machine. What to take from it - ETH is false, twice, independently, with formal proofs, pending the human review that is now under way. SETH, Gap-ETH and #ETH go with it. - The wall was the expander, and the way through was a minus sign. Both algorithms count instead of decide, so that terms can be negative and cancel. That is the one-sentence intuition, and it is the same for both. - Claude's version runs on the octonions. A 1818 identity for sums of eight squares turns two crossing equality checks into terms that are each cheap in one direction, and a recursion multiplies the exponent by 11/12 per level until it is as small as you like. - OpenAI's version deforms and interpolates. A polynomial that equals the count at 0 and splits into independent groups at {% katex inline %}1, \dots, Q{% endkatex %}, held together by swap matrices and a polynomial that imitates {% katex inline %}(-1)^j{% endkatex %} on a window under a bell curve. - No practical consequence. The crossover is beyond {% katex inline %}10^{10\,000}{% endkatex %} variables. The consequences are for theory: hundreds of conditional lower bounds lose their hypothesis, and a circuit lower bound moved for free. - Two labs, the same week, the same bound. Whatever this says about the problem, it says something about the models: the frontier of what they can find now includes a result that one of the field's leading experts, in 2019, put at 70-to-30 against. --- Sources: Anthropic's paper and Lean formalization (A 2^o(n) Time Algorithm for 3-SAT, by Claude), OpenAI's Lean scope note and paper (The Exponential Time Hypothesis is False). On the eight-square identity and the octonions: John C. Baez, "The Octonions", Bulletin of the AMS 39 (2002), 145–205; J. H. Conway and D. A. Smith, "On Quaternions and Octonions", A K Peters, 2003; A. Hurwitz, "Über die Composition der quadratischen Formen von beliebig vielen Variabeln", Nachr. Ges. Wiss. Göttingen (1898), 309–316; and Degen's eight-square identity on Wikipedia. --- Originally published on javieraguilar.ai Want to see more AI agent projects? Check out my portfolio where I showcase multi-agent systems, MCP development, and compliance automation.
Две лаборатории против одной гипотезы: что происходит вокруг ETH OpenAI и Anthropic сообщили, что их исследовательские модели нашли алгоритмы, опровергающие гипотезу экспоненциального времени — ETH. На этом предположении построены многочисленные оценки сложности вычислительных задач. Если результат выдержит проверку, исследователям придётся пересмотреть часть представлений о том, какие алгоритмы вообще возможны. Масштаб последствий зависит от того, какое ускорение обещают новые алгоритмы. Для этого нужно разобраться в связи ETH с проблемой P против NP. Что опубликовали лаборатории 26 октября 2026 года OpenAIобъявила о результатах в трёх областях: математическом анализе, теории вычислительной сложности и квантовой теории поля. Заявление об ETH относится ко второй. Компания выложила текст доказательства и его формализацию в Lean — системе проверки математических доказательств. Вскоре собственные материалыпредставила Anthropic. Компания приписывает результат внутренней исследовательской модели Claude. Заявленный алгоритм решает задачу 3-SAT за субэкспоненциальное время. Он также должен подсчитывать число удовлетворяющих формуле наборов значений. За внешнее изучение результата OpenAI взялись Райан Уильямс из MIT, Рассел Импальяццо и Рамамохан Патури из Калифорнийского университета в Сан-Диего. Воткрытом письме исследователи подчеркнули: их участие не означает, что заявленное опровержение уже получило научное подтверждение. Какую границу устанавливает ETH ETH касается задачи выполнимости булевых формул. В варианте 3-SAT формула состоит из условий, соединённых оператором «И». Каждое условие содержит до трёх переменных или их отрицаний, связанных через «ИЛИ». Нужно подобрать значения «истина» и «ложь», при которых вся формула окажется истинной. Простой пример: (x ИЛИ y ИЛИ НЕ z) И (НЕ x ИЛИ z ИЛИ w). Если x, z и w истинны, а y ложно, оба условия выполнены. Проверить предложенный набор значений нетрудно: достаточно пройти по условиям. При поиске подходящего набора готовой подсказки уже нет. У n булевых переменных есть 2ⁿ возможных наборов значений. Полный перебор проверяет их один за другим; добавление одной переменной удваивает число комбинаций. ETH утверждает более тонкую вещь: даже при другом подходе в худшем случае нельзя полностью избавиться от экспоненциальной зависимости. Пример представления булевой формулы графом и объединения групп узлов. Фрагмент иллюстрации из работы Anthropic СогласноETH, для 3-SAT нет алгоритма со временем 2^(o(n)), с точностью до полиномиальных множителей по размеру входа. Обозначение o(n) означает, что показатель растёт медленнее n: отношение этих величин стремится к нулю. Поэтому 2^(√n) — пример субэкспоненциальной зависимости, а 2^(0,01n) — всё ещё экспоненциальная. Маленький постоянный коэффициент сам по себе гипотезу не опровергает. Быстро решить много удачно подобранных формул недостаточно: нужна доказанная оценка для худшего случая. Именно такую гарантию заявляют лаборатории. Почему вопрос P против NP остаётся открытым Проблема P против NP проводит другую границу. Класс P включает задачи с ответом «да» или «нет», которые можно решить за полиномиальное время. В классе NP для положительного ответа существует свидетельство, которое можно проверить за полиномиальное время. Для 3-SAT таким свидетельством служит подходящий набор значений переменных. Если его предоставить, проверить формулу можно быстро. Вопрос в том, существует ли столь же эффективный общий способ определить, есть ли решение. «Быстро» здесь означает полиномиальную зависимость от длины входных данных, например квадрат или куб этой длины. Разницу между оценками удобно увидеть на трёх выражениях: Зависимость Тип роста Что происходит при увеличении n n³ Полиномиальный Размер входа возводится в фиксированную степень 2^(√n) Субэкспоненциальный, но сверхполиномиальный Растёт быстрее любой фиксированной степени n 2ⁿ Экспоненциальный Каждая дополнительная единица n удваивает значение Таблица иллюстрирует типы роста функций. Она не описывает измеренную скорость новых алгоритмов. Полиномиальная, субэкспоненциальная и экспоненциальная зависимости растут с разной скоростью. По вертикали показан двоичный логарифм значения функции; обе оси имеют логарифмический масштаб 3-SAT — NP-полная задача: полиномиальный алгоритм для неё дал бы полиномиальные алгоритмы для всех задач NP. ETH — более сильное предположение, чем P ≠ NP. Её истинность влечёт P ≠ NP, но опровержение ETH само по себе не устанавливает P = NP. У 3-SAT может существовать субэкспоненциальный алгоритм, который всё равно работает дольше любого полинома. Что подтверждает проверка в Lean Lean проверяет, что утверждение следует из заданных определений и аксиом. Человеку остаётся убедиться, что формализованная теорема соответствует исходной задаче. Безошибочное доказательство более слабого утверждения не подтверждает более сильное. Вописании формализации OpenAI уже видна существенная деталь. Рукопись заявляет время: 2^(O(n · log log n / √log n)). В документе о границах проверки Lean указана более слабая оценка: 2^(O(n · (log log n)² / √log n)). Оценки приведены для фиксированного k — максимальной длины условия; полиномиальные множители по размеру входа опущены. Дополнительный множитель log log n ухудшает верхнюю оценку времени. При этом обе зависимости остаются субэкспоненциальными и, если доказаны для нужной задачи, достаточны для опровержения ETH.GitHub Anthropic отдельно отмечает этот предел вREADME проекта: машина проверяет доказательства, но соответствие формальных утверждений тексту статьи требует человеческого прочтения. Для этого компания вынесла основные формулировки в отдельный короткий файл MainResults.lean.raw.githubusercontent.com Что изменится для алгоритмов и криптографии ETH использовали как исходное предположение для условных нижних оценок. Логика таких работ выглядит примерно так: «Если ETH верна, задача X не может решаться быстрее определённой границы». Опровержение предположения не делает условную теорему ошибочной, но лишает её основания для вывода о реальном пределе скорости. Сведения задач друг к другу, методы и промежуточные результаты сохраняют ценность. Здесь есть ещё одна тонкость. Из нового алгоритма для 3-SAT нельзя автоматически получить одинаковое ускорение для любой NP-полной задачи. При сведении одной задачи к другой размер входа может вырасти. Поэтому последствия нужно рассчитывать для каждого конкретного сведения, учитывая, по какому параметру измеряется сложность. Для разработчиков ПО важен следующий вопрос: при каких размерах данных новый алгоритм начинает выигрывать? Асимптотика описывает рост затрат при увеличении входа. Она скрывает постоянные коэффициенты и не сообщает, будет ли реализация полезна на доступном оборудовании. Anthropic прямо характеризует свой результат как асимптотический, без утверждений о практической скорости решения формул. По той же причине заявление об ETH не даёт оснований объявлять существующее шифрование взломанным. Для такого вывода нужен конкретный способ атаки, оценка его затрат и применимость к используемым параметрам криптосистемы. Общего утверждения об ускорении 3-SAT для этого недостаточно. Уильямс рассказал, что спросил OpenAI о возможных последствиях для криптографии. По его словам, компания проверила этот вопрос и не обнаружила оснований считать, что результат приводит к взлому криптосистем. Этопересказ ответа лаборатории в TechCrunch, а не независимый аудит безопасности. Как учёные собираются проверять результат Ранее Уильямс сравнил массовую публикацию ИИ-доказательств с DDoS-атакой на математиков: их проверка требует времени специалистов, которого новые тексты не прибавляют. Теперь OpenAI согласилась открыть материалы по ETH и профинансировать конференцию для обсуждения последствий. Участники внешней группы работают без вознаграждения от компании и без обязательств о неразглашении. Они могут публиковать собственные выводы, включая критику.openai.com Внешняя группа предлагает совместно разбирать доказательство, публиковать объяснения и изучать последствия для других задач. Отдельный вопрос — как признавать вклад тех, кто проверяет и упрощает результат, и кому предоставлять ранний доступ к материалам. Следить за проверкой можно насайте рабочей группы. В новых публикациях стоит обращать внимание на четыре вещи: Точную задачу: алгоритм находит решение, проверяет его существование или считает все решения. Параметры оценки: что обозначают n и размер входа, какие величины считаются фиксированными. Объём формальной проверки: совпадает ли доказанная теорема с главным утверждением рукописи. Практические результаты: есть ли реализация и измерения, позволяющие говорить о скорости на реальных данных. Если опровержение подтвердится, следующим шагом станет поиск более простых и эффективных алгоритмов. Для этого потребуется понять, какие идеи обеспечили ускорение и где ещё их можно применить. В блоге Спешу АИI мы разбираем новые исследования, возможности нейросетей и события вокруг их разработчиков. Подписывайтесь, чтобы следить за развитием ИИ и понимать, что стоит за громкими заявлениями. А познакомиться с разными ИИ-моделями на собственных задачах можно в speshu.ai — нашем сервисе, который объединяет их в одном месте.
Почему скорость написания кода не то же самое, что скорость разработки AI-агенту не нужен отдых. Это понятно. Но порой из этого делают куда менее полезный вывод: разработка теперь может идти без пауз. Один агент пишет код, другой проверяет, третий обновляет документацию, четвёртый что-то ищет в web, пятый осуществляет сведение общего плана и тд. Закончили задачу - берём следующую, и так аж до самой технологической сингулярности. Казалось бы, кожаные наконец избавились от необходимости иногда прекращать делать новое и возвращаться к уже сделанному - можно просто гнать вперёд. Но здесь, как водится, есть нюанс: что именно получится после нескольких месяцев такой работы - консистентная система или коллекция условно успешно закрытых задач? Попробуем таки подумать об этот вопрос… Как лиса сыр делила В сказке “Два жадных медвежонка”, соответственно - два жадных медвежонка нашли головку сыра, но поделить её не смогли - каждый боялся, что другому достанется больше. На помощь пришла лиса и разломила сыр на два неравных куска, а затем принялась исправлять: откусила от большего - теперь больше другой, откусила от другого - опять не поровну. Так и выравнивала, пока медвежатам не остались два почти что ничего. С кодом вот примерно то же самое. Подправили один сервис, подогнали под него второй, потом побежали к следующему - там теперь тоже надо кое-что подправить и так далее. Каждый раз есть конкретная задача и вполне конкретный результат. А вся цепочка потиху обрастает костылями, пока очередной фикс не поделит её на ноль. И тут дело в том, что агент быстрее пишет код…но также и быстрее косячит. Причём даже не в плане каких-то банальных ошибок, а в плане консистентности кодовой базы и документации. И если время от времени не останавливаться и не разбираться (при помощи AI-агентов, разумеется, а как вы думали - 2026 год на дворе), как эти части вообще должны работать вместе, то вместо системы получим конгломерат. Код не стирается, но система меняется Код сам по себе не стирается. Зато требования меняются, зависимости обновляются, нагрузка растёт. Также со временем даже сами разработчики (это не точно) начинают лучше понимать, что они вообще строят. Временный костыль от этого, правда, сам не исчезает. Ещё Уорд Каннингем, вводя метафору технического долга, писал о необходимости возвращаться к реализации с учётом нового понимания задачи: сделали, разобрались лучше - теперь надо переделать. AI ускоряет первый шаг, но вот второй и третий - всё равно придётся делать. Также при исследовании внедрения Cursor рост активности разработки оказался кратковременным, а вот рост сложности кода и предупреждений анализатора - продолжительным. Удивительно, да? Хотя, это наблюдательное исследование открытых репозиториев, так что с обобщениями надо всё же аккуратнее. Но сам вопрос открыт: разработка ускорилась или же просто код стал писаться быстрее? Ну…кто ж его знает, да? Может у агентов спросим и пусть сами разбираются? С математикой же у них вроде что-то получается. Обслуживать придётся и тех, кто обслуживает (рекурсия, ага) Теперь ещё один нюанс: у агентов есть модели, тулзы, скиллы, MCP, AGENTS.md, MEMORY.md и тд, и тп - вся та обвязка, которую принято называть харнессом. И она тоже устаревает - да каждый день летят стоящие апдейты! Модель обновили, а старые инструкции оставили. Когда-то десять промежуточных шагов были нужны, потому что иначе агент терял контекст. Теперь справляется за, условно, три, но по инструкции послушно делает десять. Или инструмент уже отвечает иначе, а агент всё ещё трактует ответ по старым правилам. Память у него есть, вот только помнит он уже не то, что нужно. Кстати, у BAntropic есть разбор такой переработки харнесса: возможности модели изменились, часть обвязки удалось убрать. Правда, попытка разом всё сильно упростить сначала ухудшила результат - пришлось проверять, что именно можно удалять. То есть обслуживать придётся ещё и тех, кто обслуживает. Поставить над ними ещё одного агента можно, но у него тоже будут инструкции и критерии проверки. И фразу “сервис восстановлен” в любом случае надо проверять реальной операцией: красивый отчёт клиентский запрос не обработает. Получается, теперь нужно иногда останавливаться и “смазывать AI-станок”? Вкратце - получается, что таки да. Обслуживание легко оставить на потом: агент не устал, новая фича почти готова, а там ещё одна - можно пока не отвлекаться. Только это абстрактное “потом” - в реальное потом - обернётся упавшим продом. Ну и вообще, хорошо бы (хотя бы гипотетически) делить dev-timeline на три куска: Разобрать накопившееся - найти причины сбоев, закончить миграции, выкинуть отжившие костыли, согласовать изменения между сервисами. Делать новое - сразу вместе с интеграцией и проверками, пока ещё понятно, что и зачем поменяли. Проверить готовность - испытать именно ту систему и тех агентов, которые будут работать под нагрузкой. И оставить время что-то исправить, если вдруг выяснится, что что-то опять решило “уйти погулять”. То есть, при агентной разработке порой придётся просто остановливаться и разбираться с тем, что имеем - даже ценой задержки очередной фичи. Что значит “готовность” “Всё готово” - это вообще к чему? К обычному дню, десятикратной нагрузке, отказу зависимости? Зелёные тесты мало что объясняют, пока мы не уточнили, что именно проверяли (и пока не увидели красные, конечно). Ну вот например у Shopify, например, к Black Friday/Cyber Monday готовятся отдельно: проверяют запас мощности, гоняют нагрузку и отказы, заранее заканчивают крупные архитектурные изменения. При том, что над надёжностью работают круглый год. Вполне понятная логика: выяснять, что система не вывозит, лучше до распродажи. А с AI-разработкой это соотносится следующим образом: иногда - особенно перед наиболее критичными событиями/ситуациями/периодами - внедрять новых фич при помощи агентов - вообще лучше не надо. А насчёт “ручного ревью” кода, написанного AI-агентами, то…если у вас реально есть на это время - вроде как лучше сразу руками и писать, а то весь профит теряется. И да, бэкапы тоже лучше делать, чем не делать, а также обязательно попробовать восстановить их. Чисто на всякий случай, ага… Ну короче, агентам отдых действительно не нужен, а вот агентной разработке - очень даже. Иными словами, при текущем подходе порой придётся переставать разрабатывать и заниматься “смазкой AI-станка”.
It remains to be verified. The people looking into includes someone who stated the hypothesis originally. I have been very critical of their math dumps, tbc. But given that another group also gave an algorithm github.com/anthropics/formal-math/blob/16a5ce4130… it should be easy to do the complexity analysis / correctness.
Independent paper with claimed proof of the same result (I don't know if the algorithm is the same) by Anthropic; tbh the Anthropic paper seems *much* easier for me (a non expert) to read. github.com/anthropics/formal-math/tree/16a5ce4130…
and but also: github.com/anthropics/formal-math/tree/16a5ce4130… and uhh... where.. oh... heyyy.. hi... uhm, how can.. how does one get into that sweet /pldb? lmk if you need a hand, hmu,,, ok byyyye! 😅
OpenAI annuncia che la sua IA ha confutato l'Ipotesi del tempo esponenziale e dimostrato l'esistenza della teoria di Yang–Mills; 6 ore dopo Anthropic pubblica la sua confutazione: 67 e 49 pagine, entrambe datate 16 ottobre, nessuna verifica indipendente e la prova di fisica ancora non pubblica Lunedì 26 ottobre 2026 OpenAI ha annunciato tre risultati scientifici prodotti dai suoi modelli interni, in matematica, informatica teorica e fisica. Poche ore dopo Anthropic ha pubblicato una dimostrazione propria di uno dei tre, con la stessa data di scoperta. Scientific American parla di esperti «ancora storditi». Nessuno dei tre risultati, per ora, è stato confermato in modo indipendente. I tre annunci di OpenAI 1. Matematica. Una dimostrazione della congettura di local smoothing proposta da Christopher Sogge nel 1991, valida in ogni dimensione. Riguarda il modo in cui le onde si concentrano, e implica la congettura di Kakeya, finora dimostrata solo in 3 dimensioni da Hong Wang e Joshua Zahl nel 2025 (un lavoro che è valso a Wang la Medaglia Fields). OpenAI dice di aver ottenuto il risultato il 18 ottobre e di averlo formalizzato in Lean il giorno dopo. Articolo e prova formale sono pubblici. 2. Informatica. La confutazione dell'Ipotesi del tempo esponenziale (ETH), formulata nel 2001 da Russell Impagliazzo e Ramamohan Paturi: l'idea che il problema 3-SAT non si possa risolvere in meno di un tempo esponenziale. Secondo OpenAI è stata usata come base in «centinaia di articoli». Data dichiarata della scoperta: 16 ottobre. Articolo di 67 pagine e prova in Lean sono pubblici. 3. Fisica. Una prova matematicamente rigorosa dell'esistenza della teoria di Yang–Mills pura, della cromodinamica quantistica (QCD) e di un completamento unificato del Modello Standard in 4 dimensioni. I modelli l'avrebbero prodotta tra il 9 e il 18 settembre. Di questa prova non è pubblico nulla. Lo stesso risultato, due aziende, sei ore OpenAI ha caricato i file su GitHub alle 21:52 del 26 ottobre (ora italiana). Alle 04:07 del 27 ottobre Anthropic ha pubblicato sul proprio GitHub un articolo di 49 pagine intitolato «Un algoritmo per 3-SAT in tempo 2^o(n)», firmato «Claude, Anthropic», con la sua prova in Lean. Anthropic scrive che l'algoritmo è stato trovato il 16 ottobre «da un modello interno di ricerca Claude con 14 milioni di token in uscita e nessun intervento umano». Lo stesso giorno, per tutte e due. Ma la data è dichiarata dalle aziende stesse: le uniche prove con data verificabile sono i commit su GitHub del 26 e 27 ottobre. L'annuncio di OpenAI non nomina Anthropic, mentre l'articolo di Anthropic parla di risultati trovati «in modo indipendente e simultaneo» e cita quello di OpenAI. Cosa NON cambia - P contro NP resta aperto. Un algoritmo più veloce dell'esponenziale non è un algoritmo polinomiale, e lo scrivono tutti e due gli articoli. Anthropic aggiunge che il risultato «non dice nulla sulla risoluzione delle formule nella pratica»: per formule tipiche il limite dimostrato batte la ricerca esaustiva solo oltre 10^10.000 variabili, e il metodo difficilmente darebbe vantaggi sotto i 10 milioni. La crittografia di tutti i giorni non è toccata. - Il problema del Millennio non è risolto. Il premio Clay da un milione di dollari chiede due cose: che la teoria di Yang–Mills esista e che abbia un mass gap. OpenAI rivendica solo la prima parte. In più il Clay Institute valuta una soluzione solo dopo la pubblicazione su una rivista e almeno 2 anni di accettazione da parte della comunità. - Una prova in Lean non basta da sola. Il computer controlla che i passaggi siano corretti, ma non che l'enunciato formale dica davvero quello che i matematici intendono. Il README di Anthropic lo scrive esplicitamente. Chi controlla, e la polemica OpenAI ha scelto dei «pastori» esterni. Per l'ETH, Impagliazzo e Paturi, cioè gli stessi che la formularono, più Ryan Williams del MIT. Per la fisica, un gruppo guidato da David Gross, premio Nobel 2004, con Arthur Jaffe, che scrisse il problema del Millennio insieme a Edward Witten. I tre informatici hanno scritto ai colleghi: «Il nostro coinvolgimento non va inteso come una certificazione». L'AGMAI, un gruppo di matematici ospitato dall'Institute for Advanced Study di Princeton e nato proprio dopo le critiche ai precedenti rilasci di OpenAI, aveva raccomandato il 25 ottobre, un giorno prima dell'annuncio, di non designare esperti prescelti, per rischi come «accesso diseguale» e «reputazione presa in prestito». Il 26 ottobre ha chiesto a OpenAI di pubblicare «senza ritardo» la prova di Yang–Mills: «non c'è alcuna ragione scientifica per ritardare oltre». Scientific American ricorda anche che il modello resta proprietario, e che prompt, tempo di calcolo e catene di ragionamento non sono stati resi pubblici. Sul fronte Yang–Mills c'era già una corsa: il matematico Ethan Sussman (Northwestern), insieme a un dipendente di Anthropic, stava completando con dei modelli linguistici il programma di Tadeusz Balaban degli anni '80. Secondo la rivista, OpenAI li avrebbe preceduti, ma senza una prova pubblica. Il punto che resta Per la prima volta due aziende private rivendicano lo stesso risultato di frontiera nello stesso giorno, e una di loro tiene riservata la prova di un risultato che tocca un problema del Millennio. Il giudizio finale resta alla comunità scientifica. Ma decidere chi vede per primo i dati, e quando, oggi lo decidono le aziende. Domanda per voi: una scoperta fatta da un modello chiuso, con la prova trattenuta e la verifica affidata a esperti scelti dall'azienda, va considerata scienza a tutti gli effetti finché la comunità non la verifica? E chi dovrebbe decidere i tempi di pubblicazione: l'azienda, i revisori o nessuno dei due? Fonti - OpenAI, annuncio del 26/10/2026: openai.com - OpenAI, articolo "The Exponential Time Hypothesis is False" (67 pp.) e prove Lean: github.com/openai/math/tree/main/preprints/The-Ex… - Anthropic, "A 2^o(n) Time Algorithm for 3-SAT" (49 pp.) e prova Lean: github.com/anthropics/formal-math/tree/main/eth - Scientific American, 27/10/2026: scientificamerican.com - Papex, analisi con le dichiarazioni AGMAI e la lettera di Impagliazzo, Paturi e Williams: papex.org - Clay Mathematics Institute, il problema Yang–Mills e il mass gap: claymath.org
A 2^O(n) Time Algorithm for 3-SAT Discussion