About this episode

Deniz and Thorsten discuss the impact of proof assistants like Lean and Agda on mathematics education and the role of AI in formal verification.

Your support helps us keep these conversations going! If you’d like to contribute, you can buy us a coffee here: https://buymeacoffee.com/aboutlogic How do interactive theorem provers like Lean and Agda change the way we teach and do mathematics? In this aboutlogic: premises episode, Deniz and Thorsten discuss the role of proof assistants in education, the differences between Lean and Agda, and how AI is transforming formal verification.

People in this episode

Hosts: Deniz Sarikaya, Thorsten Altenkirch

Topics covered

• interactive theorem provers
• proof assistants
• education
• mathematics
• AI
• formal verification

Keywords

• Lean
• Agda
• proof assistants
• theorem provers
• mathematics education
• AI
• formal verification

Mentioned in this episode

Organizations: AI

Products: Lean, Agda

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 #19 | Homotopy Type Theory, Narya & the Future of Proof Assistants with Mike Shulman · August 26, 2026 · 1h 1m
• 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

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