Matt Kaufmann (Joint work with Bob Boyer, J Moore, and the ACL2 community)
This is a talk given at JAF (a logic conference, "Weak Arithmetics Days") on May 28, 2019, in New York City.