Informal Friday Seminar: Narayanan -- Informal Friday Seminar: Narayanan -- Lean times:

Title: Learning to lean on Lean! 

Speaker: Ashvni Narayanan (SMRI) 

Abstract: In these talks, I will introduce the theorem prover Lean.  Lean is used to
formally verify mathematics, that is, use a computer to check that the mathematics we do
is accurate.  Lean uses dependent type theory as its foundation (instead of set theory),
thus making it a little different from the general paper mathematics we know and love.
We will learn to code basic theorems and their proofs in Lean.  We should also be able
to read theorems present in mathlib, the mathematical library of Lean.  

Some more information on Lean and mathlib for the interested reader: Lean community.  

https://leanprover-community.github.io/ 

If you enjoy challenges and would like to be introduced to new ways of thinking about
the mathematics we do, this is your opportunity! 

Note: This is meant to be a hands-on lecture, where the audience works on Lean on their
laptops, and I will be around to guide.  Thus, the experience will be much better if
each attendee comes with a laptop and a pre-installed version of Lean 4 (installation
instructions are here: Get started with Lean).  

https://leanprover-community.github.io/get_started.html 

If you have trouble with installation, feel free to reach out to me via email, or come
have a chat with me (I sit in L447, SMRI)! We can also have an “installation party”
next week (say 3 pm on Tuesday 20th August), please email me if you would like to join.