PSI is trying to make a business out of AI-driven scientific discovery

PSI used an unreleased Anthropic model to solve an 18-year-old problem in quantum computing, the Aaronson-Ambainis conjecture, by autoformalizing the problem in Lean and using a team of top researchers to explain the solution. The solution provides a negative result, showing that quantum computers cannot solve certain problems at high speed by following a particular avenue. This reflects the growing impact of AI problem-solving in the scientific world, as exemplified by PSI's model which uses specialized model harnesses and scaffolding to tackle complex research problems.