Kevin Buzzard and Alex Kontorovich on the Future of Formal Mathematics(renaissancephilanthropy.org)

https://www.renaissancephilanthropy.org/news-and-insights/kevin-buzzard-and-alex-kontorovich-on-the-future-of-formal-mathematics-a-mathlib-initiative-interview