PSI claims mathematical proof assisted by a non-public Anthropic model
Physical Superintelligence announced a proof of the Aaronson-Ambainis conjecture on 6 November 2026, using a system running a non-public Anthropic model. The lab says the Lean proof assistant accepted its formalization.
The manuscript and code are publicly accessible. The result concerns the number of input queries needed for quantum computation on random inputs; it does not show that quantum computers are useless or lack an advantage on structured problems.
The repository says a human must still check that the formal statement matches the printed conjecture, and that the paper’s text is not machine-checked. David Turturean led and reviewed the work and takes responsibility for it. The model is unnamed; full independent validation and reproducibility of the AI system remain to be established.