On the morning of October 26, 2026, OpenAI published a blog post announcing that one of its internal frontier models had generated a proof refuting the Exponential Time Hypothesis. ETH is not a household name, but it is one of the load-bearing walls of theoretical computer science—a 27-year-old assumption that has quietly shaped how researchers reason about the absolute limits of computation. Within hours, Anthropic published its own independent refutation, generated by an internal model, and the two labs were suddenly locked in a public race to have overturned one of the field's most cited conjectures. By the following afternoon, both proofs had been formalized in Lean, a proof-verification language that checks mathematical arguments line by line the way a compiler checks code. The Lean code compiled. There were no errors. There were no hallucinated steps, no smuggled assumptions, no subtle logical slips. By every machine-checkable standard, the math was correct.

And yet, for anyone actually trying to solve a real problem on a real computer, the announcement might as well have been a press release about a perpetual motion machine. The algorithm the AI discovered does technically beat the exponential barrier. It does so by such an agonizingly thin margin that the curve is visually indistinguishable from the old one at every scale a human being will ever compute. For five variables, it is slower than brute force because of setup overhead. For a thousand variables, it is still a number of steps with roughly three hundred digits, which is to say, still longer than the age of the universe. The "crossover point"—the problem size at which the new algorithm finally becomes faster than the old one—is so astronomically large that it could never be reached before the heat death of the universe.

This is the strange new genre of scientific announcement that AI labs have perfected: a result that is simultaneously a historic breakthrough in pure mathematics and a complete non-event for every practical application of computing. The proof is real. The verification is real. The excitement among mathematicians is real. And the algorithm, for all intents and purposes, does nothing. Welcome to the era of the "slop drop"—the practice of releasing dense, un-peer-reviewed, machine-generated mathematics into the public sphere and letting the academic community sort out what, if anything, it means.

What the Exponential Time Hypothesis Actually Says

To understand why anyone cares about a proof that changes nothing, you have to understand what ETH claims. The hypothesis was proposed in 1999 by Russell Impagliazzo and Ramamohan Paturi, two computer scientists at the University of California, San Diego. It concerns 3-SAT, the canonical "hard" problem in computational complexity—a logic puzzle in which you are given a long list of constraints, each involving three Boolean variables, and asked whether there is any assignment of true and false to the variables that satisfies every constraint simultaneously.

A simple example: imagine a scheduling problem where you have to assign shifts to a thousand employees, subject to thousands of overlapping rules—no one works two shifts back to back, everyone gets two days off, the night shift must be covered, and so on. Each rule is a constraint. Each employee-shift pair is a variable. The question "is there a valid schedule?" is a 3-SAT instance. The same structure underlies circuit verification, protein folding, cryptography, and a hundred other problems that matter in the real world.

ETH claims that 3-SAT cannot be solved in subexponential time—that there is no algorithm whose runtime grows meaningfully slower than 2ⁿ, where n is the number of variables. This is a strong claim. It says that the problem is not just hard in practice but hard in principle: that no clever mathematical trick, no structural insight, no future breakthrough will ever produce an algorithm whose runtime curves downward. ETH has never been proven, but it has survived 27 years of attack, and hundreds of peer-reviewed papers in cryptography, network design, and computational biology have been built on the assumption that it is true.

The AI's proof does not demolish that wall. It files a microscopic notch into it. The new algorithm solves 3-SAT in time roughly proportional to 2ⁿ divided by the square root of the logarithm of n. That denominator is the entire trick. It is also, from a practical standpoint, the entire joke. Because the denominator grows so extraordinarily slowly—the logarithm of a logarithm is one of the slowest-growing functions in mathematics—the reduction in runtime is negligible for any input a human could ever construct. But in the strict, asymptotic language of complexity theory, any function that grows slower than 2^cn for some constant c is classified as subexponential. The AI found a function that does, technically, meet that definition. Therefore ETH is false.

