October 31, 2026 | Artificial intelligence and theoretical computer science. OpenAI and Anthropic have released AI-assisted mathematical work claiming to overturn the Exponential Time Hypothesis (ETH), a central conjecture in fine-grained complexity theory. Both have made technical materials and Lean formalizations public. These are substantial, verifiable research releases, but publication and formal checking should not be confused with broad independent scientific acceptance.

What happened?

In its October 26 announcement, OpenAI says its models produced a natural-language disproof on October 16 and formalized it in Lean on October 17. The October 25 revised manuscript describes a deterministic exact-counting algorithm for fixed-width CNF formulas. Anthropic independently released A 2^{o(n)} Time Algorithm for 3-SAT and a Lean 4 formalization. Independent in this context describes the research artifacts, not a completed external validation process.

Why ETH matters

The Exponential Time Hypothesis states, roughly, that deciding satisfiability of 3-CNF formulas with n variables cannot be accomplished in subexponential time in the worst case. The 3-SAT problem asks whether true-or-false assignments exist that satisfy a collection of logical clauses. Exhaustive search considers as many as 2^n assignments; clever algorithms improve this, but ETH posits a fundamental asymptotic barrier.

The conjecture is widely used to derive conditional lower bounds for algorithms in graph theory, optimization and other combinatorial domains. It is not itself a proven theorem, which is why a correctly proved counterexample would be so consequential.

OpenAI's claimed algorithmic breakthrough

The published manuscript claims a deterministic algorithm that exactly counts satisfying assignments of arbitrary fixed-k CNF formulas using polynomial space and time bounded by a polynomial factor times 2 raised to n divided by a growing logarithmic factor. In particular, its running time is 2^{o(n)} up to polynomial factors. Exact counting goes beyond deciding whether an assignment exists: a nonzero count yields a satisfiable formula. Hence the claim, if correct, directly contradicts ETH for 3-SAT.

OpenAI discusses stronger conditional consequences, including ramifications for related exponential-time hypotheses and some counting problems. Those claims need to be evaluated against the precise stated reductions and proof details.

Anthropic's independent technical release

Anthropic's research repository claims a deterministic subexponential-time algorithm for 3-SAT and #3-SAT, with a runtime of the order of 2^{O(n log log n / sqrt(log n))}. Its authors explicitly state that the result is purely asymptotic: it says nothing about making real SAT instances practical to solve on today's hardware. They provide a Lean 4 artifact as well as a paper.

What does Lean verification establish?

Lean is a formal proof assistant. It checks derivations against explicit definitions and accepted logical rules, helping expose gaps that prose arguments may miss. But a green checkmark is not the end of independent review. Specialists must inspect whether the formal theorem accurately corresponds to the claimed complexity-theoretic result, whether all assumptions are appropriate and whether the machine model and input encoding match the paper.

OpenAI's formalization-scope document is valuable because it specifies exactly what its Lean proof checks and distinguishes those bounds from sharper variants described in the manuscript. Scrutiny of these details is normal mathematical practice.

Five misconceptions to avoid

  • This does not prove P = NP. A subexponential algorithm is not a polynomial-time algorithm.
  • It does not automatically give subexponential algorithms for every NP problem. Polynomial reductions can inflate input size.
  • It does not instantly solve production optimization workloads. Asymptotic improvements may still be computationally prohibitive.
  • It does not establish that current cryptography is broken. Cryptographic assumptions must be assessed separately.
  • Formalized research is not the same as universally accepted research. Independent experts still have substantial work to do.

How the community is responding

OpenAI describes an open process with researchers including Russell Impagliazzo, Ramamohan Paturi and Ryan Williams to examine and contextualize the ETH claim. Their involvement in organizing scrutiny should not be represented as an endorsement. A result of this magnitude deserves detailed checks of the algorithm, encoding, asymptotic bounds, Lean statements and implications.

What would confirmation change?

A sound refutation would unsettle conditional lower bounds built on ETH and invite investigation of improved exact algorithms. It would also mark a notable milestone for AI-assisted mathematical research: models participating in the formulation and formalization of genuinely novel claims, with the wider academic community providing an essential quality-control layer.

The immediate lesson is neither that mathematicians have been replaced nor that any model-generated theorem should be trusted. It is that research workflows may evolve toward a combination of AI exploration, reproducible formal artifacts, and rigorous independent interpretation.

Frequently asked questions

Has ETH already been conclusively refuted?

OpenAI and Anthropic say their results imply this. Their papers and proof artifacts are public; wider independent validation remains crucial.

Does this imply P = NP?

No. The claimed algorithms are subexponential, not polynomial.

Are passwords suddenly insecure?

No direct conclusion about everyday cryptographic systems follows from this claim.

Can developers use the new algorithms today?

There is no demonstrated practical speedup for ordinary workloads; Anthropic explicitly calls its bound asymptotic.

Primary references

Editorial status: reporting on public research materials as of October 31, 2026; claims are attributed to their authors rather than presented as a settled scientific consensus.