THE HOOK
A research system running a hidden Anthropic model just turned an 18-year-old quantum conjecture into a theorem, and a computer checked every step.
THE GIST
Physical Superintelligence says its internal research system, running instances of a non-public Anthropic model, found a complete proof of the Aaronson-Ambainis conjecture on day three of a run. Lean accepted the proof, then two later improvements. The result, open since 2008, says quantum computers cannot be exponentially faster on random yes-or-no inputs.
THE TAKE
This is the rare AI-for-science claim that comes with a machine-checked proof, not a press-kit vibe. Credit the system, not a chatbot demo: PSI built the harness and Lean did the auditing. The catch is you cannot inspect the model that found it. A theorem with a black-box co-author is still a theorem — and a new kind of credit problem.
OPINION
Stanford's Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who had proved a special case in August, called it a huge result that 'resolves a decades-old conjecture' and are writing a shorter exposition, according to PSI. The Lean formalization is public on GitHub, which is the part anyone can actually check. Peer review still has not happened, so treat the implication as strong and the social process as unfinished.
- Story type: Important story
- Impact: High
- Confidence: High (official announcement)
- Audience: Researchers
- What changed: PSI's research system, using a non-public Anthropic model, produced a Lean-accepted proof of the Aaronson-Ambainis conjecture.
- What to watch: Independent expert write-ups and whether the Lean formalization survives outside scrutiny.
- Reading time: 2 minute(s)
