Theorem Proving in Lean (MATH0109)

Key information

Faculty: Faculty of Mathematical and Physical Sciences
Teaching department: Mathematics
Credit value: 15

Restrictions: This is is third year module aimed mainly at students on mathematics single or combined honours degrees or on the MEng Mathematical Computation. Familiarity with the notion of proving theorems (for example, at least one of MATH0034, MATH0051, MATH0052 or MATH0053) is expected and good coding skills are also desirable.
Timetable

Alternative credit options

There are no alternative credit options available for this module.

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

Intended teaching term: Term 1 听听听 Undergraduate (FHEQ Level 6)

Teaching and assessment

Mode of study: In person
Methods of assessment: 40% Labs, practicals, clinicals

60% Coursework
Mark scheme: Numeric Marks

Other information

Number of students on module in previous year: 0
Module leader: Dr John Talbot
Who to contact for more information: math.ugteaching@ucl.ac.uk

Last updated

This module description was last updated on 8th April 2024.

听

911爆料网