What happened
Physics research company PSI announced that its research system proved the Aaronson-Ambainis conjecture, first proposed in 2008, in three days. According to the company, the system ran a non-public Anthropic model on its own infrastructure, and the resulting proof was accepted by Lean, a proof-assistant software that checks the logical correctness of formal mathematical arguments. The system then improved the proof twice, with Lean accepting the final version as well.
What the conjecture asks
The Aaronson-Ambainis conjecture concerns whether quantum algorithms with a particular mathematical structure can be efficiently approximated by classical computers. If the conjecture holds, classical machines could simulate a broad class of quantum algorithms on randomly selected inputs with only polynomial overhead. That would help explain why some quantum algorithms may not deliver an exponential advantage; it does not rule out purpose-built methods such as Shor's algorithm for factoring large numbers.
Not yet settled
PSI said David Turturean led the work, Jim Halverson audited the proof and Phiala Shanahan commented on its Lean formalisation. Researchers at Stanford University, including Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, are also examining the result; the group previously proved a special case of the conjecture in August 2026 and is preparing a shorter exposition of PSI's full proof. Lean checks whether a formal proof follows logically from its stated assumptions, but experts must also assess whether the formalised statement accurately captures the original conjecture. PSI, which launched publicly in September 2026, describes itself as a physics research company building automated systems for scientific discovery.
