News · 2026-11-07

PSI reports an AI-assisted Lean proof of a quantum-computing conjecture

Physical Superintelligence says its AI research system produced a Lean-checked proof of the Aaronson–Ambainis conjecture, a question connecting the structure of Boolean functions to quantum query speedups. The group has published a paper and formalization, while independent review of the statement and argument remains important.

Key facts

• PSI’s November 6 announcement describes its research system and result.
• Its public repository contains a paper and Lean formalization.
• PSI says a complete initial proof appeared on day three and was later improved.
• The original conjecture appears in Aaronson and Ambainis’s 2009 paper.

The conjecture concerns a bounded, low-degree mathematical function whose output varies over Boolean inputs. Roughly, it says that if the output varies enough, at least one input coordinate must have a meaningful influence. This is useful in a theoretical setting where researchers compare quantum query algorithms with classical ways of examining inputs; it is not a claim about all practical quantum computers.

A proof assistant is like a very strict checker for a chain of mathematical steps. It can check that the conclusions follow from the definitions and assumptions encoded in its language. It cannot by itself guarantee that those definitions capture the intended human question, that the right file was checked, or that every part of a separate paper has been formalized. PSI’s repository itself calls attention to this trust boundary. Our research pass did not independently rebuild the project. The site’s proof-assistant lesson explains the distinction.

PSI says its system used an unnamed non-public Anthropic model on PSI infrastructure. The group credits David Turturean with developing the harness, running the task and accepting responsibility for correctness, and names advisors who reviewed the work. It does not disclose enough to assign a precise share of the proof to one model or to Anthropic. No Anthropic endorsement is established in the reviewed material.

PSI reports that outside researchers reading the proof called it a “huge result,” but says further exposition is in preparation. That is an encouraging early signal attributed to PSI, not completed peer review or consensus. An earlier purported proof of the conjecture was withdrawn; Scott Aaronson’s account illustrates why mathematical review and careful statement matching matter even for exciting claims.

The practical significance extends beyond this theorem. A system that proposes ideas and checks formal steps can narrow the feedback loop for research. The important unanswered question is how much independent work was required to encode, inspect and validate the result, and how reliably the same process succeeds on other problems.

The result uses a formal proof assistant called Lean. PSI's repository maps named declarations to the theorem statement and provides verification materials. The research notes say the project records checks through Lean's kernel and a second type-checker implementation. Those are statements about the published artifact and its reported checks; the current synthesis did not run the software and cannot independently attest to its build environment.

There are at least three things to inspect. First, does the formal statement say what mathematicians mean by the conjecture? Second, do the proof and its dependencies check under the stated assumptions and toolchain? Third, does the human-readable paper correctly explain the formal development? Success on one question is evidence about that question; it does not automatically answer the other two. PSI's own trust-boundary discussion says portions of the paper do not have a formal counterpart.

The chronology also needs care. PSI says a complete initial proof appeared on day three, followed by improvements to the bound. The shorthand that an AI 'solved it in three days' can conceal later refinement as well as the human work of defining the task, constructing the harness and auditing the outcome. PSI reports that its system used instances of a non-public Anthropic model, but the reviewed announcement does not name the model or apportion each contribution across tools and people.

An independently checked formal result would still need interpretation within its field. Other mathematicians must inspect assumptions, connect the theorem to the established literature and test the stated implications. PSI reports that outside researchers are reading the work; their eventual analysis is a more informative signal than social-media enthusiasm. The wider opportunity is a research loop that proposes arguments and uses formal feedback, while the limitation is that reliable formal verification begins only after a meaningful question has been encoded.

Primary source, verified: read the paper →

Ground Truth. (2026, November 7). PSI reports an AI-assisted Lean proof of a quantum-computing conjecture. Ground Truth. https://groundtruth.day/news/psi-ai-aaronson-ambainis-lean-proof.html

@misc{groundtruth:psi-ai-aaronson-ambainis-lean-proof,
  title  = {PSI reports an AI-assisted Lean proof of a quantum-computing conjecture},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {nov},
  url    = {https://groundtruth.day/news/psi-ai-aaronson-ambainis-lean-proof.html}
}

Topics: research · mathematics · agents