About this episode

Mike Shulman discusses the intersection of homotopy type theory and computational proof systems.

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.

People in this episode

Hosts: Deniz Sarikaya, Thorsten Altenkirch

Guest: Mike Shulman

Topics covered

• Homotopy Type Theory
• Proof Assistants
• Mathematics
• Computational Proof Systems
• Equality
• Equivalence

Keywords

• Homotopy Type Theory
• Narya
• Proof Assistants
• Mathematics
• Computational Proof Systems
• Equality
• Equivalence

Mentioned in this episode

Organizations: University of San Diego

More episodes of aboutlogic

• aboutlogic #20 | Can AI Prove the Riemann Hypothesis? | Tudor Achim (Harmonic) · September 9, 2026 · 41 min
• aboutlogic: premises #07 | Fixing Russell’s Paradox: The Birth of ZFC & Constructive Set Theory · September 2, 2026 · 30 min
• aboutlogic:premises #06 | What Is a Set? A Beginner’s Guide to Set Theory · August 19, 2026 · 27 min
• aboutlogic #18 | The Hidden History of Logic: Jan von Plato on Gödel, Gentzen & Bernays · August 13, 2026 · 1h 3m
• aboutlogic: premises #05 | Dependent Type Theory: A Revolution in Math & Computer Science · August 5, 2026 · 28 min
• aboutlogic #17 | José Pérez Escobar – Wittgenstein, Turing & the Philosophy of Applied Mathematics · July 29, 2026 · 1h 16m

Explore listener stats, chart rankings, contacts and more on the aboutlogic podcast page.