Tudor Achim, co-founder and CEO of Harmonic, says the more important milestone for AI in mathematics is not simply generating better answers. It is producing results that can be verified by a machine.
In a recent conversation on The Neuron, Achim described Harmonic’s work on Aristotle, a formal reasoning system designed to create mathematical proofs that computers can check step by step. His broader argument is that AI’s value in advanced math will come from moving beyond impressive-sounding outputs toward claims that can be validated.
That distinction matters because math is one of the few domains where correctness can be tested with precision. Achim framed this as a transition from systems that ask users to trust their output to systems that let users inspect and confirm it.
Harmonic’s pitch is not only about solving famous open problems. Achim also emphasized practical uses for formal verification across fields that rely on mathematical rigor. Those include software, chip design, scientific computing and other areas where errors can carry serious costs.
The company’s Aristotle system is part of a broader effort to make formal math more usable for working researchers and engineers. Achim argued that once formal reasoning becomes easier to apply, it could change how people collaborate, share results and build on one another’s work. He compared the idea to a more structured, verification-focused version of GitHub for mathematics.
The interview also touched on why advanced mathematics matters outside pure theory. According to Achim, breakthroughs in hard math can feed into real-world technologies and improve the tools used to design and verify complex systems.
Achim’s view of AI in mathematics is not that machines will simply displace mathematicians. Instead, he sees AI as a force multiplier that could let researchers explore more ideas, test more paths and formalize more results than they can today.
The conversation explored whether AI could one day make progress on major open problems such as the Riemann hypothesis. Achim suggested that the field is moving toward a point where formal math may become practical enough for AI systems to contribute meaningfully to problems once considered far beyond automation.
He described that shift as a major turning point, suggesting that the ability to generate machine-checkable proofs could be a kind of zero-to-one moment for the discipline.
Even so, Achim did not portray the path as simple. The discussion covered the current limits of scaling math-focused AI, including the need for more compute and better approaches to reasoning. The source material does not indicate that Harmonic has solved those challenges, only that the company sees them as central to the next phase of progress.
The episode also highlighted potential benefits for education and access. If formal reasoning tools become more usable, they could lower barriers for students and researchers who want to work in advanced mathematics without relying solely on manual proof construction.
For Harmonic, the bet is that the future of mathematical AI will be defined less by conversational fluency and more by proof. In Achim’s framing, the real prize is not an AI that merely sounds confident, but one whose reasoning can be checked, shared and trusted.