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.
Outline:
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:
Podcast Links:
Podcast website: https://augmented-mind.github.io/
Apple Podcasts: https://podcasts.apple.com/us/podcast/augmented-mind-podcast/id1868102170
Spotify: https://open.spotify.com/show/40KculkYTe2tOpqJm6TAYr?si=PU_UncsMT4mXjVNCRwoXog&nd=1&dlsi=6d9bed7a43d64085
RSS: https://anchor.fm/s/10dbf5b7c/podcast/rss
Special Thanks to Zixiao Jolene Wang and Rajarshi Mukherjee for their help with this episode!
About the Hosts:
The AM Podcast is hosted by Yijia Shao, Shannon Shen, and Michael Ryan, CS PhD students at Stanford University and MIT.
