It's Our Mathematics: AI, Verification, and the Future of Math with Jeremy Avigad | AM Podcast #5

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.