Lean 4 as a Programming Language
Lean 4 as a programming language: types, data, control flow, effects and projects, with no theorem proving required.
This guide covers Lean 4 from the perspective of a software engineer. You will learn syntax, data structures, control flow, and how to build real applications. The theorem proving aspects are covered separately in the Tactics section.
Modules
Foundations
Lean's syntax, basic types and functions, and the interactive environment.
Data Modeling
Structures, inductive types, recursive data, and the standard collections.
Control Flow & Logic
Pattern matching, recursion, higher-order functions, and error handling.
Type Classes
Polymorphism through type classes, which work much like Rust traits or Haskell type classes.
Effectful Programming
do notation, the IO monad, and mutable state.
Project Engineering
Lake projects, modules, and compiled executables.
Ready to begin?
Start with the first lesson to learn about Lean's interactive environment.
Start Module 1