AI helped close a quantum conjecture. Keep the proof receipt

01

WHAT ACTUALLY CHANGED

PSI released a claimed proof of the Aaronson-Ambainis conjecture and the artifacts needed to inspect it. The conjecture originated in work by Scott Aaronson and Andris Ambainis on the structure required for quantum speedups. Their paper connected a statement about influential variables in low-degree polynomials with limits on how far certain quantum query algorithms can separate themselves from classical algorithms on most inputs. PSI's theorem gives an explicit lower bound on the influence of at least one variable. In the notation used by the project, the bound is proportional to epsilon raised to the five-halves power divided by the sixth power of the degree. The important point for non-specialists is that the influence cannot vanish arbitrarily fast. A polynomial relationship exists.

The project describes a mixed machine and human research process. PSI says an internal system used instances of a non-public Anthropic model and reached a complete proof during the third day of a run. The public report does not make that entire system reproducible. It does name the human lead, the internal audit and the external experts reviewing the result. That distinction matters. Saying an AI proved a theorem compresses several jobs into one sentence. A model can propose lemmas and proof steps. A research system can search, test and package them. Lean can verify a formal derivation. Humans choose the problem, interpret the claim, audit the formalization, connect it with the literature and accept responsibility.

The proof is accompanied by a complete Lean formalization. Lean is a proof assistant. It translates a theorem into precise objects and checks each permitted inference. The public repository says the development has no placeholders and introduces no extra axioms. PSI also reports that two independent Lean kernels rechecked the proof. Independent kernels reduce the chance that one checker implementation silently accepted an invalid proof. They do not remove every trust assumption. Users still depend on the theorem statement, definitions, library, compiler path and the foundations that Lean permits. The receipt should expose those boundaries instead of treating verified as a synonym for infallible.

Independent mathematical review is still underway. PSI reports that Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan at Stanford have been reading the proof, sent comments and are writing a shorter expert exposition. That is encouraging because a formal proof and a readable proof serve different purposes. The formal object establishes a checkable derivation. The exposition helps mathematicians understand the central idea, compare it with earlier techniques, find fragile interpretations and decide where the method might travel next. A proof can be formally accepted and still need a great deal of human explanation before a field knows what it has learned.

02

WHY THIS MATTERS

For mathematicians, the release offers something better than a screenshot of a successful run. The public code lets specialists inspect definitions, dependencies and proof structure. They can challenge the correspondence between the informal conjecture and the formal theorem. They can attempt shorter arguments, test alternate assumptions and identify which lemmas contain the real idea. That is how a machine-assisted result becomes part of mathematics rather than a product demonstration with unusually stern punctuation.

For quantum computing, the result clarifies a theoretical boundary rather than delivering a new machine. The original Aaronson-Ambainis work asks when quantum algorithms can achieve dramatic query advantages over classical methods. Resolving the conjecture strengthens that line of theory. It does not produce a faster chip, a new error-correcting code or an immediate quantum advantage for a commercial workload. Readers should celebrate the theorem at the scale of a theorem. Quantum computing has enough fog machines already.

For AI research, the process suggests that formal domains can support unusually strong verification loops. A model can generate an argument, but a proof assistant can reject steps that do not follow. That creates a feedback signal much sharper than a human preference score or a plausible-looking paragraph. The model still may formalize the wrong claim, import a surprising assumption or find a proof no one understands. The checker makes one layer rigorous, not the whole scientific story.

For research institutions, responsibility remains human even when contribution becomes distributed. The PSI report names who scoped and ran the work, who audited it, who commented on formalization and who is conducting external review. That is a useful pattern. Institutions should resist the temptation to assign all credit to the machine when a result succeeds and all blame to a person when it fails. Authorship and accountability need contribution records precise enough to survive both marketing and correction.

For everyone publishing machine-assisted science, the release raises the expected standard of evidence. A consequential claim should travel with source material, machine-readable artifacts, versions, assumptions, checks, named reviewers, known limitations and a correction path. Not every field has a proof kernel. Every field can still publish a receipt that shows what was measured, what was inferred, what was checked and what remains uncertain.

03

WHERE IT COULD HELP

• Publish the exact target statement before the proof. Preserve the original wording, the formal theorem and a plain-language map between them so reviewers can find mismatches.
• Record the research system. Name the model, model version, orchestration, tools, search strategy, run dates, compute limits and any hidden components that prevent reproduction.
• Preserve the run artifacts when policy and privacy allow. Keep prompts, intermediate lemmas, rejected attempts, tool calls and the final packaging step instead of saving only the successful ending.
• Pin the formal environment. Record the Lean version, mathlib commit, dependencies, build commands and hardware or container details needed to reproduce the check.
• Audit the trust boundary. List imported axioms, unsafe features, opaque definitions, generated code, compiler assumptions and any part that a kernel check does not cover.
• Use independent checkers. Re-run the proof with separate kernels or trusted builds and publish the resulting hashes and logs.
• Separate verification roles. Assign reviewers to the formal statement, proof object, mathematical exposition, prior literature, significance claim and reproducibility package.
• Write a human exposition. Identify the central idea, explain why older approaches stalled, show which steps are new and mark where the formal proof is doing work that prose tends to hide.
• Invite adversarial review. Offer a clear channel for counterexamples, statement mismatches, missing citations and build failures, then keep corrections and version history public.
• Carry the receipt into downstream claims. If a paper, lecture, model card or product uses the theorem, link the exact version and distinguish the proved result from broader interpretation.