HackerTube / Video
The Future of Mathematics?
Microsoft Research
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.
Recommended as the clearest mathematician's perspective on formal proof assistants and why mathematics should be formalized.
14 Hacker News mentions · 2019–2025