A Bauhaus-style branching network of black squares, with a red path connecting to blue circles and yellow squares.

OpenAI and Anthropic have independently presented algorithms that could overturn a fundamental assumption in computer science. No, they haven't solved P vs NP. And no, your laptop isn't about to solve every impossible problem.

Something rather extraordinary has happened in theoretical computer science.

OpenAI has published a paper titled The Exponential Time Hypothesis is False.

Anthropic has published another, called A 2ᵒ⁽ⁿ⁾ Time Algorithm for 3-SAT.

Different papers.

Different mathematical approaches.

The same rather ambitious conclusion.

One of the fundamental assumptions about how difficult certain computational problems must be may be wrong.

And to make the situation even more interesting, both results emerged from AI-assisted mathematical research.

Anthropic explicitly attributes its central discovery to an internal research Claude model.

OpenAI has also released its result as part of its AI-generated mathematical research programme.

If the proofs survive independent scrutiny, this could be a major development in complexity theory.

But before anybody announces that AI has solved mathematics, defeated cryptography and rendered half the world's computer scientists unemployed, there's something we need to understand.

What exactly has been disproved?

And why does it matter?

First, a problem involving an unreasonable number of switches

Imagine a collection of switches.

Each switch has only two possible positions.

On or off.

True or false.

Now imagine a series of logical requirements involving those switches.

For example:

At least one of switches A, B or C must be on.

At least one of A being off, C being on or D being on must be true.

And so on.

Every requirement contains three conditions connected by OR.

All the requirements are connected by AND.

The question is simple.

Can you find a configuration of the switches that satisfies every requirement simultaneously?

This is essentially the problem called 3-SAT, or 3-satisfiability.

SAT stands for Boolean satisfiability.

And the number three refers to the number of literals allowed in each clause.

A literal is a variable or its negation.

It's a deceptively simple problem.

With ten variables, there are 1,024 possible assignments.

With twenty variables, there are more than a million.

With a hundred variables, the number of possible assignments becomes astronomical.

Of course, nobody sensible solves serious SAT problems by blindly examining every possible combination.

Modern algorithms use sophisticated search strategies, logical inference, pruning and various mathematical tricks.

Many practical SAT instances can be solved remarkably efficiently.

But the worst-case problem remains a fundamental challenge.

And for decades, computer scientists have believed there is a limit to how much its exponential growth can be reduced.

That belief is what the new papers challenge.

Why 3-SAT matters far beyond logic puzzles

3-SAT occupies a special place in theoretical computer science.

The general satisfiability problem was the first problem proved NP-complete through the Cook–Levin theorem.

3-SAT became one of the canonical NP-complete problems through subsequent reductions.

In simple terms, NP-complete problems are among the most difficult problems in the class NP.

If we discovered a polynomial-time algorithm for any NP-complete problem, we could use polynomial-time reductions to solve every problem in NP in polynomial time.

That would establish P = NP.

One of the most famous unresolved questions in mathematics and computer science.

But the new papers aren't claiming that.

They concern a different, more specific hypothesis.

And understanding the difference is essential.

P vs NP isn't the same as ETH

The Exponential Time Hypothesis, or ETH, was introduced by Russell Impagliazzo and Ramamohan Paturi around the beginning of this century.

Its basic claim is that 3-SAT requires exponential time in the worst case.

Not necessarily the naïve 2ⁿ exhaustive search.

We already know algorithms that perform substantially better than that.

ETH says something more subtle.

No matter how ingenious our algorithms become, there is no general algorithm for 3-SAT whose running time is subexponential in the number of variables.

In asymptotic notation, the hypothesis rules out algorithms running in:

2ᵒ⁽ⁿ⁾

Here, n is the number of variables.

The little o means that the exponent grows more slowly than every fixed positive multiple of n.

This is different from ordinary exponential algorithms such as 2^(0.5n).

That would still be exponential in n, even though it's enormously faster than 2ⁿ.

A subexponential algorithm has an exponent that becomes an increasingly small fraction of n as the problem grows.

And that's precisely what both laboratories claim to have found.

Not a polynomial-time algorithm.

Not a magical instant solution.

But an algorithm that crosses a mathematical boundary previously believed to be impassable.

Then OpenAI published a rather alarming title

