I think the topics of discussion would be of interest to a lot of people here, so I thought I'd share the first episode:
Tanner Duve is a Member of Technical Staff at Logical Intelligence working on formal verification and compilers in Lean, an open-source contributor to Mathlib and CSLib, and a former D1 football player.
I sat down with him for a conversation about his work and his thoughts on the future of AI-assisted math formalization.
Chapters:
00:00 Intro05:12 Social aspect of formal verification07:34 Contributing to mathlib and CSLib15:57 AlgoLean 23:17 What is a Free Monad? 34:27 Turing (in)completeness in Lean 43:13 AI in math formalization 46:22 Where did you learn type theory? 49:49 Lean vs Rocq vs Haskell 51:50 Favorite concept in type theory 55:16 Rust's type theory 56:57 Pedagogy of PL theory 59:52 When did you decide to work in PL theory? 1:02:06 Formal verification pre-AI vs. now 1:05:19 Playing D1 football in college 1:08:16 Veganism 1:12:17 Advice