Abstract

Computational proof assistants now make it possible to carry out mathematical reasoning and argumentation interactively, in a precise, fully verified manner. I will explain why the technology is so useful, not just for establishing correctness, but also for collaboration and discovery.

I will explain why the technology provides a powerful tool for mathematics education. I will also describe some of my experiences using proof assistants in teaching, from graduate students in mathematics and computer science to freshman undergraduates in humanities. Finally, we'll work through one or two examples together, to get a sense of what the experience is like.

Bio

Jeremy Avigad is a Professor of Philosophy and Mathematical Sciences at Carnegie Mellon University, and he is the director of the Hoskinson Center for Formal Mathematics. His research interests include mathematical logic, formal verification, and history and philosophy of mathematics.