AI System Proves 18-Year Quantum Conjecture in Three Days, Lean Proof Confirms

A research system built by Physical Superintelligence (PSI) and running a non-public Anthropic model has produced a machine-verified proof of the Aaronson-Ambainis conjecture — an open problem in quantum complexity theory that has gone unresolved since 2008. PSI announced the result on November 6, 2026, alongside a Lean 4 formalization that the company says passed independent type-checking with no unproven placeholders and no axioms beyond the foundations of standard mathematics.

The conjecture, originally posed by computer scientists Scott Aaronson and Andris Ambainis, asks whether every bounded low-degree polynomial defined over Boolean inputs necessarily has at least one variable with high influence on its output. If the answer is yes — which the proof claims to establish — then every quantum algorithm can be classically simulated on most inputs using only polynomially more computation. The implication is precise: exponential quantum speedups require that the problem's inputs carry specific algebraic structure. Without that structure, the quantum computer does not gain a meaningful advantage.

The AI system completed the core proof in approximately three days of computation, according to PSI. The team then prompted the system on related questions, triggering two rounds of exponent refinement before the final result was formalized and verified. The verified influence bound is at least (8√15 / (125π⁴)) · ε^(5/2) / d^6, equivalently expressed as (ε/d)^7 — a polynomial relationship where previous general bounds had decayed exponentially with degree.

An 18-Year Gap and the Partial Proof That Came Two Months Earlier

The Aaronson-Ambainis conjecture sits at the center of a question that has shaped quantum computing theory for three decades: does quantum computation require structured problems to outperform classical algorithms by an exponential margin?

Aaronson and Ambainis formalized this intuition into a concrete polynomial-analysis question in papers from 2008 and 2014. In the query complexity model — where the complexity of an algorithm is measured by how many times it reads its input — Beals et al. had already shown in 1998 that total Boolean functions always have a polynomial relationship between classical and quantum query complexity. That meant exponential quantum speedups could only emerge from partial (promise) functions — problems where the input is guaranteed to satisfy some global condition, like periodicity in Shor's algorithm. The simulation conjecture generalized this intuition to the low-degree polynomial setting, and the Aaronson-Ambainis conjecture became its concrete formulation.

For 18 years, researchers made only limited progress. In 2023, Shachar Lovett and Jiapeng Zhang published a strategy that reduced the full conjecture to a single unproven inequality. The strategy worked in every other respect — but that one gap, a bound on a sum over all pairs of Boolean inputs, resisted every attempt to close it. Standard combinatorial tools, including David Reimer's Butterfly Lemma, were too weak.

As recently as August 19, 2026, the problem was still open. A team at Stanford — Guy Blanc, Jordan Docter, Carmen Strassle, and Li-Yang Tan — published a paper titled "Quantum Speedups Require Structure or Depth" that proved a special case: the parallel-round version of the conjecture, where the quantum algorithm is restricted to a single parallel round of queries. This was genuine progress, but the full conjecture remained unsolved. The Stanford team is now reviewing PSI's full proof and preparing a shorter exposition aimed at theoretical computer scientists.

How the AI System Filled the Gap

PSI Member of Technical Staff David Turturean built the research system, scoped the problem, and ran it on PSI's infrastructure. The system was given the Lovett-Zhang proof strategy and tasked with finding an inequality that would work where existing tools had failed.

The key contribution is a new determinant-based pairing inequality — strictly stronger than the Butterfly Lemma. Where Reimer's lemma bounds a sum over pairs of inputs using a combinatorial argument, PSI's AI found a bound based on the determinant of a matrix constructed from a bijection over input pairs, full technical details available in PSI's public repository. This approach turns out to be the missing piece that makes the entire Lovett-Zhang strategy complete.

The full proof proceeds in four steps. First, the determinant-based inequality is applied to establish an all-pairs bound using the bijection construction. Second, this bound is converted into an integral over the level sets of the polynomial, translating the combinatorial argument into a continuous form. Third, the bound is averaged over all coordinates to show that at least one coordinate must have high influence. Fourth, a pointwise sensitivity bound establishes the row constraint needed to complete the influence calculation. The chain produces the final (ε/d)^7 bound.

The AI system did not stop at its first proof. After Turturean prompted the system on related open problems, it improved the intermediate exponent twice before the formalization was run, arriving at the final result. This iterative behavior — generating a valid proof then tightening it autonomously — is consistent with the kind of post-training refinement increasingly visible in frontier AI systems applied to formal mathematics.

PSI advisors Jim Halverson and Phiala Shanahan audited the proof and the Lean formalization respectively. Both are PSI affiliated, not independent external reviewers — a distinction the community will note when evaluating the announcement.

What Lean Verification Means — and What It Does Not

The Lean 4 formalization is the most technically significant aspect of PSI's claim, and understanding its scope matters for evaluating the result.

