It's Our Mathematics: AI, Verification, and the Future of Math with Jeremy Avigad | AM Podcast #5
Augmented Mind PodcastShow Notes
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: Jeremy’s Homepage: https://www.andrew.cmu.edu/user/avigad/
The Lean Theorem Prover: https://lean-lang.org/papers/system.pdf
Lean projects: https://leanprover-community.github.io/lean_projects.html
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.
More from Augmented Mind Podcast
Geoffrey Litt is a design engineer at Notion. Previously, he was a senior researcher at the independent research lab Ink & Switch, and he got his PhD in HCI at MIT. Geoffrey’s work focuses on malleable software and designing environments for thinking.
Zora Wang is a CS PhD student at Carnegie Mellon University. Zora’s work lies at the intersection of coding agents and human-ai collaboration. In this episode we explore how agents work, how humans work, and how we can get more done together.
Ken Liu is a Stanford CS PhD student and founder of The Open Anonymity Project. Ken’s pioneering work explores the intersection between language models and data & user privacy.
Woosuk Kwon is CTO of Inferact and creator of the vLLM inference library. Woosuk shares what it takes to build the most popular open-source LLM inference engine from a human-centered perspective.
Sherry Wu is a professor at CMU whose research sits at the intersection of human-computer interaction and natural language processing. From making AI work for imperfect humans to making humans work better with AI — Sherry's work challenges us to rethink both sides of the equation.