Physical Superintelligence (PSI), an AI science startup, has announced that an internally developed research system running a non-public Anthropic model produced a proof of the Aaronson–Ambainis conjecture, a question that has been open since 2008.
According to the company, the system produced a complete proof on the third day of its run and the proof was accepted by Lean, a proof assistant that checks every step formally. PSI then tasked the system with related open problems; during this process the system reportedly improved the result twice and Lean accepted the final version as well.
Background
The Aaronson–Ambainis conjecture, posed by Scott Aaronson and Andris Ambainis in 2008, concerns the circumstances under which quantum computers can achieve exponential speedups over classical computers. PSI states that its research system found a proof settling this long-standing question, and that the proof was formally verified in Lean.
The announcement is based on the company’s own report: the specific Anthropic model used is not public, and PSI’s statement does not include independent external verification beyond the Lean acceptance claimed by the company.
Why this matters
If the reported proof is validated through independent peer review and broader scrutiny, it would represent a significant theoretical advance in understanding the limits of quantum computation. Beyond the mathematical result, the event exemplifies a broader trend where automated or semi-automated AI systems contribute to extending scientific knowledge. PSI frames this development as an illustration of what some describe as the early stages of a technological “singularity,” where the pace of scientific and technological progress outstrips humans’ ability to immediately assimilate it.
Next steps
PSI says it is applying the system to other related open problems. The customary next steps for the scientific community are transparent publication of the proof, independent verification, and peer review to confirm the correctness and implications of the claimed result.
