An unreleased Anthropic model proved an 18-year-old quantum conjecture

Physical Superintelligence announced on November 6 that its internal research system, running instances of a non-public Anthropic model, found a proof of the Aaronson-Ambainis conjecture — open since 2008 and counted among quantum computing's central open problems, the question of when quantum computers can be exponentially faster than ordinary ones.

The system had a complete proof by the third day of the run, and Lean, a proof assistant that machine-checks every step, accepted it. PSI then set the system on related open problems, improved the result twice, and got Lean's sign-off on the final version. The manuscript and the full Lean formalization are public, and the Stanford researchers who proved a special case of the conjecture in August are now reading the proof and writing a shorter exposition for experts.

The catch is in the fine print: the proof has not been peer reviewed, and a human still has to confirm the formal statement in Lean matches the conjecture as Aaronson and Ambainis meant it. PSI staffer David Turturean built the system, scoped the problem, and is named as responsible for the paper's correctness — the AI wrote the first draft and the formalization, a person owns the claim.