The Future of Mathematics?

Microsoft ResearchLength: 1 hour 14 minutesLogic & formal methods

In brief

Mathematician Kevin Buzzard explains why he believes the Lean theorem prover will shape the future of mathematics, and describes digitizing his university curriculum in Lean with undergraduates, plus the cultural challenges.