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 Intro 05:12 Social aspect of formal verification 07:34 Contributing to mathlib and CSLib 15: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
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 Intro
05:12 Social aspect of formal verification
07:34 Contributing to mathlib and CSLib
15: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