Today we announced live on X that our advanced formal reasoning model Aristotle achieved Gold Medal-level performance at the 2025 International Mathematical Olympiad, widely regarded as the world’s most prestigious mathematics competition. We are releasing Aristotle’s full proofs, which critically did not require human checking since they were formally verified, publicly on Github. This result places Aristotle at the forefront of advanced mathematical reasoning performance among frontier AI models.
As the world is witnessing an explosion in AI-generated content, from news articles to computer code, an unintended side-effect of this has been to turn the people using these AI tools from creators into human verifiers. In technical fields like software engineering, this means engineers spend less time coding and more time confirming the correctness of AI-generated code. We call this the verification problem, and believe it is a major bottleneck in scaling the usefulness of AI tools.
Aristotle overcomes this by design. Every solution it generates is formally verified down to foundational axioms using the Lean4 proof assistant, providing a machine-checkable guarantee of correctness. We’re starting to deploy this technology with mathematics, and we’re already working on expanding support to dependent disciplines such as physics and software engineering.
As an early look into what we expect this new verified AI technology to look like, we are launching Aristotle for iOS in Beta. When someone asks Aristotle a complex question, they not only see the solution in English but also the corresponding Lean code that verifies the correctness. Aristotle for iOS also supports photo-based solving and solving multiple questions in parallel, all with just a couple taps. Users can sign up for our waitlist now, with the rollout already underway.
Press inquiries: pr@harmonic.fun
