PSI Says AI Proved a Quantum Conjecture in Formalized Lean

By Amara Osei

Physical Superintelligence (PSI), the $58 million seed-funded startup, says its internal AI system completed a full proof of the Aaronson–Ambainis conjecture, open in quantum complexity theory since 2008. PSI says the system ran an unreleased, unnamed Anthropic model on PSI’s own infrastructure, then used Lean 4, a proof assistant that verifies every logical step, to check the proof.

PSI posted the paper and full formalization to GitHub on November 6, 2026. According to Quantum Zeitgeist’s November 7 report, the paper had not undergone journal peer review, and neither Scott Aaronson nor Andris Ambainis had publicly assessed it.

What did PSI claim to have proved?

According to PSI’s research note, the conjecture asks how much a quantum computer can accelerate any yes-or-no question about random, unstructured data. PSI says the proved limit is a polynomial amount of speedup. Exponential quantum gains, such as making large-number factoring easy on quantum computers while it remains apparently hard on classical ones, require exploitable hidden structure.

PSI’s chronology traces Aaronson’s early work to around 1999 and his formulation of the precise polynomial-influence statement with Ambainis in 2008. A 2019 Nathan Keller–Ohad Klein preprint claimed a proof but was withdrawn after a fatal flaw.

Paata Ivanisvili, who found that flaw, published partial work in September 2026. A Stanford group settled the fixed-round case in August, while the general case remained open until PSI’s announcement.

How did Lean verify the result?

PSI’s research note says instances of the unnamed, nonpublic Anthropic model produced the full proof on the third day of the run. Lean accepted the result. PSI then gave the system related open problems, and the system improved its own result twice; Lean accepted the final version as well.

The proof’s GitHub repository formalizes the development in Lean 4. It shows four main theorems with no placeholders (sorry) and no added axioms beyond standard Lean principles: propext, Classical.choice and Quot.sound.

According to the repository, two independent implementations of the Lean kernel rechecked the development: the official kernel and the Rust-based lean4lean. A comparator run on GitHub-hosted infrastructure accepted all four final theorems.

The PSI note cautions that Lean guarantees only the theorem as written in Lean. Experts still need to confirm that the formal statement matches the original conjecture exactly and check the paper’s nonformal portions, including the translation from the polynomial-influence bound to the quantum-query conclusion.

Who ran the proof?

According to PSI’s launch announcement, the company emerged from stealth on September 1, 2026, with a $58 million seed round led by Breakthrough Energy Ventures. PSI describes itself as an AI-native physics laboratory. Its main product, Emmy, comprises virtual physicists initially focused on data-center optimization.

PSI’s research note identifies David Turturean, a member of its technical staff, as the conjecture project’s leader. Turturean built the research system, scoped the problem and took responsibility for the paper.

What does PSI stand to gain?

PSI’s press release, carried by PR Newswire, presented Emmy and data-center optimization as the initial proof point for its technology. The conjecture proof, announced separately on November 6, 2026, served as a subsequent demonstration of the platform’s capabilities.

In the same release, CEO Matt Pines said: “PSI aims to industrialize the discovery of new physics.” The release added that its job was “to make that kind of ambition affordable and scalable again for our customers.”

What remains unresolved?

Quantum Zeitgeist’s November 7 account identified four gaps:

• Peer review: The paper had not yet completed journal peer review.
• Author assessment: Neither Aaronson nor Ambainis had published an evaluation as of November 7, 2026. A reader linked PSI’s note under Aaronson’s 2019 post about the withdrawn Keller–Klein proof and asked for his view.
• Model transparency: Anthropic’s model remained unreleased and unnamed. PSI had not disclosed the model’s identity, size or training details.
• Independent reproduction: The Lean code was public and rerunnable, but no third party had independently reproduced the AI-generated proof search.

Why does the result matter?

If the theorem holds, it would explain why decades of attempts to find exponential quantum speedups on unstructured black-box problems failed: PSI says the advantage is mathematically impossible. The result would require any such claim to identify hidden structure, while Grover-style polynomial speedups would remain allowed.

PSI’s account says the proof follows a 2023 plan by Shachar Lovett and Jiapeng Zhang. It closes the gap they left by proving a different inequality through a determinant-based pairing argument.

The Stanford group that solved the fixed-round case was reading the full proof, sending comments and writing a shorter version for specialists. In a PSI-published statement, the group called it “a major result that settles a conjecture standing for decades.”

What happens next?

Quantum Zeitgeist identifies the Stanford group’s write-up and any assessment from Aaronson and Ambainis as the next tests. PSI says it has already assigned related open problems to its system, citing a September 2026 paper on distributional variants. Until mathematical review ends, Quantum Zeitgeist still treats the result as a claim backed by an unusually rigorous computational receipt.