Daily Issue #4 · 7 min read

Two AI labs say they refuted a core computing conjecture. The checking is the real story.

OpenAI and Anthropic both say their models refuted the Exponential Time Hypothesis. The result may hold, but the more useful lesson is about what a machine check actually proves.

The short answer

Did AI just disprove the Exponential Time Hypothesis? OpenAI and Anthropic both say their internal models did. On October 26, OpenAI announced that its system proved the hypothesis false, with a proof checked in the Lean proof assistant. Within hours, Anthropic published its own paper and Lean proof for a similar result, found by an internal Claude model. Neither claim has been peer reviewed yet, and the experts organizing a review of OpenAI's claim say their involvement is not a certification. Anthropic says its result says nothing about solving formulas in practice, and OpenAI says practical gains will need significant further research. I think the most useful part for anyone building with AI is the question both releases raise: when a model says its work is verified, verified against what?

What happened

The Exponential Time Hypothesis, or ETH, is a conjecture proposed by Russell Impagliazzo and Ramamohan Paturi. In plain words, it says that 3SAT, a classic logic puzzle about whether a formula can be made true, cannot be solved much faster than by trying an exponential number of possibilities. OpenAI says it has been used in hundreds of papers to show that problems in graph theory, computational biology, databases and other fields are hard.

Here is the sequence, according to the two companies:

• OpenAI says its model found a natural language disproof on October 16 and that the result was formalized in Lean on October 17.
• Anthropic's paper says the core algorithm "was found on October 16 by an internal Claude research model with 14M output tokens and no human input." Anthropic researchers then worked with Claude on the write up.
• OpenAI announced its result on October 26, alongside two other claimed results in mathematics and physics.
• Anthropic posted its paper and Lean proof hours later. The paper notes that, "independently and concurrently, an internal model at OpenAI claims to have proven a similar result."

Both labs say their models found the key idea on the same day. That is striking whichever way the review goes.

What the claims say, and what they do not

Both labs describe a deterministic algorithm that does more than answer yes or no. It counts the satisfying assignments of a formula, in time that grows more slowly than any fixed exponential. If that holds, ETH is false.

The Anthropic paper is unusually direct about the limits:

• It says the result "does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems."
• It says that for 3SAT formulas with five clauses per variable, the proven bound does not beat brute force search unless the formula has more than 10^10,000 variables. The paper notes that brute force is already impractical at 100 variables.
• It also refutes a stronger version called SETH. It does not refute the Orthogonal Vectors hypothesis, which many other hardness results rely on.
• In a literature search run by Claude, the authors found more than 800 papers that prove at least one result only under ETH or a hypothesis that implies it.

OpenAI's post makes a similar point in softer words: turning the advance into practical improvements "will require significant further research."

So if you run SAT solvers, schedulers or optimization code today, nothing changes this week. What changes, if the proofs hold, is the theory. Hundreds of results that assumed ETH would need another look.

What "verified in Lean" covers

Lean is a programming language where a computer checks every step of a proof. That sounds final. Anthropic itself explains why it is not.

Its README puts it this way: "Lean checks the proofs, but no machine checks that this file says what the paper says." The paper goes further. Whether its two Lean definitions say what they are meant to say "no machine can check," and 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."

OpenAI's own documentation for its Lean proof shows a similar gap from another angle. The Lean theorem proves a bound with a weaker exponent than the one in its manuscript. The sharper bound in the paper is not the one the machine checked.

None of this means the proofs are wrong. It means the machine check answers a narrower question than the headline. Lean confirms that a proof proves a formal statement. A person still has to confirm that the formal statement is the claim everyone cares about.

How the review is set up

OpenAI calls these manuscripts "a form of raw research data" and asked outside experts to act as shepherds. For the ETH result, the group is led by Impagliazzo and Paturi of UC San Diego, who OpenAI says proposed the hypothesis together with Francis Zane, and Ryan Williams of MIT.

OpenAI lists four principles for these collaborations: no nondisclosure agreements, no academic credit claimed by OpenAI, recognition for the people who write the explanations, and voluntary, unpaid participation. At the group's request, OpenAI says it made the raw data public and committed to fund a conference on the result.

