On November 6, the research group PSI published a proof of the Aaronson-Ambainis conjecture, an 18-year-old open problem in quantum complexity, and the work came from an internal system running non-public Anthropic model instances on PSI hardware.
Scott Aaronson and Andris Ambainis raised the question in 2008, asking if a quantum machine can beat a classical one by an exponential margin on random inputs. If the conjecture is true, the separation is polynomial at most, which is why the result sits near the center of the field’s reasoning.
Lean accepted it, then twice more
Day three of the run yielded a complete proof, and the Lean proof assistant certified it. The system did not stop. It moved to adjacent open problems and rewrote its own theorem twice, and Lean passed the final version.
As stated, the result holds for any degree-d bounded polynomial whose values are nonconstant: at least one of its bits shows influence of c times v to the power 5/2, divided by d to the sixth, and the constant c sits near 0.0025. Earlier results from Lovett, Zhang and Reimer underpin the argument.
What a machine check cannot tell you
Lean confirms a derivation follows from its premises. It cannot confirm the premises prove the theorem someone cared about, or that the theorem matters. PSI reports an internal audit. Independent peer review has not happened.
That gap is the open question in AI mathematics. Formal checking is now cheap enough to certify machine output in bulk, while judging which results deserve attention stays expensive.
Closing an 18-year-old question in three days is a genuine milestone. Deciding whether the proof enters the literature is a separate problem, and no proof assistant solves it.