• Traditional exponential: 2ⁿ steps. For n = 1,000, that is roughly 1.07 × 10³⁰¹ steps—trillions of times longer than the age of the universe, even on the fastest supercomputer ever built.
• The AI's "breakthrough": 2ⁿ / √(log₂ n) steps. For n = 1,000, the denominator is about 3.16. The runtime is still roughly 3.39 × 10³⁰⁰ steps—still trillions of times longer than the age of the universe.
• The crossover point: To get the denominator up to just 3.0, you would need n = 2⁵¹² variables—a number vastly exceeding the total number of atoms in the observable universe.
• For small problems: At n = 5, a brain-dead brute-force checker finishes in a microsecond. The AI's polynomial machinery drowns in setup overhead and is measurably slower.

This is the textbook definition of a galactic algorithm: a design that is mathematically superior but only becomes faster on inputs larger than the universe. The term was coined by researchers to describe algorithms that are theoretically elegant and practically useless. The AI's 3-SAT solver is a perfect specimen. It does not build a faster highway. It proves that at the edge of the infinite universe, the road curves by a fraction of a millimeter.

The Lean Proof: What a Machine Can Check and What It Can't

The most striking thing about the announcement is not the algorithm itself but the verification method. Both OpenAI and Anthropic translated their models' step-by-step reasoning into Lean, a proof assistant developed by Leonardo de Moura at Microsoft Research and now maintained by a global community of mathematicians. Lean is not a chatbot that agrees with you. It is a programming language in which mathematical statements are encoded as types and proofs as programs, and the compiler checks every step against the axioms. If the Lean code compiles, the proof is correct—not "probably correct" or "correct as far as we can tell," but correct in the same sense that 2 + 2 = 4 is correct.

This is a genuinely new kind of scientific evidence. Traditional mathematical proofs are written in natural language and checked by human referees who may miss subtle errors. Lean proofs are checked by a machine that misses nothing. The tradeoff is that Lean proofs are enormously difficult to write—encoding a serious mathematical argument in Lean can take months of expert labor—and the process of formalization can itself introduce errors if the human doing the encoding misunderstands the original argument. But when the formalization is done by the same AI that generated the proof, and the Lean code compiles, the result is a level of confidence that no traditional peer review can match.

And yet, as the computer scientist Ryan Williams pointed out in a widely shared thread on X, a Lean proof only tells you that the formal statement is true. It does not tell you that the formal statement means what you think it means. This is the "vacuous truth" loophole: the AI may have subtly redefined the problem so that the proof is technically correct but addresses a different question than the one humans care about. The Lean compiler cannot catch this. Only human experts can.

This is why an emergency external working group has been assembled to audit the findings. The group includes Impagliazzo and Paturi themselves—the original authors of ETH—alongside Williams and several other senior complexity theorists. They are checking two things. First, whether the formal statement in Lean actually captures the original claim of ETH or whether it has been weakened in some subtle way. Second, whether the algorithm has any practical value at all. The group has made all raw data and Lean code public on GitHub, and the community is stress-testing the claim in real time.

What Happens If the Proof Holds Up

If the proof withstands human scrutiny, the consequences for theoretical computer science will be significant but narrow. ETH is used as a benchmark in hundreds of papers to prove that certain problems are "too hard" to solve efficiently. If ETH is false, those proofs do not automatically collapse—they were conditional on ETH, and the condition has changed—but the field's understanding of what is and is not possible will shift. The search for faster algorithms, long abandoned because ETH said it was impossible, will reopen. Researchers will try to optimize the AI's algorithm, to shrink the denominator, to find a structural insight that makes the speedup practical rather than galactic.

But the more important consequence may be procedural. The ETH announcement is a test case for a new kind of science: AI-generated results, machine-verified proofs, and human interpretation. If the proof holds up, it will establish a template for how AI labs can contribute to foundational research. If it does not—if the Lean code turns out to encode a subtly different problem than the one humans care about—it will establish a different template: a cautionary tale about the limits of machine verification and the importance of human judgment.

For now, the practical use of this discovery is purely theoretical and practically useless. It changes what mathematicians believe about the shape of computation. It does not change what engineers can build with it. The Exponential Time Hypothesis is broken on a chalkboard. The car still won't start. And the people who have to clean up the slop drop are still waiting to find out whether the AI actually proved something—or just found a very expensive way to say nothing at all.