Physical Superintelligence Claims a Proof of the Aaronson-Ambainis Conjecture: Claimed vs Verified

Physical Superintelligence (PSI) says an AI system has proved the Aaronson-Ambainis conjecture. On November 6, 2026 the company published a research page, a paper, and a Lean repository. It says the proof was found by its internal research system running a non-public Anthropic model, and that Lean, a proof assistant that checks every step, accepted it. The conjecture has been open since 2008.

This is a claim from the company that made the system. The Lean code is public, which is a real strength. Other parts are not yet checkable. This post separates the two.

TL;DR: claimed vs verified

What is the Aaronson-Ambainis conjecture?

Quantum algorithms like Shor's factoring algorithm get their speed from hidden structure in the input, such as a repeating pattern. Scott Aaronson and Andris Ambainis asked a different question: can a quantum computer be exponentially faster on random inputs, with no special structure? They showed that if a certain statement about low-degree polynomials is true, the answer is no. A quantum computer could then save at most a polynomial number of input reads on most inputs.

PSI describes the statement this way: take a polynomial f of degree d whose values stay between 0 and 1, and let v be the variance of its values. Flipping some input bit should change the output, on average, by at least a fixed power of v over d, no matter how many bits there are. Earlier general bounds shrank exponentially with the degree, which was too weak to settle the question.

PSI's stated result is that some bit i has influence at least c times v to the power 5/2 over d to the power 6, which is at least (v/d) to the power 7. The repository gives the constant as 8 times the square root of 15, over 125 times pi to the fourth. The research page renders the constant in a garbled way, so check the paper for the exact value.

If the result holds, then for yes/no questions on random strings, a quantum computer cannot save exponentially many input reads unless the string has a rare pattern. Our earlier post asked whether AI labs are hoarding solved math problems, and Aaronson's name appears there too.

How did PSI say it got the proof?

PSI describes an internal research system run on its own infrastructure, using instances of a non-public Anthropic model. According to the page:

• A complete proof existed by day three of the run.
• The system was then pointed at related open problems and improved the result twice.
• Lean accepted both the day-three proof and the final improved version.
• The page does not give the total length of the run, its cost, or how much human guidance went in beyond the roles listed.

The proof builds on named earlier work: Lovett and Zhang (whose plan relied on one conjectured inequality), David Reimer's Butterfly Lemma, Agarwal and Ben-David, Kulkarni and Tal, and Filmus, Hatami, Keller and Lifshitz. PSI says the key new step replaces Lovett and Zhang's conjectured inequality with a new inequality, proved by pairing switch settings through a determinant.

David Turturean, a member of technical staff, led the work: he developed the system, scoped the problem, ran it, had the model draft the results, reviewed the draft, and, in PSI's words, is responsible for its correctness. Advisor Jim Halverson audited the proof, and advisor Phiala Shanahan commented on the Lean formalisation. The README says the proof, paper and formalisation were AI-generated, with Turturean reviewing the paper.

What can you check yourself?

A puzzle fitting together with a green seal at its center, a metaphor for Lean formal verification of the Aaronson-Ambainis proof

The repository is the most valuable part of the release. From its README:

The repository showed one commit on its main branch and, when we looked, 6 stars. We did not run the build ourselves, so we report these steps as the README describes them.

This is the same pattern as PSI's October release. In our post on PSI's five open quantum problems with Lean proofs we noted that Lean checking confirms the formal statements follow, but not that those statements match the real problems.

What is not verified?

1. Statement fidelity. The README says whether the Lean statement PrintedConjecture matches the conjecture as printed is left for a human reader to confirm. If the formal statement is subtly weaker or different, a valid Lean proof proves the wrong thing.
2. An unformalised input. One hypothesis, FbsDegreeBound, from Agarwal and Ben-David, is not formalised and is an input to one theorem.
3. The paper. The README says the paper is not machine-checked. The prose argument rests on human review, and the proof was reviewed by the person who ran the system plus advisors.
4. Peer review. No journal or arXiv refereeing exists yet.
5. The model. A non-public Anthropic model cannot be tested by outsiders, so the process cannot be reproduced. Only the output can be checked.
6. Outside reaction. PSI quotes four Stanford researchers, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who read the proof. According to PSI's page, they call it "a huge result" and say the proof brings everything together "in a rather magical way". Those comments are relayed by PSI, not published by the authors themselves. The page also notes that the same Stanford group proved a special case in August 2026, for quantum algorithms with a fixed number of parallel rounds. We found no public assessment from Aaronson or Ambainis.

Why does this keep happening in AI math?

AI-assisted proofs are arriving faster than the community can review them. We have covered the same shape several times: Axiom's Lean formalisation of the classification of finite simple groups, Axiom's 16-million-line Stacks Project formalisation, and the Discovered prize for five open materials-science problems. Anthropic has also published a report on 207,000 Claude scientist research sessions.

Each time, the verification story is similar. The formal proof is checkable by machine. The link between the formal statement and the real question needs expert reading, and expert reading takes weeks or months. A fast announcement and slow confirmation are normal here, and neither means the claim is wrong.

What should you watch next?

• Expert posts. Aaronson, Ambainis and quantum complexity researchers commenting on the proof or the statement match.
• A second formalisation or independent audit of PrintedConjecture against the original paper.
• The Stanford group's exposition. PSI says their shorter expert write-up is still being prepared.
• arXiv and journal status. Whether the paper is submitted and refereed.
• Anthropic. Whether it comments on the non-public model, which it has not, as far as we could find.

What this means for readers

If you follow AI-for-science news, treat this as a strong claim with unusually good evidence for its formal part and the usual open questions about everything else. If you build with AI, the release is a useful example of how to make an AI result auditable: a pinned toolchain, an axiom audit, a replay target and a clearly stated list of what is not checked. Copy that format when you publish your own results. If you are deciding what to believe, wait for the statement check and outside review before calling the conjecture settled.

Related reading

• PSI's five open quantum problems with Lean proofs: claimed vs verified
• Are AI labs hoarding solved math problems?
• Axiom: classification of finite simple groups in Lean
• Axiom: Stacks Project in Lean
• Discovered: $1 million for five open materials-science problems
• Anthropic report on 207,000 Claude scientist sessions

Details reflect PSI's research page and repository on November 6, 2026 and may change as experts respond.