AI Physics Startup PSI Says a Non-Public Anthropic Model Cracked an 18-Year-Old Quantum Conjecture in Three Days

A research system built by AI physics startup Physical Superintelligence (PSI) produced a complete proof of the Aaronson-Ambainis conjecture, a quantum computing problem that had stood open since 2008, the company said in a research post published Thursday. The proof emerged during the third day of an autonomous run on PSI's own infrastructure, which used instances of a non-public Anthropic model, and every logical step was checked and accepted by the kernel of the Lean proof assistant.

The conjecture, posed by Scott Aaronson and Andris Ambainis, concerns when quantum computers can be exponentially faster than classical ones. Celebrated quantum speedups like Shor's factoring algorithm rely on structure: the input hides a repeating pattern the quantum machine can exploit. Aaronson and Ambainis asked whether a quantum algorithm could still gain an exponential advantage on random inputs, which almost never contain such structure, and reduced the question to a statement about polynomials that has resisted proof for eighteen years.

PSI's result answers it: no. For yes-or-no questions on most randomly chosen inputs, a classical algorithm can estimate the quantum computer's probability of answering yes using a number of input reads that grows only as a fixed power of the quantum algorithm's read count, never exponentially fewer. The theorem limits data reads rather than total computing time, so it does not rule out practical quantum advantages, but it tells algorithm designers where to look: at problems whose structure offers a genuine edge.

The proof follows a 2023 plan laid out by Shachar Lovett and Jiapeng Zhang, replacing one conjectured inequality with a new one: in any non-constant bounded polynomial of degree d and variance v, some input bit must have influence of at least a fixed power of v/d, with the constant worked out explicitly at roughly 0.0025. The argument pairs switch settings through a determinant-based construction that strengthens David Reimer's Butterfly Lemma. PSI said the system went on to improve its own result twice after the first complete proof, with Lean accepting the final version.

The claim is company-reported and has not yet been through peer review, but it carries unusual third-party weight. The Stanford team of Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who settled the conjecture's prediction for fixed-round quantum algorithms in August 2026, have been reading the full proof and are writing a shorter exposition of it for experts. "This is a huge result," they wrote to 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."

Credit for the work goes to David Turturean, a member of technical staff who developed the research system, scoped the problem and ran the system on it, then prompted the model to package the results into a first draft of the paper, which he reviewed and for whose correctness he is responsible. Advisor Jim Halverson audited the proof, and advisor Phiala Shanahan commented on the Lean formalization.

The result lands in a fast-moving sequence of AI-for-mathematics milestones: Meta reported in early October that its Muse Spark models had helped mathematicians settle five open problems, and Axiom Math formalized the entire Stacks Project into 16 million lines of Lean last week. What distinguishes the PSI claim is that the machine did not merely formalize known arguments or search a space of candidates. It produced a proof of a problem specialists count among the central open questions of quantum complexity theory, and then strengthened it without human direction.

If the proof survives community scrutiny, the significance cuts both ways. For quantum computing, it draws a sharper boundary around where exponential speedups can exist, pointing research toward structured problems. For AI, an unreleased frontier model, checked by a mechanical verifier, settling an 18-year-old conjecture is the strongest signal yet that the path from code-generation assistant to genuine research collaborator runs through formal verification, the one judge that cannot be fooled by fluent nonsense.