Where quantum computers could really pull ahead
- What it is
- PSI reports an AI-assisted proof of the Aaronson–Ambainis conjecture: a bounded, low-degree polynomial with meaningful variation must have at least one influential input.
- Who did it
- David Turturean at PSI, using an internal research system powered by a non-public Anthropic model; human review and contributions are disclosed.
- What it could mean
- Where might quantum computers earn their keep? This result could sharpen that search by showing why special structure matters for dramatic query advantages. It does not make quantum computers obsolete.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
A proof of the Aaronson–Ambainis conjecture ↗See the proposed checks
Compare PrintedConjecture with the original Aaronson–Ambainis Conjecture 1.7, including the uniform distribution, degree, variance and bit-flip normalization. Trace the three core endpoints separately from the conditional improved bound. Then independently replay the pinned dependency closure in an isolated environment and inspect the query-complexity consequence separately; it is outside the Lean formalization.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
One input direction cannot stay invisible
The cube introduces Boolean inputs; parallel edges represent flipping the same input bit. The amber direction suggests influence. This is an illustrative three-dimensional example, not the theorem’s proof, a measured influence plot or a quantum device.
Read the source · Theorem 1.1; Conjecture.lean · bounded low-degree polynomial influence ↗- Source kind
- Mathematical research record
- Evidence reported
- Manuscript; independent examination not started
- Source date
- ; added 2026-11-06
- What it claims
- For a real polynomial p of degree at most d, bounded between 0 and 1 on the Boolean cube, and variance at least ε>0 under uniform inputs, the manuscript claims some coordinate has squared bit-flip influence at least (8√15/(125π⁴)) ε^(5/2)/d⁶, hence at least (ε/d)⁷. Three public Lean endpoints state the core conjecture and explicit bounds. A fourth, stronger-constant endpoint assumes FbsDegreeBound, an external theorem not formalized in this repository.
- Why this could matter
- Where quantum computers could really pull ahead Quantum computers are costly to build. Knowing where a dramatic advantage is possible could help researchers choose better targets. This result would narrow one theoretical route to that advantage; it does not measure hardware performance or supply a fast classical replacement.
- If it holds up
- It would settle the influence conjecture and support a classical query-simulation guarantee on most uniformly random inputs, sharpening the distinction between structured quantum opportunities and unstructured ones.
- If it does not
- The failed statement, dependency or translation would identify what needs repair; it would not show that every claimed quantum advantage is real.
- Impact horizon
- Foundational · Quantum computing · Computational complexity · Formalized mathematics
- Version
- 2026-11-06; November 2026 manuscript; repository release 1.1.0 at Git commit 2a6ceaef872ae993708950f951989134084b851a.
- Why we tracked it
- source-reviewed intake only; independent examination has not started.
- Highest-risk dependency
- Analyst judgment: theorem-to-formal-statement correspondence and the published verification provenance remain to be independently examined. The fourth endpoint assumes FbsDegreeBound; the core three do not. The quantum consequence concerns acceptance-probability approximation on most uniformly random Boolean inputs and counts input queries, not total runtime. Publisher-reported outside comments are not completed journal peer review or State of Proof validation.
- Available artifacts
- Pinned PSI repository 2a6ceaef872ae993708950f951989134084b851a; November 2026 manuscript, Conjecture.lean, Main.lean, axiom report, paper-to-Lean map and recorded Lean/lean4lean/comparator checks. Lean 4.33.0; Mathlib db584cd6d46c92f209a44c0f1c829460d327499d. The records report only propext, Classical.choice and Quot.sound for the final endpoints. These are publisher-supplied verification records; State of Proof has not executed the proof or replayed the checks.
- Current boundary
- Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Compare PrintedConjecture with the original Aaronson–Ambainis Conjecture 1.7, including the uniform distribution, degree, variance and bit-flip normalization. Trace the three core endpoints separately from the conditional improved bound. Then independently replay the pinned dependency closure in an isolated environment and inspect the query-complexity consequence separately; it is outside the Lean formalization.