On October 25, 2026, OpenAI dated a preprint with the wonderfully understated title:

The Exponential Time Hypothesis is False.

No question mark.

No Towards a Possible Improvement.

Straight to the conclusion.

The paper describes a deterministic algorithm for exactly counting the satisfying assignments of a Boolean formula in conjunctive normal form.

For every fixed clause width k, it claims subexponential running time and polynomial space.

The approach uses several mathematical techniques, including sparse parity tests, algebraic representations and polynomial interpolation.

The interesting part is that the algorithm doesn't merely answer the usual SAT question.

Does at least one solution exist?

It addresses the more demanding counting problem.

How many satisfying assignments exist?

That's the distinction between SAT and #SAT.

In ordinary SAT, you're looking for a yes-or-no answer.

In #SAT, you want the exact count.

Suppose a formula has 17,384 satisfying assignments.

A counting algorithm must return that number.

Not merely confirm that the answer is greater than zero.

And if the exact count is zero, then the formula is unsatisfiable.

So an algorithm that counts solutions can also decide whether any solution exists.

That's why an exact subexponential counting algorithm would be enough to refute ETH.

The paper claims considerably more than a clever shortcut for one narrow example.

It claims a general algorithmic result.

Which, if correct, would be a very big deal.

Anthropic arrived with a different argument

Then Anthropic published its own work.

A 2ᵒ⁽ⁿ⁾ Time Algorithm for 3-SAT.

The conclusion is similar.

The method is different.

Anthropic's approach centres on tensor-network constructions and algorithms for contracting those networks.

This isn't simply another presentation of OpenAI's algebraic method.

The two teams approached the problem through different mathematical machinery.

And Anthropic's publication has an additional detail that deserves attention.

According to its research statement, the core algorithm was discovered on October 16 by an internal Claude research model.

Anthropic says the model generated approximately 14 million output tokens during the discovery process, without human input to that research run.

Human researchers subsequently worked with Claude to improve the presentation.

That's a remarkable account of AI-assisted mathematical discovery.

But it also raises an immediate question.

How do we verify something like this?

A complicated proof produced by an AI model isn't automatically trustworthy because it looks mathematical.

Anyone who has used language models extensively knows that they can produce very convincing explanations of things that aren't true.

And mathematical arguments are particularly dangerous in this respect.

A proof can look impeccable for dozens of pages while containing one subtle mistake that destroys the entire conclusion.

Fortunately, the researchers didn't simply ask us to trust the prose.

The proofs come with something more substantial than confidence

Both teams released formal mathematical material in Lean.

Lean is a proof assistant.

Instead of merely reading an informal argument and deciding whether it sounds persuasive, a proof assistant checks formal derivations against explicitly defined mathematical rules.

That's a significant advance over the traditional approach of publishing an intimidating paper and hoping enough experts can find time to examine it.

Anthropic's repository includes Lean statements representing the main counting theorem and the claimed refutation of ETH.

It also provides a formal proof and instructions for checking it.

Its documentation describes verification with Lean and an additional independently implemented checker.

OpenAI likewise published a Lean formalization related to its algorithm.

There's a subtle but important distinction in the OpenAI materials.

The running-time bound established in the Lean formalization is somewhat weaker than the sharpest bound stated in the accompanying paper.

But it is still subexponential.

So the formally established bound would still be sufficient for the central conclusion about ETH.

That matters.

However, formal verification isn't the end of the story.

Lean can check whether a theorem follows from its formal definitions and assumptions.

It doesn't automatically establish that those definitions faithfully represent every intended claim in the natural-language paper.

Or that there isn't an important mismatch between the mathematical model and the real computational problem.

Those connections still require expert examination.

The repositories themselves acknowledge aspects of this distinction.

Which is why I wouldn't yet describe the entire matter as an unquestioned, universally accepted theorem.

A machine-checked proof is powerful evidence. But the statement being checked matters just as much as the correctness of the derivation.

And the mathematical community now has some serious reviewing to do.

What does subexponential actually buy us?

Here's where things become slightly less exciting for anyone expecting a new application next week.

Both algorithms are still extremely expensive in their general asymptotic bounds.

A representative bound from the papers has the form:

2^(O(n log log n / √(log n)))

That expression looks unpleasant.

