Lean seminar — Mathematics Department

A semester-long working seminar on the Lean 4 theorem prover and its mathematical library, Mathlib. If you want to low-key explore what Lean looks like, check out Kevin Buzzard's Natural Number Game.

Everything the seminar uses is in this repository, and all of it is public. You do not need a GitHub account to read any of it, and you do not need one to take part — an account is only required for the Codespaces fallback described below.

Who this is for

Mathematically-inclined faculty, graduate students, and undergraduates. No prior experience with proof assistants is expected. We assume you can prove things but may have never installed a compiler.

This is a working seminar. The measure of success is that you prove things yourself, not that you follow a talk.

Ways in

	What it costs	What you get
Just read	nothing	Browse the files here. Every session folder has a README explaining what it does.
Web editor (initially)	nothing	live.lean-lang.org runs Lean with Mathlib in a browser tab. No account, nothing saved, and you work one file at a time.
Install locally (eventually)	30–45 min once, ~11 GB	Fast, offline, no quota, your files on your own disk. Nothing to wait for at the start of your work.
Codespaces (backup)	a free GitHub account	Real VS Code in a browser tab. The first launch takes about twenty minutes. For locked-down lab machines, and for anyone whose local install does not work.

The first three sessions need no setup. They are about reading a formal statement and judging whether it says what it claims to say, and a browser tab does that. Week 1's homework is the Natural Number Game, which is also a browser tab.

Eventually we start proving things ourselves, so aim to have a local install working by then. It is the only route with no waiting at startup. Lean reads about 2 GB of compiled library every time it starts cold, which is fast on a local disk and slow on anything in a data center. Install it on whatever machine you will actually use.

Full instructions for every route: handouts/setup-guide.md.

What is in here

Seminar/       one folder per meeting: demo, exercises, solutions, notes
handouts/      the setup guide and other things printed or emailed
MyWork/        yours; ignored by git, so it never conflicts when you pull
scripts/       small utilities (generating no-install links, checking files)

Start at Seminar/README.md for the session index.

Versions

Everything here is pinned to Lean 4.33.0 and Mathlib v4.33.0, and every file states the version it was checked against in its header.

Version drift is a common source of trouble. Mathlib renames lemmas and changes behaviour every few weeks; a file that worked in August fails in November against a different library. The two files that enforce the pin are lean-toolchain and lake-manifest.json, both committed here. Cloning this repository reproduces the exact environment the material was written in.

The practical consequence: do not create your own Lean project for this seminar. VS Code's "Create Project Using Mathlib" fetches whatever Mathlib version is newest on the day you run it, which is how a room ends up with five incompatible environments. Clone this repository instead.

How these files were made

The Lean in this repository was drafted with substantial AI assistance and then compiled — every file, against the pinned toolchain, before it reached anyone. Solutions files contain no sorry; exercise files contain sorry and nothing else unproved. The per-file headers record what each file was checked against.

Two reasons for saying so. The Lean community asks for disclosure of AI assistance. And the distinction is the seminar's own subject: a machine can check that a proof establishes a statement, and cannot check that the statement says what was meant.

See GROUND-RULES.md for what this implies for your own work.

Ground rules

Read GROUND-RULES.md before posting anything to the Lean Zulip. One rule in particular surprises people: asking the community to do your seminar exercises is grounds for suspension there.

Licence

Apache 2.0, the same licence as Mathlib and Mathematics in Lean, so material can move between them without friction. See LICENSE.