Got me to go back and re-watch Kevin Buzzard's talk at MS Research in re: Lean, "The Future of Mathematics?"
https://www.youtube.com/watch?v=Dp-mQ3HxgDE
https://news.ycombinator.com/item?id=21200721