In their open letter, the three researchers wrote that "our involvement should not be taken as certification of the claim." I like that sentence. It is the right posture for everyone reading these announcements, including me.

Why I think builders should care

Most readers of this newsletter will never touch complexity theory. I still think this is the most important AI story of the week. Here is why.

Long, unattended runs are producing real candidates

Anthropic describes a model that spent 14 million output tokens on one problem with no human input and came back with a candidate result that the company was willing to publish with a full Lean proof. Whether or not this one survives review, models are being trusted with long, open ended work and returning things worth checking. That changes what is worth asking a model to attempt.

The bottleneck moves to checking

When generation gets cheap, the expensive part is knowing whether the output is right. OpenAI recruited senior experts, agreed to fund a conference and published its raw data just to start that process. Most companies using AI have nothing like this. A support team that lets a model draft refund decisions, or an ecommerce search team that lets an agent rewrite ranking code, faces the same question at a smaller scale: who checks the output, and against what?

Passing a check is not the same as being right

The Lean point maps directly onto everyday AI work. A coding agent can write code and tests, and the tests can pass. That proves the code matches the tests. It does not prove the tests describe what you wanted. If the same model wrote both, you have the situation Anthropic describes: AI output reviewed by other instances of the same models. The fix is the same in both cases. A human, or an independent process, has to own the specification, meaning the short statement of what correct looks like.

What I would not read into it

I would not read this as proof that P equals NP, or as a sign that hard problems just became easy in practice. Anthropic's paper says neither follows from its result.

I would also not treat either claim as settled. Two independent results pointing the same way is encouraging, and the Lean proofs make review much easier. But the review has just started, and the people leading it have said plainly that they are not vouching for it yet.

My takeaway

AI models are now producing results that even the companies releasing them cannot fully vouch for without outside experts. The labs handled this one fairly openly: public proofs, clear limits, independent reviewers. The lesson I take for everyday AI work is to ask, every time a model says "verified" or "tests pass," what exactly was checked and who wrote the thing it was checked against.

Quick notes

• Google DeepMind announces Genie 4: Google DeepMind announced Genie 4 on October 27, a world model that generates interactive scenes with native audio such as music, ambient sound and dialogue. Google says users can steer a scene with natural language while it runs. It is rolling out first to trusted testers, with Google AI Ultra subscribers and early access partners on the Gemini API and AI Studio to follow.
• OpenAI reportedly plans to buy Google's AI chips: OpenAI plans to buy Google's TPU chips, The Information reported on October 27, according to Reuters. Financial terms were not disclosed and OpenAI declined to comment to Reuters. OpenAI is one of the largest buyers of Nvidia GPUs.

Common questions

What is the Exponential Time Hypothesis?

The Exponential Time Hypothesis, or ETH, is a conjecture proposed by Russell Impagliazzo and Ramamohan Paturi. It says that 3SAT, the problem of deciding whether a Boolean formula with at most three literals per clause can be satisfied, cannot be solved in time much faster than exponential in the number of variables. Many hardness results in computer science assume it is true.

Did OpenAI and Anthropic really disprove ETH?

Both companies say their internal models found a proof that ETH is false, and both published Lean formalizations. Neither result has been peer reviewed. A group led by Impagliazzo, Paturi and Ryan Williams is organizing an independent examination of the OpenAI claim and says its involvement is not a certification.

Does this make SAT solvers or optimization software faster?

No. Anthropic's paper says the result says nothing about solving formulas in practice, because its bound only beats brute force search for formulas with an astronomically large number of variables. OpenAI says practical improvements will require significant further research.

Does refuting ETH solve P vs NP?

No. Anthropic's paper says the result does not bear on the P vs NP question directly. ETH is a stronger assumption than P not equal to NP, so refuting it leaves P vs NP open.

What does verified in Lean mean?

Lean is a proof assistant in which a computer checks every step of a proof against a formal statement. It confirms the proof is valid for that statement. It does not confirm that the formal statement matches the claim written in the paper, which still needs human review.