Why Lean 4 Matters

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.

—

Transcript: https://www.generalist.com/p/how-a-20-person-startup-won-gold

—

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: https://www.generalist.com/p/how-a-20-person-startup-won-gold⁠

—

Production and marketing by penname.co. For inquiries about sponsoring the podcast, email jordan@penname.co.