"AI may have the answers, but mathematics has the questions."
With all the recent excitement around AI for math, many start to wonder: can mathematics be automated? And what does it mean to learn and understand math?
For EP5, we're thrilled to talk with Prof. Jeremy Avigad, philosopher & mathematician @CarnegieMellon and one of the early forces behind 3w. This episode features rich technical discussions on AI & mathematics, as well as many touching moments where Jeremy shares his vision for the future of mathematicians, math education, and mathematics itself.
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
