Forget P vs NP. The most surprising thing in OpenAI's ETH paper is a corollary on page 3. The headline result is an algorithm that decides, and even counts, k-SAT solutions in 2^O(n log log n / √log n) time with polynomial space. That's subexponential, so ETH falls and SETH goes with it. But it isn't a polynomial-time guarantee, and P vs NP remains open. Corollary 1.4 is what stopped me. There's a language in E^NP whose circuits need more than c·n·√log n gates for infinitely many input lengths. Any fan-in-2 gates, unlimited fan-out, no restrictions. Here's why that's strange. Five decades of work on unrestricted circuits moved the best lower bound from 2n gates (Schnorr 1974) to 3n (Blum 1984) to 3.1n (Li and Yang 2022). Every one of those is a constant times n. Even when you let yourself pick anything in E^NP, which is a huge class to hunt in, nobody had proven that linear size isn't enough. This isn't a better constant. The gates per input grow without limit. So how does a SAT algorithm prove a circuit lower bound? That's Ryan Williams's idea from 2010. Take a problem that provably needs about 2^n nondeterministic time. If its proofs could be written down by small circuits, you could guess the small circuit and run a fast SAT solver to confirm the proof it describes has no broken clause. That solves the problem in about 2^(n/2) time, which the time hierarchy forbids. Fast SAT and small circuits can't both exist. If fast SAT is real, the circuits can't be small. Williams is now one of the three people leading the open examination of this proof. The other two are Russell Impagliazzo and Ramamohan Paturi, two of the three people who proposed ETH in the first place. What's actually been checked • Lean verifies one fixed machine that counts k-CNF solutions in 2^O(n(log log n)²/√log n) time with polynomial space • That bound is already subexponential, so if the formal statement means what it says, the Lean-checked algorithm plus Williams's published theorem is enough for "E^NP has no linear-size circuits" • The exact n√log n rate needs the paper's sharper 2^O(n/√log n) bound for sparse formulas and a local reduction, and neither is in Lean • No outside expert has signed off on any of it yet The algorithm will get the headlines. The lower bound is the part that would change what we thought could be proven about circuits. Paper github.com/openai/math/blob/… What Lean actually checked github.com/openai/math/blob/…