Abstract:

Since the early twentieth century, it has been understood that mathematical statements can be expressed in formal languages, and mathematical proofs can be represented in formal deductive systems with precise rules and semantics, at least in principle. Remarkably, the development of computational proof assistants over the last few decades has made it possible to do this in practice. The technology is firmly based on the methods and concepts of modern logic, and in many ways the practice represents the contemporary embodiment of the foundational tradition.

In this informal talk, I will provide a brief overview of interactive theorem proving and the body of logic that supports it. I will then discuss a particular theorem prover, Lean, its formal library, mathlib, which are attracting a growing community of mathematical users. The Lean community web pages provide a good starting point for more information: https://leanprover-community.github.io/.