What Is an Interactive Theorem Prover? | Kevin Buzzard

ABSTRACT I will give a live demo of how to use the Lean interactive theorem prover, and discuss uses, and potential future uses, of such tools in teaching, research, and communication of mathematics. LECTURER Kevin Buzzard is Professor of Pure Mathematics at the Imperial College, London. His expertise is in algebraic number theory and he is currently working in the area of formal proof verification.