# Introduction to Lean: Formalizing Mathematics with Mathlib

Course material for the summer school **"Proof assistants and applications"**,
IRMA, Université de Strasbourg, **31 August – 4 September 2026**.

Xavier Roblot (Université Claude Bernard Lyon I).

## Getting started

The easiest way is **GitHub Codespaces** — nothing to install:

[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://codespaces.new/xroblot/Strasbourg2026)

Use **Firefox**, **Chrome** or **Edge** (Safari is not recommended), and allow
about **5 minutes** for the first load. Then open `Part1.lean`.

See [`References.md`](./References.md) for the full instructions, including a
local installation as an alternative, and for links to further resources.

## Contents

| File | |
|---|---|
| `Part1.lean` | **First lecture** — first steps, propositions and proofs, quantifiers, sets and functions. Also holds the keyboard shortcuts, the tour of the Lean syntax and the notes on how to work on these files. |
| `Part2.lean` | **Second lecture** — algebraic structures, analysis and topology, and how to search Mathlib. |
| `Part3.lean` | **Practical session** — two more ambitious proofs: the construction of ℤ from ℕ × ℕ, and the Schröder–Bernstein theorem. |
| `References.md` | Setup instructions and pointers to books, tools and the community. |
| `abstract.md` | Abstract of the course. |

The solutions are in the `Solutions/` directory, one file per worksheet.