An AI system built by a US research lab has, the lab says, solved a quantum computing maths problem that had stood since 2008. Physical Superintelligence (PSI) said on 6 November, US time, that its internal research system, running an unreleased Anthropic model, found a proof of the Aaronson–Ambainis conjecture.
Lean, software that checks every logical step of a formal proof, accepted the result. PSI has published the paper and the Lean files on GitHub. The proof has not been peer reviewed, and the two researchers who posed the conjecture have not commented publicly yet.
What the conjecture is about
Quantum computers can be dramatically faster than ordinary computers on some problems, such as factoring large numbers with Shor’s algorithm. Those speed-ups rely on hidden structure, such as a repeating pattern in the input.
Scott Aaronson and Andris Ambainis asked whether a quantum computer could still be exponentially faster when the input is random and has no such pattern. They turned the question into a statement about polynomials. If that statement was true, they showed, quantum computers would be at most polynomially faster on random inputs.
PSI’s proof says it is true. If you count how many times a computer must read its input, an ordinary computer can imitate a quantum one on almost all random inputs without needing exponentially more reads.
That’s a ceiling on one kind of speed-up. It is not a verdict on quantum computing as a whole. It counts input reads rather than total running time, and structured problems such as factoring keep their known quantum advantage. One widely viewed reply to PSI’s announcement asked, “So are quantum computers worthless now or?” It doesn’t.
How the AI found it
PSI says the system had a complete proof on the third day of a run on the company’s own servers. It then worked on related problems and improved the result twice. Lean signed off on the final version too.
David Turturean, a member of PSI’s technical staff, built the system and chose the problem. PSI says he had the model draft the paper, reviewed it and takes responsibility for its correctness. Adviser Jim Halverson audited the proof. The repository states plainly: “The proof, the paper and the formalization were produced by AI models”.
On X, Turturean said “it took our system upwards of 3 days”. The proof follows a plan by mathematicians Shachar Lovett and Jiapeng Zhang, replacing an inequality they had left unproven with a new one.
What has been checked, and what hasn’t
According to the GitHub repository, the main Lean theorems are proved “with no placeholder and no added axiom”. Two independent implementations of Lean’s core checker confirmed them. The conjecture’s statement sits in a single file that relies only on Mathlib, Lean’s standard maths library, so readers can compare it with the original.
Lean confirms that the formal proof establishes the formal statement. It can’t confirm that the statement matches what Aaronson and Ambainis meant; experts still need to check that. The written paper is not machine-checked either.
So far, outside praise has come through PSI. Stanford’s Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who proved a special case in August, are reading the proof and writing a shorter explanation for experts. PSI quotes them: “This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups.”
An earlier claimed proof did not survive. In 2019 Aaronson announced a claimed proof by Nathan Keller and Ohad Klein on his blog. He later added that they had retracted it “because of what currently looks like a fatal flaw in Lemma 5.3”. A full Lean check is meant to catch that kind of gap.
Lech Mazur, who keeps a ranked list of open maths problems, put the conjecture at “the #388 spot overall on my list of the top 500 open problems in math”.
Why it matters
It joins a string of recent claims of AI systems settling long-standing maths problems. Here, the full Lean formalisation is public, so anyone can rerun the check. The model is not: Anthropic hasn’t named or released it, and PSI’s system is internal, so nobody outside can repeat the run itself.
We found this story through PSI’s announcement thread on X.
Sources
- PSI announcement
- Paper (PDF, GitHub)
- Lean formalisation repository
- Aaronson and Ambainis, The Need for Structure in Quantum Speedups (arXiv)
- Shtetl-Optimized, 2019 post and retraction update
- PSI on X
- David Turturean on X
- Lech Mazur on X
Discover more from Sulat — AI & Tech News
Subscribe to get the latest posts sent to your email.
