Physical Superintelligence (PSI) announced on November 6 that a proof of the Aaronson-Ambainis conjecture, a problem in quantum complexity theory open since 2008, has been found by an internal research system running a non-public Anthropic model. The company's announcement says the system had a complete proof during the third day of the run, and that Lean, a proof assistant that checks every step by computer, accepted it.
The conjecture, stated by computer scientists Scott Aaronson and Andris Ambainis in their 2008 paper on the need for structure in quantum speedups, bears on a basic question: when can quantum computers be exponentially faster than classical machines? Famous quantum speedups, like Shor's factoring algorithm, rely on mathematical structure hidden in the problem. Whether quantum computers can also be exponentially faster on random inputs, which almost never have such patterns, had remained an open question.
Aaronson and Ambainis proposed a conjecture about polynomials and showed that if it held true, quantum computers could be at most polynomially faster on random inputs. The conjecture concerns "influence," the idea that in any bounded, low-degree polynomial that isn't constant, at least one input bit must substantially affect the output. Researchers have counted the problem among the central open questions in quantum complexity theory.
How PSI Says It Was Found
David Turturean, a Member of Technical Staff at PSI who studied physics and AI at MIT, led the work. According to PSI's announcement, Turturean developed the research system, scoped the problem, and ran the system on it. The paper says he then prompted an instance of a non-public Anthropic model to package the results into a first draft of the paper. Turturean reviewed the draft and is responsible for its correctness.
The proof builds on earlier work by Shachar Lovett and Jiapeng Zhang, who had left one inequality unresolved 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. The company says the system improved the result twice over the course of the run, and Lean accepted the final version.
Jim Halverson, an advisor to PSI, audited the proof. Phiala Shanahan, an MIT theoretical physicist and another PSI advisor, commented on the Lean formalization. Both the manuscript and a Lean 4 formalization are publicly available on GitHub.
Outside Reaction, With a Caveat
In August, a team at Stanford had settled the conjecture's prediction in a special case. Guy Blanc, Jordan Docter, Carmen Strassle, and Li-Yang Tan proved there is no exponential speedup on random inputs for quantum algorithms that examine their input in a fixed number of parallel rounds. According to PSI's announcement, that group has since been reading the new proof and sent comments.
"This is a huge result," the Stanford researchers wrote to PSI, as quoted in the company's announcement. "It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups."
What PSI is claiming would be significant. It would also be an early demonstration of AI systems contributing to formal mathematics in a field where conjecture proofs are notoriously difficult to verify without machine assistance. But the result has not yet been published in a peer-reviewed journal, and as of publication, no public assessment by Scott Aaronson or Andris Ambainis has surfaced. A Lean proof, while mechanically checkable, is not the same as the broader scrutiny of expert review.
The Company
PSI is a Cambridge, Massachusetts-based public benefit corporation that launched publicly in September with a $58 million seed round led by Breakthrough Energy Ventures. The company describes itself as an AI-native physics laboratory staffed by "virtual physicists" intended to reason like theorists and validate results like computational physicists. Its founders include Matt Pines, Alex Klokus, and Alexander Wissner-Gross.
PSI says it solved five long-standing problems in quantum information theory last month. The Aaronson-Ambainis proof is its second major announcement in approximately two weeks.
Whether the proof holds under sustained outside scrutiny is the open question. Lean has accepted it. The field has not yet weighed in.
