A physics laboratory called Physical Superintelligence (PSI) said that they used AI to prove the Aronson-Ambanis conjecture in three days.
This conjecture was proposed in 2008 and asked a very fundamental question: under what conditions can quantum computers be significantly faster than traditional computers. Many people have tried it over the past decade, but there has been no conclusion.
PSI has released the paper and proof code, and the proof has passed Lean’s formal test. Lean is a tool used by mathematicians to let the machine check the proof line by line. If it is passed, it at least means that there are no logical loopholes in the derivation chain.
Stanford scholars who have studied this problem before also read the proof and gave their opinions. However, the independent review by the academic community has not yet been completed, and it is too early to say that it has been "resolved".
About the tools: The system was built by PSI technician David Turturian himself, running on the laboratory's infrastructure, and the bottom layer calls Anthropic's unpublished model. The specific model is not specified.
There has been a lot of news about AI doing mathematics in the past year, mostly competition problems or re-proofs of known conclusions. The difference this time is that it is a real, open research problem with machine-verifiable results.
If the review passes, this will probably be a landmark case of AI participating in theoretical computer science research.