OpenAI says an AI system disproved the Exponential Time Hypothesis, and the conjecture's original authors are now reviewing the Lean proof

On October 26, OpenAI announced that one of its systems had refuted the Exponential Time Hypothesis (ETH). Since 1999, the ETH has served as the standard assumption that 3-SAT, a basic logic-satisfiability problem, cannot be solved in subexponential time. According to reporting on the announcement, the model produced a natural-language disproof on October 16, and the proof was formalized in the Lean proof assistant on October 17. OpenAI announced two other results at the same time, one in harmonic analysis and one in quantum field theory.

The preprint describes a deterministic algorithm. It counts the exact number of satisfying assignments of fixed-width conjunctive normal form formulas (a standard way of structuring logical statements in satisfiability problems) and uses only polynomial memory. The Lean statement gives a running time of 2 raised to O(n·(log log n)²/√log n). That is far slower than polynomial time, but it beats every 2^(cn) bound that the ETH says 3-SAT requires, as summarized by FourWeekMBA. Russell Impagliazzo and Ramamohan Paturi of the University of California, San Diego, two of the three authors who proposed the ETH, will verify the work together with Ryan Williams of the Massachusetts Institute of Technology (MIT). Independent academic confirmation has not yet been published.

For cryptography, the precise scope matters. Elliptic-curve signatures, hash functions and lattice schemes depend on the hardness of specific problems, not on the ETH, and disproving the ETH does not show that P equals NP. The savings in the exponent grow extremely slowly with problem size. The damage falls instead on fine-grained complexity theory. Many conditional lower bounds in that field begin with "assuming ETH," and those results now need new foundations. OpenAI itself says that turning the result into practical speedups "will require significant further research."

The same machine-checked method is reaching protocol code. On Ethereum Research, a contributor published a Lean verification of EIP-7002, the hand-written 504-byte contract at 0x00000961Ef480Eb55e80D19ad83579A64c007002. Since the Prague upgrade, validator exits and partial withdrawals requested from the execution layer pass through this contract. The proof shows that the per-block system call succeeds and that requests leave the contract in first-in, first-out order.