A Course in Lean 4 at Stanford University

In Spring 2025, I’m teaching Stanford’s CS 99: Functional Programming and Theorem Proving in Lean 4. You can preview the course here. As far as I know this is the first type theory and proof assistant course at Stanford.

Slide Example

Course Design Rationale

The learning objective of the course is to get a systematic understanding of Lean 4. Rather than introducing the tactic proof system directly as like Mathematics in Lean 4, I elected to first introduce the functional programming system. This makes it natural to transition to proofs in lecture 6, following the historic development path of mathematics. Without functional programming I can’t teach the metaprogramming system anyways, so it makes sense for it to be the first.

The course is partially inspired by Dr. Jeremy Avigad’s Course at CMU.

Exam

The exam will be done on paper to prevent the abuse of LLM assistants and cheating, but more importantly we can ask type inference questions on the exam.

Lecture Infrastructure

The course’s lecture slides along with its website are written in Svelte (with SvelteKit) and RevealJS. A skeleton project can be found here. I had to customize some features in RevealJS in order for the visualizations to work.

Overall, writing lecture slides in HTML is much more pleasant than LaTeX. Several inherent problems exist in LaTeX’s compilation system and the PDF format:

Almost no interactivity
No transition animation
Long compilation time
Difficult to get fragile content (e.g. code annotation) to work with beamer

Grading Infrastructure

Thanks to Lean’s expressive metaprogramming system, automatic grading with scripts is very easy. In fact, the script can be fine-tuned to allow/disallow imports, unsafe functions, constant usage, etc.

I may write more details here when I have interesting details to share.

Why is it called The Perfect Math Class

Besides obvious reasons that subscriber to this blog will know, the reason its called perfect is not that the user can prove any statement they want, but rather the software can check for errors and ensure existing proofs are watertight.