AI Proved What?

PSI06 (outside OpenAI’s math catalogue), November 2026

The Aaronson–Ambainis conjecture, proved?

PSI says a non-public Anthropic model found a proof, with a 60-page paper and a Lean proof of the influence bound. Not yet on arXiv, peer reviewed or checked by anyone outside PSI.

Play PSI06: the Aaronson–Ambainis conjecture. PSI’s four-bit example as two cubes, with bit 4’s edges in yellow, and the bound Inf ≥ (ε/d) to the 7th.

7:03. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:57The claim
  3. 4:00What Lean checked
  4. 5:38Where it stands

The claim, in plain words

This is PSI06. Some quantum algorithms need exponentially fewer looks at their input than any ordinary algorithm. Shor’s factoring algorithm is one, and it works because its input hides a repeating pattern: structure. The looks are called queries. Beals, Buhrman, Cleve, Mosca and de Wolf showed that after T queries, a quantum algorithm’s chance of saying yes is a polynomial in the input bits, of degree at most 2T, with values between zero and one. Here is PSI’s own example: a polynomial of degree two on 4 bits. Each corner of these two cubes is one of the 16 inputs, shaded by its value. The influence of a bit is the change in value when that bit is flipped, squared and averaged over all inputs. By our count, bit 4’s influence is a quarter; the other three have 0.02, 0.02 and 0.01.

Is there always an influential bit? The question goes back to a 2008 lecture by Scott Aaronson. With Andris Ambainis, in a paper first posted in 2009, he stated it as a conjecture. If a polynomial of degree at most d stays between zero and one on every input, and its variance is at least ε, then some bit has influence at least (ε/d) to a fixed power, however many bits there are. They showed this would let an ordinary algorithm imitate any quantum one on most inputs, with only polynomially more queries. So exponential speedups would need structure. Earlier bounds for general polynomials shrank exponentially with the degree. In 2019, Nathan Keller and Ohad Klein posted a claimed proof, then withdrew it, writing: our proof contains a serious flaw. In August 2026, a Stanford group proved its prediction in a special case: quantum algorithms that query in a fixed number of parallel rounds.

On November 6, 2026, the company PSI, Physical Superintelligence, announced: the Aaronson–Ambainis conjecture is now a theorem. With the post came a public repository, holding a 60-page paper by David Turturean and a Lean proof. In Aaronson and Ambainis’s own terms, the main result says some bit has influence at least a constant c, times ε^(5/2)/d⁶. And that is at least (ε/d)⁷. The constant is 8√15/(125π⁴): about 0.0025. Through the known reduction, the paper says, a quantum algorithm making T queries can be imitated on most inputs by an ordinary one making at most (4T)⁸ queries, times factors for the allowed error and for the fraction of inputs allowed to fail. Who did the work? The paper says its mathematical statements were produced by AI models: instances of a non-public Anthropic model, in a research harness that Turturean built at PSI. He prompted the first draft, reviewed and edited it, and is responsible for its correctness. We cannot check which model was used. AI Proved What? is itself made with Claude, Anthropic’s AI.

Where it stands

Released by PSI
Blog post, November 6, 2026; repository with one commit (2a6ceae, “Initial commit”, November 6 UTC) holding the 60-page paper by David Turturean and the Lean proof.
On arXiv, peer reviewed
No arXiv or ECCC posting found as of November 6, 2026; not peer reviewed.
Independent review
None yet. Jim Halverson audited the proof and Phiala Shanahan commented on the Lean; both are PSI advisors. The Stanford group (Guy Blanc, Jordan Docter, Carmen Strassle, Li-Yang Tan) is quoted on PSI’s page and, PSI says, is writing a shorter exposition; we found no statement under their own names, and none from Scott Aaronson or Andris Ambainis.
Independent check of the Lean
None found: PSI ran the recorded build, replay and comparator checks itself, on rented machines and in private GitHub repositories, on October 22 and November 6, 2026 (copied logs; PSI’s notes: “None has been repeated by another party”); the public repository shows 0 Actions runs as of November 6, 2026.
Lean proof, by PSI
Lean 4.33.0, Mathlib v4.33.0. The statement PrintedConjecture imports only Mathlib, with the bound (ε/d)7; no placeholder and no added axiom, per the README. Covers the influence bound (Theorem 1.1, Corollary 1.2), not the quantum consequences (paper Section 1.3) or the survey, overview and remarks (Sections 1.4, 1.5, 9). Not built or run by us.

