Dates &Time:

Apr 18 (Tuesday), 2023 08:00-9:30 PM

Apr 25 (Tuesday), 2023 08:00-9:30 PM

May 2 (Tuesday), 2023 08:00-9:30 PM

Venue:  Zoom Meeting

https://us06web.zoom.us/j/84187405379?pwd=VkREZmdFNysvM01Sa293ei9wejJjQT09

Meeting ID: 841 8740 5379

Passcode: 989564

Abstract: In these lectures, I will give an introduction to interactive theorem proving on a computer using the Lean theorem prover. We will consider how it is even possible to check a proof using a computer. After all, this is quite a different activity than computing thousands of prime numbers or digits of pi. I will demonstrate what it looks like to interactively prove a theorem in Lean.

To get a grip on how Lean works, we will take a little peek under the hood. Lean is built on a foundation of type theory, and I will explain some of the jargon and how to map it to your working knowledge of mathematics. We will also look at some of the available tools for (small scale) proof automation, that help with filling in parts of proofs.

Finally, I will give an overview of the mathematics that has been formalized in Lean, and I will pay particular attention to mathlib, the main mathematical library for Lean.

Parallel to these lectures, interested audience members can practice interactive proofs with Lean using the Natural Number Game (https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) or any of the other learning resources listed on the Lean community

webpage (https://leanprover-community.github.io/learn.html). I will be around to answer any questions about Lean after the lectures.