Two AIs just broke a 27-year-old rule of computer science on the same day. Nobody has checked either proof.

On October 26, OpenAI announced that an internal AI model had proved the Exponential Time Hypothesis is false, a belief that has organised theoretical computer science since 1999, along with a proof of a famous wave-equation conjecture and an existence proof in particle physics. Hours later, Anthropic published its own paper, written by "Claude (Anthropic)," proving the same ETH result by a different method, and said its model found it on October 16 with "no human input." As of today, no human outside either company has confirmed either proof, no outside party has reported building OpenAI's formal proof file, and the three computer scientists OpenAI named as its checkers wrote in an open letter that their involvement "should not be taken as certification of the claim."

Greg Brockman's announcement post on X has been seen 1.3 million times. Bret Taylor, the chairman of OpenAI's board, posted something more interesting than the announcement: "I was and am shocked the exponential time hypothesis is false. I had hoped for a result on P / NP from the models, but had naively presumed they would prove the opposite of this result." The chairman of the company expected its own model to confirm the old belief, not break it. Lance Fortnow, who has spent his career on exactly this question, described it carefully on X as what OpenAI "claims," with a link to the paper and nothing more.

That is the real story, and it has three parts. What was claimed. What it actually means, because almost every news piece got this wrong, including my own first draft. And how it was released, which is where the experts are angry.

What ETH is, in plain words

There is a puzzle called 3-SAT. You have a list of true-or-false switches, and a list of rules, where each rule says "at least one of these three switches must be set a certain way." The question is whether any setting of the switches satisfies every rule. With n switches, the obvious way is to try all 2 to the power n combinations. For 100 switches, that is more combinations than there are atoms in a galaxy.

The Exponential Time Hypothesis, proposed by Russell Impagliazzo and Ramamohan Paturi, says you cannot do much better than that. You can shave the exponent a bit, but it will always be 2 to the power of some fixed fraction of n. For 27 years almost everyone believed it, and hundreds of papers used it as a foundation: "problem X cannot be solved faster than this, unless ETH is false." Anthropic's paper counted "more than 800 papers that prove at least one result of their own only under ETH or under a hypothesis that implies it."

Both AIs now claim an algorithm that runs faster than any fixed-fraction exponent. The speed is 2 to the power of n divided by something that grows with n, slowly. That breaks ETH. OpenAI's paper says it also breaks the stronger cousins, SETH, Gap-ETH and others.

What it does not mean, and this matters

If you read that encryption is now at risk, or that P equals NP, that is false, and both labs say so in their own papers.

P versus NP asks whether these problems can be solved in polynomial time, like n squared or n cubed. The new algorithm is nowhere near that. It is still enormous, just slightly less enormous than before. Ryan Williams of MIT, one of the named checkers, was asked on Bluesky whether it changes his view and said, "If true, it should make every computer scientist put at least a little more weight on the possibility of P=NP." A little more weight. Not a solution.

Encryption is unaffected. RSA depends on factoring large numbers, which is a different kind of problem that already had sub-exponential attacks for decades. AES and hashing can be written as 3-SAT puzzles, but with hundreds of thousands of switches, and at that size the new algorithm is far slower than plain brute force. Anthropic's paper is blunt about it: the bound "does not improve on the 2^n of exhaustive search unless n > 10^10000," a number with ten thousand zeros. In its words, "The result is purely asymptotic and says nothing about solving formulas in practice."

What does change is the map of theoretical computer science. A whole field called fine-grained complexity built its lower bounds on ETH and SETH. Those bounds now have no support. Some survive because they also follow from a different conjecture, Orthogonal Vectors, which neither paper refutes. A Codeforces grandmaster who writes under the name pajenegod put it dramatically: "in half a month, an entire field of theoretical computer science has completely collapsed. This has been a funeral for an entire field of science." Another user pushed back that the concern is "both too overblown or too narrow," since Orthogonal Vectors still stands. Both are right. The field is not dead. Its foundations are being replaced in real time, by machines, faster than people can read.

The two proofs, and the word "verified"

OpenAI's blog says the ETH result "was subsequently verified in Lean." Lean is software that checks mathematical proofs line by line, and when it accepts a proof, the proof is correct, with one giant caveat. Lean checks that the proof proves the statement you typed in. It cannot check that the statement you typed in is the thing you claimed in English.

