How a 20-Person Startup Won Gold at the Math Olympiad—Tying With OpenAI & DeepMind (Tudor Achim, CEO of Harmonic)

"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

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

• Anna Karenina: https://www.amazon.com/Anna-Karenina-Leo-Tolstoy/dp/0143035002

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

• Mathlib: https://lean-lang.org/use-cases/mathlib

• 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

• Go: https://en.wikipedia.org/wiki/Go_(game)

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.

YouTube

Spotify

Apple

Production and marketing by penname.co. For inquiries about sponsoring the podcast, email [email protected].