Startup Claims Unreleased Anthropic Model Proved 18-Year-Old Quantum Conjecture

A US startup called Physical Superintelligence (PSI) says an internal AI system running an unreleased Anthropic model has produced a complete proof of the Aaronson–Ambainis conjecture, a central open problem in quantum complexity theory since 2008. The proof was checked and accepted by Lean, a proof assistant that verifies every logical step. The paper and full formalization were posted to GitHub on 6 November 2026. The work has not been peer-reviewed, and neither Scott Aaronson nor Andris Ambainis had publicly assessed it as of 7 November 2026.

The claim

PSI, which emerged from stealth on 1 September 2026 with a $58 million seed round led by Breakthrough Energy Ventures, describes itself as an "AI-native physics laboratory." Its main product is Emmy, a team of virtual physicists initially focused on data-center optimization. The conjecture work was led by David Turturean, a member of PSI's technical staff, who built the research system, scoped the problem, and takes responsibility for the paper.

According to PSI's research note, the system—running instances of an unnamed, non-public Anthropic model on the company's own infrastructure—produced a full proof on the third day of the run. Lean accepted it. The system was then given related open problems and improved its own result twice; Lean accepted the final version as well.

What the conjecture says

The Aaronson–Ambainis conjecture asks how much a quantum computer can speed up the answer to any yes-or-no question about random, unstructured data. The answer, now claimed proved, is: at most a polynomial amount. Exponential quantum speedups—the kind that make factoring large numbers easy on a quantum computer but apparently hard on classical ones—only appear when the input data has a hidden pattern or structure to exploit.

The conjecture has a long history. Aaronson first worked on the underlying question around 1999. By 2008 he and Ambainis had formulated the precise polynomial-influence statement. A 2019 preprint by Nathan Keller and Ohad Klein claimed a proof but was withdrawn after a fatal flaw was found. Partial results continued, including a September 2026 paper by Paata Ivanisvili (who had spotted the 2019 flaw) and an August 2026 result from a Stanford group that settled the fixed-round case. The general case remained open until PSI's announcement.

Verification by Lean

The proof is formalized in Lean 4. The GitHub repository shows four main theorems proved with no placeholders (sorry) and no added axioms beyond standard Lean principles (propext, Classical.choice, Quot.sound). The development has been re-checked by two independent implementations of the Lean kernel (the official kernel and lean4lean, a Rust implementation). A comparator run on GitHub-hosted infrastructure accepted the four final theorems.

Lean guarantees that the theorem as written in Lean has been proved. Experts still need to confirm that the formal statement matches the original conjecture exactly, and to check the parts of the paper outside the formal proof (such as the translation from the polynomial-influence bound to the quantum-query conclusion).

What's missing

• Peer review: The paper has not yet been through journal peer review.
• Author assessment: Neither Aaronson nor Ambainis had published an evaluation as of 7 November 2026. A reader posted a link to PSI's note under Aaronson's 2019 blog post about the withdrawn Keller–Klein proof, asking for his view.
• Model transparency: The Anthropic model used is unreleased and unnamed. PSI has not disclosed which model, its size, or its training details.
• Independent reproduction: While the Lean code is public and rerunnable, the AI-generated proof search itself has not been independently reproduced by a third party.

PSI's incentives

PSI is a venture-backed startup ($58M seed) with a commercial product (Emmy) and a narrative of aiming to industrialize the discovery of new physics. A high-profile result in quantum complexity theory serves as a powerful demonstration of its platform. The company's press release quotes CEO Matt Pines saying "PSI aims to industrialize the discovery of new physics" and adds that its job is "to make that kind of ambition affordable and scalable again for our customers." The press release presented Emmy and data-center optimization as the initial proof point for its technology; the conjecture proof, announced separately on 6 November 2026, is a subsequent research result demonstrating the platform's capabilities.

If the result holds

The theorem would explain why decades of attempts to find exponential quantum speedups on unstructured black-box problems have failed: they are mathematically impossible. For quantum computing companies, it sharpens the burden of proof: anyone claiming exponential advantage on messy, patternless data must identify the hidden structure. Grover-style polynomial speedups remain allowed.

The proof follows a 2023 plan by Shachar Lovett and Jiapeng Zhang and closes the gap they left by proving a different inequality using a determinant-based pairing argument. The Stanford group that solved the fixed-round case has been reading the full proof, sending comments, and writing a shorter version for specialists. They described it in a PSI-published statement as "a major result that settles a conjecture standing for decades."

What happens next

The next real tests are the Stanford group's write-up and whatever Aaronson and Ambainis make of it. PSI says it has already set its system to work on related open problems, citing a September 2026 paper on distributional variants of the conjecture. Until the mathematical community finishes its review, the result remains a claim—albeit one with an unusually rigorous computational receipt.