Episode
The AI Trying to Solve Math’s Biggest Mystery w/ Tudor Achim of Harmonic
- Podcast
- The Neuron: AI Explained
- Published
- May 20, 2026
- Duration seconds
- 2794
- Processing state
not_requested
Actions
POST https://stenobird.com/v1/public/podcasts/the-neuron-ai-explained-6886341/episodes/the-ai-trying-to-solve-math-s-biggest-mystery-w-tudor-achim-of-harmonic/transcription-requests
Idempotently request low-priority transcript generation for this episode.GET https://stenobird.com/podcast/the-neuron-ai-explained-6886341/the-ai-trying-to-solve-math-s-biggest-mystery-w-tudor-achim-of-harmonic.md
Read the agent-friendly Markdown representation of this episode resource.
Summary
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.