The AI Trying to Solve Math’s Biggest Mystery w/ Tudor Achim of Harmonic

What happens when AI stops simply giving answers and starts producing proofs a computer can verify?

In this episode of The Neuron, Corey Noles and Grant Harvey talk with Tudor Achim, Co-Founder and CEO of Harmonic, the company behind Aristotle — a formal reasoning system built to generate machine-checkable mathematical proofs. Tudor explains why math may be the clearest test case for moving AI from “trust me” to “check me,” and why formal verification could matter far beyond Olympiad benchmarks.

They discuss what “mathematical superintelligence” actually means, why Tudor thinks solving a Millennium Prize problem would be a meaningful threshold, and how Lean-based proofs could change the way mathematicians collaborate. They also explore Aristotle’s real-world use cases, from open math problems to verified software, chip design, scientific computing, and the future of AI-assisted discovery.

Plus: why Tudor thinks formal math has reached a “zero to one” moment, why specs may be the bottleneck in verified software, and why humans still need to direct the questions AI systems try to solve.

Subscribe to The Neuron and sign up for The Neuron Daily at theneuron.ai.