Description
Lean is a programming language that can be used to interactively prove mathematical theorems. More precisely, when one types a proof into lean, the computer checks that the proof is correct. Furthermore, when one has typed part of a proof, the computer determines at any stage what we have proved so far, and what is still to be proved. Lean also has various high level commands which can be used to prove simple statements automatically. One very appealing feature of Lean for mathematicians is the existence of a large and growing library of formalised mathematics: https://leanprover-community.github.io/mathlib-overview.html The ultimate goal of this course is to provide students with a level of proficiency in Lean that will allow them to formalise (i.e. prove in lean) theorems of undergraduate level pure mathematics.
Module deliveries for 2024/25 academic year
Last updated
This module description was last updated on 19th August 2024.
Ìý