Anthropic: Claude also disproves a conjecture about computing time that is almost thirty years old

Anthropic has put a mathematical paper online in which, according to the company, an internal Claude research model independently disproves a well-known conjecture from computer science: the Exponential Time Hypothesis (ETH). That conjecture, formulated in 1999 by Russell Impagliazzo, Ramamohan Paturi and Francis Zane, is one of the quiet assumptions that a lot of other work in computer science rests on.

The news came shortly after OpenAI reported three major breakthroughs by its own AI models, in mathematics, computer science and physics. One of those three is exactly this result: according to OpenAI as well, the ETH is false. So two AI companies say they have independently solved the same old problem.

What is it about?

The conjecture is about a puzzle called 3-SAT. You get a long list of yes/no questions and a pile of conditions, each of which concerns at most three of those questions. The task: find an answer to every question so that all the conditions are met at the same time. Anyone who goes through all the possibilities has twice as much work with every extra question. With 100 questions that is already impossible.

Clever methods do it faster. With the best one so far, each extra question added roughly a third more work, instead of doubling it. But even then the work grows by the same fixed percentage with every extra question, and for large puzzles that still gets out of hand. The ETH says this can never be fundamentally better: there will always be such a fixed percentage left. According to Anthropic, Claude shows that it can be done. With the new method, the extra work per question gets smaller and smaller as the puzzle grows, and eventually becomes smaller than any fixed percentage.

What Anthropic claims

The paper is called 'A 2^o(n) Time Algorithm for 3-SAT' and is credited to 'Claude, Anthropic'. The computer scientist Jelani Nelson posted it on 27 October on behalf of Anthropic on the mathematics site Hexagon. The method it describes solves 3-SAT and can also count how many solutions there are. According to the paper and Anthropic researcher Levent Alpoge, the model found the core of the method on 16 October, without help from people. It used 14 million tokens (pieces of text the model writes) to do so. Researchers then worked with Claude on the write-up.

The proof has also been written out in Lean 4, a program that lets a computer check a mathematical proof step by step. Anthropic put that version on GitHub. Two independently built checking programs accept the proof. Earlier this year Claude already produced a computer-checked version of the proof of Fermat's Last Theorem.

Anthropic is open about what still has to happen. According to the paper, the Lean version was written by AI models and checked by other instances of the same models. No person is yet known to have checked that version themselves. People also need to verify that the theorem in Lean says exactly the same as in the paper; that is why the main theorems in Lean form are in an appendix to the paper, together with what the computer did and did not check.

Great for theory, not for practice

The result is mainly theoretical. According to the paper, it says nothing about solving such puzzles in practice. The new method beats simply going through everything only once the number of questions reaches a 1 followed by 108 zeros, at the earliest. For an ordinary puzzle, with about five conditions per question, that threshold is even a 1 followed by 10,000 zeros. For comparison: the observable universe is estimated to contain about a 1 followed by 80 zeros of atoms. The result also does not solve the famous P versus NP question.

Still, it is big news for science, if it holds. A stricter version of the conjecture (SETH) then falls as well. According to a literature review by Claude in the paper, more than 800 earlier scientific papers rely on the ETH or an assumption that follows from it. If the proof holds up, researchers will have to find a new foundation for those papers. The underlying problems do not become any easier in practice.

The same result twice

The results of Anthropic and OpenAI are very similar. According to OpenAI, its model also found a method on 16 October that counts how many solutions such a puzzle has, and that proof is in Lean too. Anthropic refers to OpenAI's result in its own paper.

The difference lies mainly in the checking. At OpenAI, a group led by Impagliazzo and Paturi, two of the people who came up with the ETH, and Ryan Williams (MIT) is examining the proof. They stress that their involvement is not yet an endorsement. Anthropic put its paper and the Lean proof publicly online. Both claims therefore come from the companies themselves; the verdict of mathematicians is still to come.

What does this mean for the road to the singularity?

If both claims are correct, two AI models independently reached a breakthrough on the same day on a question that people had been stuck on for almost thirty years. That is a step from AI as a tool to AI that finds new mathematics itself.

At the same time, it becomes clear what matters now: checking. An AI can find a proof in days, but only a few people can judge such a proof. You can see that at OpenAI too, which in early October already put 372 results on open questions in mathematics and computer science online, almost all from a single task given to an AI model. There too, mathematicians are still busy checking. Proofs that a computer has already checked, as in Lean here, make that work a lot lighter. That way, new knowledge from AI can soon reach science faster and more reliably.

What is the technological singularity? Read the explanation →