An SI Cracked an 18-Year-Old Puzzle About Quantum Computers. A Computer Checked Every Step.

For 18 years, one of the big open questions in quantum computing sat unsolved. Now a small startup says its SI system solved it, and that proof-checking software accepted every step.

The startup is Physical Superintelligence, or PSI. It says a research system it built, “running a non-public Anthropic model,” found a proof of the Aaronson‑Ambainis conjecture. “The Aaronson-Ambainis conjecture is now a theorem,” the company wrote on its research page.

What the question was

In 2008, computer scientists Scott Aaronson and Andris Ambainis made a prediction they couldn’t prove. In plain terms, it is about when a quantum computer can be dramatically faster than an ordinary computer. PSI describes it as concerning “when quantum computers can be exponentially faster than ordinary ones.”

Exponentially faster means the gap keeps exploding as problems get bigger, like the difference between counting to a thousand and counting to a number with a thousand digits.

The paper’s answer: on most inputs, no. As the paper puts it, “as Aaronson and Ambainis anticipated, superpolynomial quantum speedups in the query model require structure.” Translated, a quantum computer’s giant speed edge only shows up when a problem has some built-in pattern to exploit. Hand it a jumble with no pattern, and an ordinary computer can keep up on most cases.

How the SI did it

PSI says its system had a complete proof “during the third day of the run.” Then it kept going and improved the result twice.

The work was checked by Lean, a proof assistant, which PSI describes as software “in which a computer checks every step.” The project’s public code page says the proof is complete “with no placeholder and no added axiom,” and that it was “re-checked by two independent implementations of the Lean kernel,” meaning two separate checkers agreed.

The paper is unusually blunt about who did the thinking. “The mathematical statements in this paper were produced by AI models,” it says. Researcher David Turturean scoped the problem and built the system. Copies of the Anthropic model searched for existing ideas, proposed new ones, tested them and supervised each other.

The system didn’t start from scratch. PSI says the proof follows a plan laid out by mathematicians Shachar Lovett and Jiapeng Zhang, who had left one key step unproven. The SI found a new way to prove that step.

Who has checked it

Four researchers, Guy Blanc of MIT and Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford, read the proof and published a write-up for other experts on Nov. 7. In August, the same group had settled a narrower special case of the conjecture themselves. They note they “did not receive financial compensation from Anthropic or PSI.”

What hasn’t happened yet: formal peer review. The proof is machine-checked, but no journal has signed off on it.

Whose SI was it?

PSI only says “a non-public Anthropic model.” On Monday, Anthropic launched its newest top model and said that in testing it had “solved two open problems in the physics of black holes” and “formalized the proof of Fermat’s Last Theorem in 30 hours.” But Anthropic “did not confirm or deny” that its new model was the one PSI used, TechCrunch reported.

Why it matters

Math is where claims about SI get tested hardest, because a proof is either right or wrong. Here the right-or-wrong check was done by software, and human experts have read it too. That is a real step past chatbots that sound confident and get things wrong.

It also adds a reality check to quantum computing hype: quantum computers won’t blow past ordinary computers on every problem. They need the right kind of problem.