Last checked November 6, 2026. Where it stands. The paper is not on arXiv, as of November 6, and has not been peer reviewed. Jim Halverson audited the proof, and Phiala Shanahan commented on the Lean; both are PSI advisors, so not independent of PSI. PSI quotes the Stanford group, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan: this is a huge result. PSI says they are writing a shorter exposition of the proof; we found no statement under their own names yet. The paper thanks Scott Aaronson for referring PSI to them. We found no public statement from Aaronson or Ambainis. The Lean proof is PSI’s; we did not build or run it.

This is outside OpenAI’s math catalogue, and PSI’s second entry, after PSI01–05. If it holds, a question open since 2008 is settled: bounded polynomials of low degree have influential bits, so exponential quantum speedups in the query model need structure. The proof comes with machine checks that anyone can repeat, though no outsider has published a run yet. What remains is for outside experts to confirm that the short Lean statement says what Aaronson and Ambainis meant, and to read the paper’s parts that Lean does not cover. See PSI01–05.

How the proof goes, and what Lean checked

  1. The outline. The proof, which the paper calls elementary, follows a plan of Shachar Lovett and Jiapeng Zhang. Slice the function at every level. At every input, give each bit a weight, so that flipping any group of bits changes the value by at most the group’s total weight. Their plan left one inequality as a conjecture. The new proof puts an all-pairs inequality in its place, proved with a one-to-one pairing of inputs that comes from a determinant. That pairing refines David Reimer’s Butterfly Lemma. By the paper’s timeline, the first complete proof came on the third day of the run, with exponent 22 in place of 7, and was checked in Lean. Later work in the run brought it to 11, then 7, each checked in Lean.
  2. The statement. Now the Lean proof. The statement it proves is called PrintedConjecture. It imports only Mathlib, Lean’s community library, and is written with ordinary polynomials and finite sums, with the bound (ε/d)⁷. The README says a reader needs to read only this definition to check what the theorem proves. There are four public theorems; one assumes an unformalized result of Agarwal and Ben-David, only to improve the constant. The repository says there is no placeholder and no added axiom, only Lean’s three standard ones. Our own count: 95 Lean files, about 9,600 lines. PSI reports 761 declarations.
  3. The checks. Then the checks, as PSI records them. Every declaration was replayed by Lean’s own kernel checker, and again by lean4lean, an independent implementation of Lean’s type checker. A tool called comparator matched the four theorems against the plain statements, with a third kernel, nanoda, written in Rust. Controls are included: a false file that an ordinary build accepts but both replays reject, and four wrong comparator solutions, all rejected. But PSI ran all these checks itself, on rented machines and in private GitHub repositories, first on October 22 and again on November 6. Only copied logs are public, and the public repository shows zero runs so far. And the checks cover the influence bound only. The quantum consequences, in Section 1.3 of the paper, have no Lean counterpart, and neither do its survey, overview and closing remarks.

The numbers in the video

  • PSI’s example f(x) = 0.1 + 0.5x4 + 0.2x1x2 + 0.1x3 (from its post). Ours: values 0.1 to 0.9; influences (squared change, averaged over the 16 inputs) 0.02, 0.02, 0.01, 0.25; variance 0.0725.
  • The constant c = 8√15/(125π⁴) = 0.002545, “about 0.0025” (post); the paper’s Theorem 1.1 uses √15/(500π⁴) ≈ 7.95e-05 on the cube with values ±1, which is c/32.
  • Exponents during the run (paper, Appendix A): 22, then 11, then 7, each checked in Lean. Query bound (paper, Section 1): (4T)⁸ε⁻¹⁴δ⁻⁸.
  • Ours: 95 Lean files, 9,625 lines in the repository at commit 2a6ceae. PSI’s count: 761 declarations (648 theorems, 113 definitions) in 84 modules.
  • Keller and Klein’s 2019 claimed proof (arXiv:1911.03748) was withdrawn on December 2, 2019: “Unfortunately, our proof contains a serious flaw.”

Read the source

AI Proved What? is independent and not affiliated with PSI, Anthropic (beyond using Claude) or OpenAI, or with the researchers named. It is made with Claude, Anthropic’s AI, and holds results made with Anthropic models to the same standards.

Transcript

Read the full script

0:00The question

