![Type Theory Forall artwork](https://is5-ssl.mzstatic.com/image/thumb/Podcasts124/v4/ed/de/43/edde43db-febe-b892-3a30-358ebe2e2c07/mza_16532267942080647912.png/100x100bb.jpg)
#26 Mechanizing Modern Mathematics - Kevin Buzzard
Type Theory Forall
English - January 16, 2023 20:30 - 2 hours - 125 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #25 Formally Verifying the Tezos Codebase - Formal Land
Next Episode: #27 Formalizing an OS: The seL4 - Gerwin Klein
Kevin Buzzard has been very passionate spreading the word among
mathematicians to use theorem provers mechanize theorems of modern
mathematics. In this conversation we will talk about his vision in teaching
undergrads to use the Lean theorem prover, what is the Xena Project, his view
of how theorem provers can change the way we do mathematics, and much more!
Links
Xena's Project Twitter
Xena Project's Website
Lean's Website