What happened, and what I did
The claim. The Exponential Time Hypothesis, proposed by Impagliazzo and Paturi in 1999, says that some problems, like 3-SAT, cannot be solved much faster than trying every possibility: the time has to grow exponentially. Hundreds of results in computer science are built on it. In October 2026, OpenAI and Anthropic each published an AI-written proof that it is false, each checked by Lean, a program that verifies mathematical proofs line by line.
The catch. A proof checker only checks the statement it is given. Each lab stated its result about a computer of its own design, reading the input in its own format. Whether that is the computer of the textbooks, the multitape Turing machine every course teaches, was argued in a paragraph, not proved.
Who claims, who decides. Two repositories, one author, two roles. claimbox is the claimant: its Claude agents wrote every bridge and every port below, and it proposes them with their planted wrong variants. cert-machine is the judge: it pins the statements, decides each proposal from the bytes, refuses what fails, and claims nothing of its own. The separation is of roles, not of people, and the page says so wherever it matters.
What I did. With AI agents in claimbox, I wrote a Lean proof that Anthropic’s statement implies the hypothesis fails on a standard multitape Turing machine reading ordinary binary input, for every formula. Then I moved Anthropic’s own proof into the same Lean, 762 of its 809 files unchanged, so every step from their proof to the textbook machine is checked in one place. Six proof checkers accepted it, four of them written apart from Lean’s own kernel.
Then OpenAI’s side. OpenAI’s proof ends at a statement of its own; Daniel Hawkley, a third party, had already proved in Lean that it implies Anthropic’s. I moved OpenAI’s proof and his two links into the same Lean as well, 3,190 of 3,210 files unchanged, so OpenAI’s statement reaches the textbook machine through the same step. Lean’s judge accepted it, and so did OpenAI’s own challenge file, unchanged, against the ported proof. On this side the judge’s own list of checkers is shorter, for a reason written out below. Every one of 12 deliberately wrong versions I planted across the two chains was refused.
What it means. When an AI lab says “machine-checked”, the question is always what was checked. For both claims, the distance between the headline and the checked statement is now one definition wide: that the textbook’s ETH is this formal one. That last step is a reading of a definition, and always will be. The claims, the algorithms and the papers remain the labs’; this page checks the links, not the mathematics behind them.
The limits come next, then the picture, then every step with its record. The full argument is in the technical note (PDF).