Skip to main content Skip to navigation

Module Catalogue

MA4N1-15 Theorem Proving with Lean

Department
Warwick Mathematics Institute
Level
Undergraduate Level 4
Module leader
Damiano Testa
Credit value
15
Module duration
10 weeks
Assessment
100% coursework
Study location
University of Warwick main campus, Coventry

Download as PDF

Introductory description

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.
The module will contribute to training BSc, MMath and MSc students in skills which are asked for in many areas of research, business, industry and government.

Module web page

Module 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.

Outline syllabus

This is an indicative module outline only to give an indication of the sort of topics that may be covered. Actual sessions held may differ.

Topics from:

Formalization of mathematics
Proof verification
Proof assistant
Metaprogramming

Learning outcomes

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.

Research element

The students need to find their own formalization path to verify the proposed goals.

Interdisciplinary

The module sits naturally between mathematics and computer science. One of the eventual goals of the area is to increment automation and bring in also Artificial Intelligence and Machine Learning to help with the formalization of known results and the discovery of new results

Subject specific skills

See learning outcomes

Transferable skills

Students will acquire key reasoning, problem solving skills and programming tools which will empower them to address new problems with confidence. They will also gain experience of collaborating with other in a joint coding project.

Study time

Type Required
Lectures 10 sessions of 2 hours (13%)
Tutorials 9 sessions of 1 hour (6%)
Private study 26 hours (17%)
Assessment 95 hours (63%)
Total 150 hours

Private study description

26 hours to review lectured material and work on set exercises.

Costs

No further costs have been identified for this module.

You do not need to pass all assessment components to pass the module.

Assessment group A
Weighting Study time Eligible for self-certification
Assessment component
Formalization of Mathematics 70% 80 hours No

Make progress in the formalization of some of the topics proposed in the module.
Reassessment component is the same
Assessment component
Presentation 20% 10 hours No

5 minutes pre-recorded presentation
Reassessment component is the same
Assessment component
Project outline 10% 5 hours No

Outline an informal approach to formalizing your group project
Reassessment component is the same
Feedback on assessment

Short report

Courses

This module is Optional for:

  • Year 1 of TMAA-G1P0 Postgraduate Taught Mathematics
  • TMAA-G1PC Postgraduate Taught Mathematics (Diploma plus MSc)
    • Year 1 of G1PC Mathematics (Diploma plus MSc)
    • Year 2 of G1PC Mathematics (Diploma plus MSc)

This module is Option list B for:

  • Year 4 of UCSA-G4G3 Undergraduate Discrete Mathematics
  • Year 5 of UCSA-G4G4 Undergraduate Discrete Mathematics (with Intercalated Year)

This module is Option list C for:

  • UMAA-G105 Undergraduate Master of Mathematics (with Intercalated Year)
    • Year 4 of G105 Mathematics (MMath) with Intercalated Year
    • Year 5 of G105 Mathematics (MMath) with Intercalated Year
  • UMAA-G103 Undergraduate Mathematics (MMath)
    • Year 3 of G103 Mathematics (MMath)
    • Year 4 of G103 Mathematics (MMath)
  • Year 4 of UMAA-G107 Undergraduate Mathematics (MMath) with Study Abroad
  • Year 4 of UMAA-G106 Undergraduate Mathematics (MMath) with Study in Europe