But the important feature is simple.

As n becomes enormous, the exponent grows more slowly than a fixed positive fraction of n.

Eventually, the algorithm's growth becomes asymptotically better than ordinary exponential-time algorithms.

That's enough to contradict ETH.

But eventually is doing a considerable amount of work in that sentence.

The constants hidden inside the notation matter.

The lower-order terms matter.

The cost of constructing the relevant mathematical objects matters.

And the problem sizes at which an asymptotic improvement becomes practically useful can be unimaginably large.

It is entirely possible for an algorithm to represent a revolutionary theoretical discovery while remaining useless for actual SAT solving.

At least in its current form.

This is an important distinction in computer science.

A better asymptotic complexity bound is not automatically a faster practical algorithm.

And the authors aren't claiming otherwise.

Anthropic's own README explicitly warns that its result is purely asymptotic and says nothing about solving formulas efficiently in practice.

So no, don't uninstall your SAT solver.

And don't expect tomorrow's laptops to start solving previously impossible scheduling and optimisation problems instantly.

And no, P vs NP hasn't been solved

This is probably the most important clarification.

ETH is stronger than the statement P ≠ NP.

If ETH is true, then P ≠ NP.

But the reverse doesn't necessarily follow.

It is possible for 3-SAT to require superpolynomial time without requiring exponential time.

There is a vast mathematical territory between polynomial and exponential complexity.

For example, a running time of

2^√n

is subexponential.

But it isn't polynomial.

An algorithm with that running time can refute ETH without establishing that P = NP.

The same principle applies to the much more complicated bounds in these papers.

So even if both proofs are completely correct, the P vs NP problem remains unresolved.

Nor should we assume that every NP-complete problem suddenly receives an equally good subexponential algorithm in its own natural input size.

Polynomial-time reductions preserve polynomial-time solvability.

They don't necessarily preserve the exact exponent or the relevant problem-size parameter.

For fine-grained complexity, those details matter enormously.

The result would therefore change our understanding of one foundational computational limit.

It wouldn't erase computational difficulty.

An unfortunate disappointment for anyone hoping that optimisation problems were about to become trivial.

The consequences for complexity theory could be enormous

Now comes the genuinely important part.

ETH isn't just an isolated conjecture sitting quietly in a mathematics textbook.

It is used throughout theoretical computer science.

Researchers prove results of the form:

This problem cannot have an algorithm faster than a particular bound, assuming ETH is true.

Such results are called conditional lower bounds.

They're extremely useful.

They help us understand the likely limits of algorithms for scheduling, graph problems, combinatorial optimisation, parameterised complexity and many other areas.

They tell researchers when a particular search for a dramatically faster algorithm is probably futile.

But if ETH is false, then conclusions relying on it need to be reconsidered.

Not every conditional lower bound automatically becomes a false statement.

Some may still be true for other reasons.

Some may admit stronger independent proofs.

Others may need entirely different foundations.

And some previously pessimistic assumptions about algorithmic possibilities may become worth revisiting.

That's why the result matters even if the actual algorithm is too slow to run.

A foundational hypothesis is a structural support inside a much larger body of research.

Remove it, and you have to examine what was built on top.

Not necessarily demolish everything.

But certainly inspect the foundations.

What does any of this have to do with AI?

There's a tempting but slightly misleading answer.

SAT and optimisation problems appear in many areas connected to artificial intelligence.

Planning.

Constraint satisfaction.

Formal verification.

Scheduling.

Automated reasoning.

Therefore, if we have a faster SAT algorithm, AI itself must become dramatically faster.

Unfortunately, the story isn't that simple.

The new constructions don't currently provide an established practical speedup for those applications.

Their theoretical advantages appear in asymptotic complexity, not demonstrated production workloads.

So the immediate AI significance lies somewhere else.

AI systems are increasingly participating in mathematical discovery itself.

Not merely searching for papers.

Not simply explaining theorems.

And not only helping researchers write proof-assistant code.

In Anthropic's account, an AI research model found the central algorithmic idea.

OpenAI's work is part of a broader programme in which models generate mathematical results and formal proofs.

That's a different kind of development.

And perhaps, over the long term, an equally important one.

Because the traditional assumption has been that AI might accelerate routine mathematical work while humans provided the difficult conceptual breakthroughs.

