Logo

Type Theory Forall

Type Theory much beyond inference rules

Episode image

#26 Mechanizing Modern Mathematics

Kevin Buzzard

Apr 11th 2024   |  136 min
0:00
0:00

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

Sponsors

join our discord