Formal Methods in Mathematics and the Lean Theorem Prover
Jeremy Avigad ( CMU )
-
11:00 27th July 2017 ( Trinity Term 2017 )051
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/.