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