I had the research team go through the actual files. OpenAI's formal statement is written on a custom machine model its own engineers built, and the bound it proves is slightly weaker than the one in the paper, though still enough to refute ETH. The repository's own README says, "Some of the unformalized results could have issues." The toolchain pulls in around 13 third-party Lean libraries and the README warns the thing is so big you should compile "only small portions at a time." A community group that tracks complexity results looked at it and wrote, "We have not built it ourselves" and "No upstream build, kernel/comparator run or full proof-dependency audit was performed." On Hacker News, one user spotted a line ending in the keyword "sorry," which in Lean means an unfinished proof, and posted it in alarm. That turned out to be a misread, because the file is a statement-only challenge file and the convention is that the real proof lives elsewhere, and the proof module has no "sorry" in it. But it tells you how little outside checking has happened: the loudest public inspection of the proof was a mistake.

Anthropic's version is more auditable in one way, because its statement uses the standard machine model from the main Lean maths library, and its build runs in about eight minutes and passed two independent checkers. But Anthropic's own paper, in Appendix E, says this: "The Lean development was written by AI models and reviewed by other instances of the same models; at the time of writing no person is known to have checked it." And: "Whether the two definitions say what they are meant to say... no machine can check; that is for the reader of the listing to judge."

So we have two proofs of a historic result. One has not been built by anyone outside the company. The other has not been read by any human at all. Both are described as verified.

This is not a theoretical worry. Earlier this month a Cambridge group examined OpenAI's September Navier-Stokes result and found the Lean file proved a weaker inequality than the paper claimed in one lemma. The result may still be right. The point is that "verified in Lean" and "the paper is correct" are different sentences, and OpenAI's blog post uses the first one as if it were the second.

The timing nobody at OpenAI wants to discuss

The sequence goes like this. On October 25, a group of nine senior mathematicians, including Timothy Gowers, Martin Hairer, Edward Witten and Melanie Matchett Wood, operating as the independent Advisory Group on Mathematics and AI, published a statement with the title "Disadvantages of Designating Mathematicians for AI Output Releases." They had been approached by OpenAI to be its advisory board, and chose instead to be independent and unpaid. Their statement says, "we recommend that AI companies do not adopt this practice for future releases," and lists why: "Delayed or unequal access," "Biased selection," which they call "opaque and unaccountable," and "Borrowed reputation," because "designated mathematicians' names end up vouching for the release and shielding the AI company from criticism."

On October 26, OpenAI announced three results, two of them with designated groups.

To be fair to OpenAI, and I will be: for ETH, the Williams group demanded immediate public release and got it. Williams wrote on X, "We've signed no NDAs and will receive no compensation, so we are free to share our ongoing findings with the community," and said OpenAI agreed to fund a conference for everyone. Boaz Barak at Harvard called it "the benefit of human understanding without gatekeeping." The maths result was released to everyone with no chosen group at all. That part follows the advice.

The physics does not. OpenAI's own post says that for the quantum field theory result, "the group has decided to hold off on releasing the AI-produced artifacts and instead work on writing it up themselves." Five physicists led by David Gross now hold a proof nobody else can see. The advisory group responded the same day: "We call on OpenAI to make public without delay the natural-language and Lean outputs behind its announced existence proofs," and added, "By their own account this is now complete, so there is no scientific reason for delaying the release any further." A commenter on Terence Tao's blog summed up the mood: "At least the mathematicians did the right thing today. The physicists, not so much."

Even the ETH letter, which is as graceful as these things get, has a sharp edge. Williams and his colleagues write, "Early access can help researchers check a result before release, but it also creates opportunities unavailable to others. As discoveries come faster, recognition may go mainly to those who publish first or have the most powerful tools." And then: "We do not have access to their internal models. We only got the PDF." Williams added that he "strongly believe[s] that all mathematicians should be given access to (at least) Astra-level models." The people OpenAI chose as its checkers are asking, politely, why they are being handed printouts from a machine they are not allowed to use.

The three weeks before this

Context matters because OpenAI's track record this month is mixed. On October 6, it released 722 manuscripts from around 4,000 problems attempted, each with about three hours of compute. Scott Aaronson called it "surely one of the biggest days in mathematical history" and in the same post wrote, "no human has understood just about any of these proofs yet." Within a day, OpenAI withdrew three papers for a sign error its own audit found. A field-leading mathematician, Hugo Duminil-Copin, said, "They have annihilated my field of research," and, "I am paralysed." Terence Tao called the pile "toxic waste," later softening to "maybe treated waste." Only 10 of the 719 remaining manuscripts came with any explanation of the model's reasoning.

