Formalising Mathematics

A handbook for mathematicians. Written by Bhavik Mehta, for his Formalising Mathematics course, adapted from an earlier handbook by Kevin Buzzard. Thanks to Imperial College London for letting the course happen.

Note

This document is written for people with some mathematical experience (e.g., people in the final year of an undergraduate mathematics degree). Its aim is to show such people how to formalise mathematics in the Lean theorem prover. We make extensive use of Lean’s mathematical library mathlib.

If you’re new here, start at the introduction.

Here’s a link to the repository for this course containing all the code.

Part 1 is a collection of notes on various frequently asked questions that might be helpful for the course.

Part 2 is a list of many basic tactics including documentation and examples.

Contents:

• Introduction
• Installing Lean
• Part 1: Lean tips
• Part 2: Tactics