Alongside OpenAI and Google DeepMind, AI startup Harmonic has also achieved a gold-medal performance at this year's International Mathematical Olympiad (IMO) 2025 with its model Aristotle. Unlike its competitors, Harmonic is not aiming for AGI, but for what it calls "mathematical superintelligence."
According to Harmonic, Aristotle is the first AI system to formally verify all solutions, eliminating the need for human review. The company has published the complete proofs openly on Github.
While Google DeepMind and OpenAI tackled IMO problems using natural language, Harmonic translated the problems into a formal, machine-readable format and used the Lean4 proof system to check the solutions. The proof chains trace back to mathematical axioms, providing what the company calls a "machine-checkable guarantee of correctness."
Verification, not hallucination
Harmonic presents Aristotle as a solution to a fundamental challenge in modern AI: the verification problem. In many technical fields - such as software development - people now spend more time verifying AI-generated content than creating it, according to Harmonic. By formally verifying results, Aristotle aims to remove this bottleneck and set a new standard for reliability.
Source: Harmonic
"Within the domains that Aristotle supports, which are quantitative reasoning domains, we actually do guarantee that there’s no hallucinations," Harmonic CEO Tudor Achim told TechCrunch. The foundation for this is output in the Lean programming language, which is widely used for verification in safety-critical industries like aviation and medical technology.
Beta app launches, API in the works
Alongside the IMO announcement, Harmonic has launched a beta version of Aristotle for iOS. The app displays both solutions and the corresponding Lean code for complex math problems. Users can scan problems using their phone's camera and solve multiple questions at once. Anyone interested can join the waitlist at aristotle.harmonic.fun. An Android version is also available.
Harmonic says a web app and an API for enterprise use are in development. The long-term goal is to bring Aristotle beyond education into fields like physics, statistics, and computer science.
