Harmonic is taking a different route through the race for stronger AI systems. Its model Aristotle has reached a gold-medal performance at the International Mathematical Olympiad (IMO) 2025, alongside OpenAI and Google DeepMind, but the startup’s focus is not AGI. Harmonic says it is building toward “mathematical superintelligence,” with verification at the center of the product.
A gold-medal result with a different method
OpenAI and Google DeepMind approached the IMO problems using natural language. Harmonic used another path: it translated the problems into a formal, machine-readable format and checked the resulting solutions with the Lean4 proof system.
That distinction matters because Harmonic is not only presenting Aristotle as a model that can solve difficult math problems. It is presenting the system as one that can prove its work in a way a machine can inspect. According to Harmonic, Aristotle is the first AI system to formally verify all solutions, which the company says removes the need for human review.
The company has published the complete proofs openly on Github. Those proof chains trace back to mathematical axioms, giving what Harmonic calls a “machine-checkable guarantee of correctness.”
Why verification is the core claim
Harmonic frames Aristotle as a response to what it calls the verification problem in AI. In many technical fields, including software development, the company says people now spend more time checking AI-generated content than creating it.
That bottleneck is familiar in any workflow where a plausible answer is not enough. If an AI system produces code, calculations, or a technical argument, someone still has to confirm that the result is correct. Harmonic’s pitch is that formal verification can move that burden away from manual review, at least in the quantitative reasoning domains Aristotle supports.
“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 basis for that claim is output in the Lean programming language. The source article describes Lean as widely used for verification in safety-critical industries like aviation and medical technology. In Aristotle’s case, Lean code is not an extra explanation beside the answer; it is the mechanism that allows the answer to be checked.
From math contest problems to user-facing tools
Harmonic announced more than the IMO result. The startup has launched a beta version of Aristotle for iOS, and an Android version is also available. The app is designed around complex math problems and shows both the solution and the corresponding Lean code.
Users can scan problems with a phone camera and solve multiple questions at once. Anyone interested can join the waitlist at aristotle.harmonic.fun.
The product direction is clear from the features Harmonic is already showing:
- Problem scanning through a phone camera.
- Solutions for complex math problems.
- Lean code shown alongside the answer.
- Support for solving multiple questions at once.
- Availability through iOS beta and Android.
For students or technical users, the important difference is that the answer is paired with formal output. That makes Aristotle less like a conventional chatbot response and more like a system built to show how its result can be verified.
The enterprise path
Harmonic says a web app and an API for enterprise use are in development. That future API is important because the company is not limiting its ambitions to education. Its longer-term goal is to bring Aristotle into fields such as physics, statistics, and computer science.
Those areas fit the same broad pattern described in the source: quantitative reasoning domains where correctness is central. The article does not claim Aristotle already supports every such use case. It says Harmonic’s goal is to move beyond education and into those fields over time.
This is also where the contrast with general AI becomes sharper. Harmonic is not trying to market Aristotle as a universal assistant. It is narrowing the problem to domains where machine-checkable reasoning can be the standard, and where hallucinations are especially costly because the output must stand up to technical scrutiny.
What the Aristotle approach signals
The broader significance of Aristotle is not only that an AI system performed at a gold-medal level on IMO 2025 problems. The more consequential claim is that its results can be formally verified. If the main limit on AI adoption in technical work is the time humans spend checking outputs, then a system that can package answers with formal proofs changes the workflow.
That does not make Aristotle a general solution to every AI reliability issue. Harmonic’s own framing is domain-specific: quantitative reasoning, Lean output, and proof chains that can be checked. Within that scope, the company is arguing for a different standard of trust.
For AI users, the practical question is whether future systems will merely generate more content or also make that content easier to verify. Harmonic’s answer is Aristotle: a model built around mathematical superintelligence, formal verification, and machine-checkable correctness.