"Within 2 or 3 years, AI mathematicians will surpass human mathematicians for any specific mathematical task. I don't think it'll be a decade, like some people say." — Tudor Achim, CEO of Harmonic
Listen or watch now on
YouTube, Spotify, or Apple Podcasts
Tudor Achim is the co-founder and CEO of Harmonic, a startup working to solve one of AI’s hardest problems: mathematical reasoning. In July 2024, Harmonic achieved gold-medal-level performance on International Math Olympiad problems alongside systems from OpenAI and Google DeepMind—but with a key difference: every proof Harmonic submitted was formally verified. Tudor's path to Harmonic wound through competitive piano, computational biology, and autonomous driving. He studied at Carnegie Mellon's music preparatory school, worked on machine learning at Quora, briefly pursued a PhD before dropping out, and then co-founded an autonomous driving company, Helm.ai. Harmonic's core product, Aristotle, uses reinforcement learning and the programming language Lean 4 to solve problems and verify solutions.
In our conversation, we explore:
Why Tudor believes math is the fundamental toolkit to understand the world
How Harmonic uses hallucinations as a feature, not a bug
How Aristotle works and the applications beyond pure mathematics
The reinforcement learning process that lets Harmonic generate synthetic training data and solve problems humans have never attempted
Why Tudor believes AI could surpass human mathematicians on specific tasks within 2–3 years
Why the future of mathematics looks more like GitHub than academic journals
The alternating pattern between intellect leaps and data leaps throughout scientific history
How studying piano under an extraordinary teacher taught Tudor discipline and the value of sticking with hard problems
Thank you to the partners who make this possible
Brex: The intelligent finance platform.
Guru: The AI source of truth for work.
Rippling: Stop wasting time on admin tasks, build your startup faster.
Explore the episode
Timestamps
(00:00) Intro
(03:34) From competitive piano to computer science
(06:28) The mathematical foundations of music (and why Tudor keeps them separate)
(08:24) Can AI ever create art with true intent?
(09:51) Early obsessions
(12:52) Defining intelligence
(14:49) Discovering machine learning’s potential at Quora
(17:30) Why Tudor chose computational biology for his PhD
(19:19) The decision to drop out and build Helm.ai
(22:55) The two breakthroughs that made mathematical AI possible in 2023
(25:28) The importance of Lean 4
(28:21) How Tudor and Vlad Tenev discovered they shared the same impossible dream
(32:35) Why formal verification became the core conviction
(34:21) The timeline for AI surpassing human mathematicians
(35:25) An overview of Aristotle: the world’s first always-correct mathematical agent
(38:12) Why Tudor says hallucinations are the engine of creativity
(39:30) The translation challenge from natural language to formal proof
(40:40) Reinforcement learning
(42:10) Why Aristotle is both faster and cheaper than alternatives
(43:34) Tradeoffs and use cases
(45:34) Math in AI now and what’s next
(47:38) Tying with OpenAI and DeepMind at the International Math Olympiad
(49:08) Democratizing AI and correctness
(53:13) Tudor’s 2030 thesis
(56:02) History’s alternating rhythm of thinking and measuring
(57:53) What Tudor has been wrong about
(58:52) What Tudor’s best at
(1:00:18) Final meditations
Follow Tudor Achim
LinkedIn: https://www.linkedin.com/in/tudorachim
X: https://x.com/tachim/with_replies
Resources and episode mentions
Books
People
Mineko Avery’s obituary: https://obituaries.post-gazette.com/obituary/mineko-avery-1089363974
Stefano Ermon on LinkedIn: https://www.linkedin.com/in/ermon
Vladislav Voroninski on LinkedIn: https://www.linkedin.com/in/vladislav-voroninski-83200213
Leonardo de Moura’s website: https://leodemoura.github.io
Vlad Tenev on LinkedIn: https://www.linkedin.com/in/vlad-tenev-7037591b
Vladimir Novakovski on X: https://x.com/vnovakovski
Terence Tao on LinkedIn: https://www.linkedin.com/in/terence-tao-6291246
Grigori Perelman: https://en.wikipedia.org/wiki/Grigori_Perelman
Other resources
Harmonic: https://www.harmonic.fun
Carnegie Hall: https://www.carnegiehall.org
Carnegie Mellon Music Preparatory School: https://www.cmu.edu/cfa/music/preparatory-summer-programs/index.html
Why A.I. Isn’t Going to Make Art: https://www.newyorker.com/culture/the-weekend-essay/why-ai-isnt-going-to-make-art
Quora: https://www.quora.com
The Unreasonable Effectiveness of Mathematics in the Natural Sciences: https://webhomes.maths.ed.ac.uk/~v1ranick/papers/wigner.pdf
Helm: https://helm.ai
Honda Introduces Next-generation Technologies for Honda 0 Series Models at Honda 0 Tech Meeting 2024: https://global.honda/en/newsroom/news/2024/c241009eng.html
Lean: https://lean-lang.org
Aristotle: https://aristotle.harmonic.fun
Poincaré conjecture: https://en.wikipedia.org/wiki/Poincar%C3%A9_conjecture
OpenAI: https://openai.com
DeepMind: https://deepmind.google
International Mathematical Olympiad (IMO): https://www.imo-official.org
Subscribe to the show
I’d love it if you’d subscribe and share the show. Your support makes all the difference as we try to bring more curious minds into the conversation.
Production and marketing by penname.co. For inquiries about sponsoring the podcast, email [email protected].
