SMS scnews item created by Catherine Meister at Mon 5 Aug 2024 1338
Type: Seminar
Modified: Mon 5 Aug 2024 1558; Mon 12 Aug 2024 1054; Wed 21 Aug 2024 0834; Wed 21 Aug 2024 0837
Distribution: World
Expiry: 31 Aug 2024
Calendar1: 23 Aug 2024 0900-1100
CalLoc1: SMRI Seminar Room (A12 Room 301)
CalTitle1: Lean times: TBA
Auth: cmeister@167-179-157-30.a7b39d.syd.nbn.aussiebb.net (cmei0631) in SMS-SAML

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.