Lean is a proof assistant that mechanically checks every logical step of an argument against declared axioms. A proof compiles in Lean only when every intermediate claim follows from established lemmas or axioms — there are no gaps that a human reviewer might skip over or assume correct. PSI reports that the full proof passed Lean's core kernel, then passed lean4lean (an independent type checker that re-verifies Lean's own kernel), and finally passed a sandboxed comparator using the Lean and nanoda kernels to validate the proof's four final theorems.

This is a meaningful guarantee. AI-generated proofs have been announced before without formal verification, leaving the mathematics community to audit them manually — a slow and error-prone process for arguments that may be hundreds of pages long. Lean verification means anyone can independently run the check: the proof either compiles or it does not.

But Lean verification has a specific scope. It confirms that the formal Lean code proves the formal Lean statement. It cannot confirm that the formal statement precisely matches the Aaronson-Ambainis conjecture as Aaronson and Ambainis intended it. This is known as the statement-fidelity problem, and it requires human review to resolve. PSI's human-readable paper is not machine-checked; reviewers must confirm that the formalized conjecture and the original problem are the same thing. That review is ongoing.

The trusted base also includes Lean's compiler, the Mathlib library of formalized mathematics, and the hardware running the checks — meaning the guarantee has practical limits even when the kernel accepts the proof.

The Boundary the Proof Draws Around Quantum Advantage

The practical consequence of the Aaronson-Ambainis conjecture being true is a theorem about quantum simulation: every T-query quantum algorithm can be classically simulated, on most inputs, by a T^O(1)-query classical algorithm. This is the simulation conjecture, and it was the original motivation for Aaronson and Ambainis's polynomial formulation.

What this means in practice is that quantum computers can only achieve exponential speedups when the input problem carries specific algebraic structure that a quantum algorithm can exploit. Period-finding — the core of Shor's algorithm for factoring and discrete logarithm problems — is exactly this kind of structured problem. The quantum Fourier transform works because the input is guaranteed to be periodic; that periodicity is the structure the algorithm needs.

Nothing in PSI's result changes this. Shor's algorithm remains valid. Post-quantum cryptography planning, which proceeds on the assumption that Shor's algorithm breaks current public-key cryptosystems when run on a sufficiently large quantum computer, is unaffected. The result adds something different: a mathematically proven lower bound showing that if the problem lacks that kind of structure, the quantum computer cannot gain an exponential advantage.

For the quantum computing industry and its investors, this is a refinement of a long-understood principle — quantum advantage is not general, it is structural — now supported by a machine-verified proof rather than expert consensus. Claims of general quantum supremacy on unstructured problems now face a formal boundary.

The result is bounded by its model. The query complexity model counts only how many times an algorithm reads its input, treating each query as equally costly. Real quantum hardware involves error rates, decoherence, and circuit depth — factors that query complexity does not capture. The simulation conjecture's conclusion is therefore a theoretical statement about query access, not a verdict on whether near-term quantum hardware can outperform classical computers in practice.

A Proof Awaiting Peer Review and Its Originators' Response

Several open questions surround the result. Neither Scott Aaronson nor Andris Ambainis — the conjecture's originators — has publicly responded to PSI's announcement as of November 7, 2026. Their assessment would carry particular weight, both for the mathematical community and for confirming that PSI's formal statement captures the intended problem. The absence of a response is not unusual at this stage, but the community will watch for it.

The paper has not undergone peer review. No journal submission has been announced. For a result of this significance — one that closes a conjecture that the theoretical computer science community has spent 18 years attempting to prove — independent peer review by experts in Boolean analysis and query complexity is the standard the field requires. The Stanford team's review and planned exposition provides a form of expert scrutiny, but it is not a substitute for the full peer-review process.

The question of how to attribute AI-generated mathematical contributions is also evolving. As Lean verification becomes standard for AI-assisted proofs, the mathematics community is beginning to ask for provenance graphs alongside formal certificates — documentation of which steps were generated by the AI, which were proposed by the human researchers, and whether any critical step resembles prior unpublished work. Some commentators have called for a full literature audit with each AI-generated proof, verifying that no decisive step was silently borrowed from existing unpublished work in the field. PSI's disclosure names David Turturean as the person responsible for the paper's correctness, which is a step toward the kind of human-accountable attribution the field is beginning to expect.

PSI's Aaronson-Ambainis announcement follows its October 23, 2026 batch, in which the company used both OpenAI and Anthropic models to publish results on five open quantum information problems. In less than two weeks, PSI has now produced six claimed proofs of open problems, all Lean-verified, all with named human researchers accountable for correctness. The pace is unusual. Whether the results hold under the scrutiny of full peer review will determine whether PSI's model of AI-native physics research — human scientists directing, AI systems executing — represents a durable methodology or a streak of early successes that the field will take months to evaluate.

The next milestone for this specific result is straightforward: a confirmed statement-fidelity review, a public response from Aaronson and Ambainis, and a peer-reviewed publication. If those three things arrive with the proof intact, the Aaronson-Ambainis conjecture will join the list of formally closed problems — and the simulation conjecture, unresolved for 30 years, will follow.