Microsoft Research has just posted a talk by Kevin Buzzard of the Imperial College of London. Don’t worry, no advanced mathematical knowledge is assumed in the talk.

Slides: https://www.microsoft.com/en-us/research/uploads/prod/2019/09/The-Future-of-Mathematics-SLIDES.pdf

From the video description:

As a professor of pure mathematics, my job involves teaching, research, and outreach.

Two years ago I got interested in formal methods, and I learned how to use the Lean theorem prover developed at MSR. Since then I have become absolutely convinced that tools like Lean will play a role in the future of mathematics.