Jeremy Avigad is a professor in the Department of Philosophy and the Department of Mathematical Sciences at Carnegie Mellon University. Jeremy is a pioneer in using AI for Mathematics and the co-creator of the Lean Theorem Prover. Currently, he is the director of the Hoskinson Center for Formal Mathematics at CMU, Dean’s Chair in Logic and Philosophy of Mathematics, and the director of the newly-established Institute for Computer-Aided Reasoning in Mathematics under NSF.
Timestamps
- 0:00 — Teaser
- 1:04 — Monologue
- 2:50 — The Historical Landscape of AI for Mathematics
- 7:28 — Formalization and Computer-Aided Proof
- 11:56 — The Birth of the Lean Project
- 21:21 — Lean Blueprint, Model Training with Lean, Using Lean in Agentic Systems
- 29:48 — Making AI Actually Useful for Mathematicians
- 32:46 — How AI is Changing Mathematics
- 36:29 — “It’s Our Mathematics, and Us Doing Mathematics”
- 43:04 — The Verification Gap in Human-AI Collaboration
- 47:46 — The Future of Math Education
- 52:23 — Capital, Startups, and the Mathematicians’ Ecosystem
- 1:01:08 — Predictions
References
Acknowledgments
Special thanks to Zixiao Jolene Wang and Rajarshi Mukherjee for their help with this episode!
Subscribe and follow us for more episodes!