Some results have since held up. Tao treats the Siegel-zero result as solved. Gil Kalai says the Borsuk result is in Lean but "still needs careful checking." Earlier in October, Anthropic's Claude refuted the 3SUM and APSP hypotheses, and two human researchers wrote it up properly. So the machines are producing real mathematics. They are also producing errors, and the only reason we know about the three withdrawn papers is that OpenAI caught them itself.

Then there is the $5 million. OpenAI and Anthropic each gave $5 million to a Simons Foundation program to help mathematicians check AI output. A Hacker News user did the maths: "$5 million might sustain 5-10 PhD students for 5 years." Against hundreds of papers a month, that is a rounding error. And no grantees have been named.

The questions that are actually open

I am not asking these for effect. Each one has no answer right now.

Who is the author? OpenAI says, "We do not seek academic credit." Anthropic's paper lists "Claude (Anthropic)." The two labs say their models found the same theorem on the same day, October 16, by different routes. A Codeforces user joked that "the mathematicians are going to say OpenAI stole all the prompts they sent to Claude." Jokes aside, precedence for one of the biggest results in the field is now contested between two companies, and the people who will spend years checking and explaining it will get, in the open letter's words, "less credit."

Who decides what counts as checked? Right now, the answer is the companies. They choose when to announce, which words to use, who gets early access, and what "verified" means. The advisory group wants labs to disclose "the name of the model, prompts, chains of thought, number of attempts, compute used, and costs." OpenAI discloses the attempt count and ten reasoning summaries out of hundreds of papers.

What happens to students? The open letter's third question is "How can we support students and researchers as methods and research directions change, while preserving the understanding and judgment needed to question results." Tao ran a post this month titled "Mathematics is a subject for the young." If the hard problems a PhD student would spend five years on get solved by a model in three hours, what is the PhD for? Nobody in either company has answered that, and the $5 million does not.

And the question I keep coming back to. An AI company has every incentive to announce a historic result the day its rival might. OpenAI announced on October 26. Anthropic's paper is dated October 26 and was merged on October 27. If either company had waited for a human to finish checking, the other would have claimed the discovery first. So the race itself guarantees that announcements come before verification, every time, from now on.

What I think

I want this to be real. If ETH is false, two machines just did something no human managed in 27 years, and that is worth being amazed by. The fact that two separate systems reached the same theorem by different methods is the strongest evidence yet that it is right.

But a proof is only a proof when people other than the author can check it, and right now the author is a machine, the checkers are either unable to build the files or have not read them, and the company that owns the machine wrote the headline. The nine-person advisory group said, the day before, that this exact way of releasing results is harmful. OpenAI did part of what they asked and ignored the rest, and its own physics group is now sitting on a result in private.

My prediction. Both ETH proofs will hold up, and by the end of 2026 at least one outside team will report a clean independent build of the OpenAI Lean file. The physics result will be released publicly within a month because the pressure will become embarrassing. And within six months, one of the big announced AI results from October will be withdrawn for a gap that the Lean statement did not cover, and that will be the moment the field finally agrees on what "verified" has to mean.

If you only remember one thing: when a company says its AI discovered something, the discovery is not the news. Whether anyone outside the company has confirmed it is the news. Right now, for the biggest claim in computer science in a generation, the answer is still no.

Questions people are asking

Is the Exponential Time Hypothesis proven false? Two AI-generated proofs, from OpenAI and Anthropic, claim so, with Lean formalizations. No independent human verification has been published yet. The named expert group says its involvement is not certification.

What is the difference between ETH and P vs NP? ETH says 3-SAT needs exponential time with a fixed-fraction exponent. P vs NP asks whether it can be done in polynomial time. Refuting ETH leaves P vs NP open; the new algorithm is still far from polynomial.

Is my data less safe now? No. RSA, AES, hash functions and lattice-based post-quantum schemes are unaffected. The new algorithm is only faster than brute force for inputs with more than 10 to the power 10,000 variables.

What did the AGMAI advisory group say? On October 25 it recommended AI companies stop designating hand-picked mathematicians to receive results first. On October 26 it called on OpenAI to release the physics proof immediately.

What about the Kakeya and Yang-Mills claims? OpenAI released the local smoothing paper and Lean files publicly; the Lean proves an epsilon-loss form within the conjectured range. The physics existence proof has not been released; it does not claim the Yang-Mills mass gap, so the Clay Millennium Prize is not at stake.