Lean crash course

A packaged computational introduction to Lean 4.

This site includes a self-contained snapshot of the Lean crash course on lalten.org. The course adapts the IntroToLean4 examples and places the Lean source beside its observed terminal output.

Open the packaged course in a full page Open the current course on lalten.org

The packaged snapshot covers 14 tutorial chapters. Chapters 1–12 contain executed examples. Chapters 13 and 14 are source-only because those two upstream files did not compile in the source state used to make the course.