These examples challenge that division.

At least enough to make it worth investigating carefully.

But they also create a new problem.

Verification.

If frontier models can produce major mathematical claims faster than researchers can independently understand them, how do we establish which ones are correct?

How do we organise review?

Who receives credit?

How do we distinguish a machine-checked formal result from an informal mathematical interpretation?

And how do we prevent a flood of impressive-looking claims from overwhelming the people responsible for evaluating them?

The ETH story isn't only about algorithms.

It's also about how mathematics itself may change when the production of potential discoveries becomes much cheaper.

Two different proofs are better than one. But they aren't a consensus.

I find the timing particularly interesting.

Two leading AI laboratories.

Two different mathematical approaches.

Two claimed refutations of the same longstanding hypothesis.

Both accompanied by formal verification work.

It would be tempting to say that the coincidence settles the matter.

It doesn't.

Two independent approaches can provide stronger evidence than two copies of the same argument.

But neither is automatically an independent review of the other.

And mathematical correctness isn't determined by the number of organisations making a claim.

One fully correct proof would be sufficient to refute ETH.

Two incorrect proofs would accomplish nothing.

The task now is to understand and validate the arguments.

In particular, specialists need to examine whether the computational models, asymptotic bounds, reductions and formal statements capture precisely what is being claimed.

The released material makes that examination possible.

But public availability and successful proof-assistant checks shouldn't be confused with completed independent mathematical consensus.

As of this writing in early November 2026, I would describe the result as an extraordinary and potentially transformative claim supported by substantial formal artifacts.

Not yet as a settled chapter in every complexity-theory textbook.

A rather interesting moment for mathematics

I've recently written about several research projects that challenge longstanding assumptions about AI itself.

Training without ordinary backpropagation.

Evolutionary optimisation of small parameter sets.

Learning better representations through carefully structured examples.

All of them ask variations of the same question.

Are we using the best possible methods, or simply the methods that have become conventional?

The new ETH papers ask a related question about computation.

Perhaps the algorithms we believed to be unavoidable weren't unavoidable after all.

Perhaps the constraints weren't where we thought they were.

Perhaps a problem can remain extraordinarily difficult without requiring precisely the kind of exponential growth we've long assumed.

If the results survive review, that would be a remarkable shift.

And it would be doubly remarkable that AI played a role in finding the alternative.

But I'd resist the temptation to turn this into another story about machines instantly conquering a field.

The more interesting story is about mathematics becoming a collaboration among human researchers, AI systems and formal verification tools.

A new result is proposed.

A formal proof is constructed.

The definitions are inspected.

The claims are challenged.

And only then does the community begin to understand what has actually changed.

That process matters.

Especially when the conclusion is something as extraordinary as overturning ETH.

The boundary may have moved. We still need to know where.

So what should we take away from this?

Not that P = NP.

Not that computational complexity has disappeared.

Not that every NP-complete problem is suddenly easy.

And certainly not that an ordinary computer will soon solve every difficult optimisation task we throw at it.

The real possibility is subtler.

One of the fundamental boundaries we believed constrained algorithms may not exist in the form we thought.

That's a substantial claim.

It changes the questions researchers can ask.

The lower bounds they can rely on.

And potentially the directions in which they search for better algorithms.

Meanwhile, the process that produced these results raises its own important questions about AI-assisted discovery and mathematical verification.

I don't know whether the papers will survive every level of scrutiny.

That's precisely why scrutiny exists.

But I find the situation fascinating.

For decades, theoretical computer science has developed increasingly sophisticated arguments about what computers probably cannot do efficiently.

Now AI systems are helping produce arguments that some of those limits may have been drawn in the wrong places.

Perhaps that's the beginning of a new era of algorithm design.

Perhaps it's the beginning of an unusually demanding review process.

Most likely, it's both.

The algorithms are still painfully slow.

The implications may be extraordinarily fast.

And the hardest part may now be understanding exactly what has been proved.


Sources

Editorial note: This review describes claims released in October 2026 and their reported formal-verification status as of November 4, 2026. It is not an independent mathematical verification of either proof.

Keep reading

Explore the writing archive →

Stay in touch

More essays and updates on ABVX Substack.

Read and subscribe on Substack →