Formal Methods in Mathematics and the Lean Theorem Prover

In computer science, the phrase "formal methods" is used to describe a body of logic-based methods that are used to specify, develop, and reason about hardware and software systems. These methods can equally well be used to discover and verify mathematical claims, however, and the boundary between mathematical and computational applications is not a sharp one. In this talk, I will survey some of the ways that formal methods have begun to make inroads in ordinary mathematics, and some of the theoretical and practical challenges that arise. 

I will also discuss a new open-source theorem prover, Lean, which is designed to support mathematical reasoning as well as hardware and software verification. I will describe Lean's logical foundations and some of the design decisions that were adopted to meet the challenges of formal reasoning in mathematics.

Reference: The Lean Theorem Prover, http://leanprover.github.io/.