This is PSI06. Some quantum algorithms need exponentially fewer looks at their input than any ordinary algorithm. Shor’s factoring algorithm is one, and it works because its input hides a repeating pattern: structure. The looks are called queries. Beals, Buhrman, Cleve, Mosca and de Wolf showed that after T queries, a quantum algorithm’s chance of saying yes is a polynomial in the input bits, of degree at most 2T, with values between zero and one. Here is PSI’s own example: a polynomial of degree two on 4 bits. Each corner of these two cubes is one of the 16 inputs, shaded by its value. The influence of a bit is the change in value when that bit is flipped, squared and averaged over all inputs. By our count, bit 4’s influence is a quarter; the other three have 0.02, 0.02 and 0.01. Is there always an influential bit? The question goes back to a 2008 lecture by Scott Aaronson. With Andris Ambainis, in a paper first posted in 2009, he stated it as a conjecture. If a polynomial of degree at most d stays between zero and one on every input, and its variance is at least ε, then some bit has influence at least (ε/d) to a fixed power, however many bits there are. They showed this would let an ordinary algorithm imitate any quantum one on most inputs, with only polynomially more queries. So exponential speedups would need structure. Earlier bounds for general polynomials shrank exponentially with the degree. In 2019, Nathan Keller and Ohad Klein posted a claimed proof, then withdrew it, writing: our proof contains a serious flaw. In August 2026, a Stanford group proved its prediction in a special case: quantum algorithms that query in a fixed number of parallel rounds.

1:57The claim

On November 6, 2026, the company PSI, Physical Superintelligence, announced: the Aaronson–Ambainis conjecture is now a theorem. With the post came a public repository, holding a 60-page paper by David Turturean and a Lean proof. In Aaronson and Ambainis’s own terms, the main result says some bit has influence at least a constant c, times ε^(5/2)/d⁶. And that is at least (ε/d)⁷. The constant is 8√15/(125π⁴): about 0.0025. Through the known reduction, the paper says, a quantum algorithm making T queries can be imitated on most inputs by an ordinary one making at most (4T)⁸ queries, times factors for the allowed error and for the fraction of inputs allowed to fail. Who did the work? The paper says its mathematical statements were produced by AI models: instances of a non-public Anthropic model, in a research harness that Turturean built at PSI. He prompted the first draft, reviewed and edited it, and is responsible for its correctness. We cannot check which model was used. AI Proved What? is itself made with Claude, Anthropic’s AI. The proof, which the paper calls elementary, follows a plan of Shachar Lovett and Jiapeng Zhang. Slice the function at every level. At every input, give each bit a weight, so that flipping any group of bits changes the value by at most the group’s total weight. Their plan left one inequality as a conjecture. The new proof puts an all-pairs inequality in its place, proved with a one-to-one pairing of inputs that comes from a determinant. That pairing refines David Reimer’s Butterfly Lemma. By the paper’s timeline, the first complete proof came on the third day of the run, with exponent 22 in place of 7, and was checked in Lean. Later work in the run brought it to 11, then 7, each checked in Lean.

4:00What Lean checked

Now the Lean proof. The statement it proves is called PrintedConjecture. It imports only Mathlib, Lean’s community library, and is written with ordinary polynomials and finite sums, with the bound (ε/d)⁷. The README says a reader needs to read only this definition to check what the theorem proves. There are four public theorems; one assumes an unformalized result of Agarwal and Ben-David, only to improve the constant. The repository says there is no placeholder and no added axiom, only Lean’s three standard ones. Our own count: 95 Lean files, about 9,600 lines. PSI reports 761 declarations. Then the checks, as PSI records them. Every declaration was replayed by Lean’s own kernel checker, and again by lean4lean, an independent implementation of Lean’s type checker. A tool called comparator matched the four theorems against the plain statements, with a third kernel, nanoda, written in Rust. Controls are included: a false file that an ordinary build accepts but both replays reject, and four wrong comparator solutions, all rejected. But PSI ran all these checks itself, on rented machines and in private GitHub repositories, first on October 22 and again on November 6. Only copied logs are public, and the public repository shows zero runs so far. And the checks cover the influence bound only. The quantum consequences, in Section 1.3 of the paper, have no Lean counterpart, and neither do its survey, overview and closing remarks.

5:38Where it stands

Where it stands. The paper is not on arXiv, as of November 6, and has not been peer reviewed. Jim Halverson audited the proof, and Phiala Shanahan commented on the Lean; both are PSI advisors, so not independent of PSI. PSI quotes the Stanford group, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan: this is a huge result. PSI says they are writing a shorter exposition of the proof; we found no statement under their own names yet. The paper thanks Scott Aaronson for referring PSI to them. We found no public statement from Aaronson or Ambainis. The Lean proof is PSI’s; we did not build or run it. This is outside OpenAI’s math catalogue, and PSI’s second entry, after PSI01–05. If it holds, a question open since 2008 is settled: bounded polynomials of low degree have influential bits, so exponential quantum speedups in the query model need structure. The proof comes with machine checks that anyone can repeat, though no outsider has published a run yet. What remains is for outside experts to confirm that the short Lean statement says what Aaronson and Ambainis meant, and to read the paper’s parts that Lean does not cover.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.