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