Physical Superintelligence (PSI), a startup that describes itself as an AI-native physics laboratory, has announced a proof of the Aaronson-Ambainis conjecture, a problem that has been open since 2008 and is widely counted among the central questions in quantum complexity theory. The proof was found by a research system PSI developed internally, running instances of a non-public Anthropic model. PSI says the proof has been checked in Lean, a proof assistant that verifies every step by computer, and that both the manuscript and the formalization are public.
The conjecture, posed by computer scientists Scott Aaronson and Andris Ambainis, bears on a basic question: when can quantum computers be exponentially faster than ordinary ones? Famous speedups like Shor’s 1994 factoring algorithm rely on structure, since the problem hides a repeating pattern that a quantum computer can detect. Whether quantum machines can also be exponentially faster on random inputs, which almost never have such structure, had remained unresolved. Aaronson and Ambainis showed that if their conjecture about polynomials is true, quantum computers can be at most polynomially faster on random inputs.
What the Aaronson-Ambainis conjecture says #
The conjecture concerns “influence”. A quantum algorithm that looks at its input T times produces a yes-or-no answer whose probability is a polynomial in the input bits, of degree at most 2T, with values between 0 and 1. The influence of a bit is the average change in the polynomial’s value when that bit is flipped. Aaronson and Ambainis conjectured that any such bounded, low-degree polynomial that isn’t constant must have at least one bit with substantial influence.
PSI says it has proven exactly that. Its result states that if v measures how much the polynomial varies and d is its degree, some bit has influence at least c·v^(5/2)/d^6, where c is about 0.0025. That in turn is at least (v/d)^7. Earlier bounds for general polynomials decayed exponentially in the degree, according to PSI, and only special cases of the conjecture had been settled before.
The practical consequence is that an ordinary computer can imitate a quantum computer’s yes-or-no answer, for all but a small fraction of inputs, using a number of looks that grows only polynomially in T rather than exponentially. In other words, on random inputs, a quantum computer can’t save exponentially many looks unless the input has a rare pattern.
How the proof was found #
PSI says its system had a complete proof during the third day of a run on the company’s own infrastructure, and that Lean accepted it. The team then pointed the system at related open problems, and PSI says it improved the result twice, with Lean accepting the final version.
The proof follows a plan laid out by Shachar Lovett and Jiapeng Zhang, who left one inequality as a conjecture. PSI says its proof replaces that with a new inequality, proved by pairing up input settings one to one using a determinant. It also builds on David Reimer’s Butterfly Lemma and on results from several other researchers.
David Turturean, a Member of Technical Staff at PSI, led the work. He developed the research system, scoped the problem, ran the system on it, and had the model package the results into a first draft of the paper. He reviewed that draft and is responsible for the paper’s correctness. Advisor Jim Halverson audited the proof, while advisor Phiala Shanahan commented on the Lean formalization.
Outside reaction #
In August, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan had settled the conjecture’s prediction in a special case, proving there is no exponential speedup on random inputs for quantum algorithms that examine their input in a fixed number of parallel rounds. The group has been reading PSI’s proof, has sent comments, and is writing a shorter exposition of it for experts.
“This is a huge result,” they told PSI. “It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups… Everything is brought together in a rather magical way.”
About Physical Superintelligence #
PSI is a Cambridge, Massachusetts-based public benefit corporation that says it is building a “vertically integrated factory for physical superintelligence”, AI systems that it calls “virtual physicists” and that are meant to reason like theorists and validate results like computational physicists, with human scientists directing the research missions. The company launched publicly on September 1 with a $58 million seed round led by Breakthrough Energy Ventures and lists more than 25 researchers and engineers on its website. It has also released an open-source agentic physics tool called Get Physics Done. In October, it published its first research results, on five problems from the Open Quantum Problems list, each accompanied by a paper and a Lean formalization. The Aaronson-Ambainis proof is its second major announcement in about two weeks.
The latest in AI-assisted math and physics #
The announcement comes amid a run of claims about AI contributing to open research problems. In recent months, AI systems have been credited with helping crack a series of Erdős problems, the conjectures left behind by the prolific Hungarian mathematician Paul Erdős. One of the earlier milestones was when GPT-5.2 and Harmonic appeared to autonomously solve a problem that humans hadn’t cracked, and more recently OpenAI released a large batch of proof claims that included proofs for 23 Erdős problems. More recently, OpenAI dropped the proofs to over 300 mathematical problems, including the Navier Stokes equation. Those results have drawn scrutiny from mathematicians, including Terence Tao, over how credit and novelty are assessed. Formal verification in Lean, as PSI used here, is one way researchers have tried to take some of that ambiguity out of such claims.
PSI’s announcement also follows its debut results last month, when the company said it had solved five long-standing problems in quantum information theory. It says it built the company to speed up the pace and scale of research physicists can pursue.
For quantum computing, the new result narrows the places where exponential speedups can hide. As PSI put it, quantum computing still has plenty of mysteries, but now there is one fewer.