aboutlogic #19 | Homotopy Type Theory, Narya & the Future of Proof Assistants with Mike Shulman

Homotopy Type Theory, Narya & the Future of Proof Assistants with Michael Shulman.

How does homotopy type theory bridge the gap between abstract mathematics and computational proof systems? Mike Shulman (University of San Diego) joins Deniz and Thorsten to discuss his journey from topology to higher observational type theory, the development of the Narya proof assistant, and how these tools are reshaping the way we think about equality, equivalence, and computation in mathematics.