SMS scnews item created by Catherine Meister at Wed 21 Aug 2024 0838
Type: Seminar
Modified: Wed 28 Aug 2024 0902
Distribution: World
Expiry: 31 Aug 2024
Calendar1: 30 Aug 2024 0900-1100
CalLoc1: SMRI Seminar Room (A12 Room 301)
CalTitle1: Informal Friday Seminar: Narayanan -- Lean times
Auth: cmeister@w95s10l3.staff.sydney.edu.au (cmei0631) in SMS-SAML

Informal Friday Seminar: Narayanan -- Learning to lean on Lean!

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.


Actions:
ball Calendar (ICS file) download, for import into your favourite calendar application
ball UNCLUTTER for printing
ball AUTHENTICATE to mark the scnews item as read
School members may try to .