An AI proof needs more than one kind of verification

On November 6, 2026, PSI reported an Aaronson–Ambainis proof obtained using a non-public Anthropic model. The interesting editorial question is not simply whether AI can produce mathematics, but which parts of that claim outsiders can test.

A result and its production process need different evidence

The public repository provides Lean formalization and recorded checks, while reserving statement correspondence for human review. Open Market Notes has not replayed the proof or reproduced its discovery.

Our assessment is that two apparently competing reactions can both be reasonable. A researcher can regard a publicly inspectable mathematical artifact as valuable while withholding judgment about the system that generated it. Conversely, uncertainty about model access does not itself refute a proof. Confusing these positions turns an assessable scientific object into a vote on a company.

Consider a hypothetical evaluator who receives a final proof file but no record of failed attempts. That evaluator might determine that the file establishes the specified proposition. They could not infer the probability that the model would solve a fresh problem, the amount of human selection involved, or the cost of the unsuccessful searches. Those are different questions, requiring different observations. A successful artifact is not a denominator for a success rate.

The quantum claim has a defined scope

The original paper links the conjecture to classical simulation of most inputs in the query model. This is not a benchmark of a quantum machine.

For a commercial reader, that distinction changes what to ask next. A claim about how many accesses to an input an abstract algorithm needs is not, by itself, a delivery schedule, an energy bill, or an application-level runtime. An operational comparison would require a specified workload, implementation and resource accounting. This article supplies none, so it cannot support a hardware purchasing decision or a forecast of when existing security systems fail.

The useful response is neither to dismiss theory for lacking an immediate product nor to present it as a ready-made engineering result. Theory can change which questions are worth investigating. Engineering must still establish whether the relevant assumptions describe the intended application. A restriction on one class of problems should not be silently promoted into a verdict on every possible use of quantum computation.

Verification is a workflow, not a badge

Lean's documentation distinguishes classical reasoning from computational content. A formal result therefore should not automatically be described as an executable method.

We propose that editorial and research teams maintain separate records for the exact proposition, the version examined, the checks actually performed and the conclusions outside those checks. These are recommendations, not a claim that this newsroom has audited PSI's work. Version identity matters because a review of one file should not become an endorsement of all future revisions. A record should also name the reviewer and say whether the evidence is a publisher's log or an independently repeated run.

The same discipline makes disagreement more useful. If someone disputes a definition, the question is whether the chosen mathematical object captures the intended one. If they dispute a derivation, the question is which step fails. If they dispute the AI capability claim, the relevant evidence concerns task selection, interventions and repeatability. Keeping the dispute at the right level allows a correction in one area without implying that every other claim must collapse.

For institutions considering AI research tools, the purchasing question is consequently broader than the most impressive demonstration. They should define the problems they care about before a trial, record all attempts, account for expert time and specify how outputs will be checked. This is an evaluation design, not an estimate of PSI's performance. It would make a future comparison more informative whether the tool succeeds or fails.

The development deserves attention because a public artifact invites concrete scrutiny. The next useful milestone is an explicit account of what an independent examination establishes, not a stronger adjective in a headline. Until then, mathematical validity, reproducible discovery and practical impact should remain separate judgments.