Here’s something you don’t see every day: an AI model that can not only solve elite math competition problems but actually prove it did the work correctly. Harmonic, the AI startup co-founded by Robinhood CEO Vlad Tenev and Tudor Achim, announced on July 28 that its reasoning model Aristotle achieved gold medal-level performance on the 2025 International Mathematical Olympiad.
The model generated formally verified proofs for five out of six IMO problems using the Lean theorem prover. For the uninitiated, that’s not just getting the right answer on a test. It’s showing every single step of your reasoning in a language that a computer can independently check for errors.
Why verified proofs matter more than raw answers
Harmonic’s approach integrates informal reasoning with formal verification through Lean, a theorem-proving language used by professional mathematicians. The Lean prover doesn’t care how smart the reasoning sounds. It either checks out logically or it doesn’t.
Aristotle’s capabilities extend beyond competition math. The model solved a variant of Erdős Problem #124, with verification taking roughly one minute.
