Minicourse Series for Lean 4

Introduction

This repo is originally served as notes for Lean 4 minicourse series taught by me in Dept of Math @ NUS. The objective for this series is to get students handed on with Lean 4 and start to formalize things of their interests in fastest possible time. For this purpose, unlike Mathematics in Lean, the design of learning process is more 'practical' rather than 'structured'. For example, I will not avoid powerful tactics for high-level automation in the first place. And theorems and lemmas will be introduced progressively and more based on their day-to-day frequency.

This course also featuring various LLM tools, such as LeanSearch, Auto-formalizer, and step-prover. I will try my best to combine these tools in my teaching.

Outline

• Chapter 1: Introduction and Basic Syntax
• Chapter 2: Useful Tactics
• Chapter 3: Structures and Organizations
• Problems: High-school Level Problems to be solved in Lean

References

Here are some references that I will use in this course:

• Mathematics in Lean
• Theorem Proving in Lean
• Lean for Curious Mathematicians 2023

Installation

To install Lean 4, you can follow the official instructions here.

Since the course mainly relies on Mathlib4, you are recommended to initialize your project from this manual.

Links

More projects from NUS-Math-Formalization group:

• Calculus Game
• CS1231 Game
• The Coxeter Project