MA4N1 Theorem Proving with Lean
Lecturer: Damiano Testa
Term(s): Term 1
Status for Mathematics students: List C
Commitment: 20x1 hour lectures and 9x1 hour tutorials
Assessment: 100% coursework
- Each group submits a plan of how they intend to formalize their project (deadline: during Term 1).
- Each student uploads individually a short video presentation, describing their contribution to the project (deadline: around the end of Term 1).
- Each group submits the final version of their formalization effort (deadline: around end of January).
Formal registration prerequisites: None
Assumed knowledge: You probably already know enough Maths for this module but some experience with programming and debugging will be essential
Useful background:
- MA117: Programming for Scientists
- PH210 Logic II: Metatheory
- MA249 Algebra II: Groups and Rings
- It is highly recommended that you try working your way through the Natural Numbers Game, as this is a great introduction to formalization
Aims: This course provides an introduction to formalization of mathematics using Lean. This involves developing a strong link between the abstract mathematical knowledge on one side and the ability to translate it into a computer-checkable format. The module gives the basic tools needed to structure mathematical thinking in a way that can be effectively formalized and automatically checked. Naturally, there are two separate but interdependent parts: converting mathematical statements into machine verifiable format and extending the software's ability to interpret mathematical language. The former draws more tools from mathematics, the latter draws more tools from computer science
Content: This module will introduce the students to formal proof verification and proof assistants using the program Lean. The module develops tools to understand the interaction between formalizing mathematical results and programming and will contribute to training BSc, MMath and MSc students in skills which are asked for in many areas of research, business, industry and government
Topics from:
- Formalization of mathematics
- Proof verification
- Proof assistant
- Metaprogramming
Objectives: By the end of the module, students should be able to:
- Learn the tactic framework of the computer program Lean for formalizing mathematics
- Learn how to write code to verify mathematical results
- Gain some experience with formal proof checkers
- Gain some experience developing code in a group
Additional Resources