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.