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.
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.