Great talk by Kevin Buzzard on teaching to undergraduates, formalizing the undergraduate curriculum, marketing theorem provers to professional mathematicians and the ultimate goal of creating a formalized database of mathematical proofs: youtube.com/watch?v=Dp-mQ3
Conversation
Having a look back at github.com/leanprover-com and I must say it looks quite impressive! Also check out github.com/leanprover-com for some 'trendy maths' which uses mathlib as a foundation.
