Lean 4 as a Programming Language
Learn Lean 4 as a modern, purely functional programming language. No proofs required—just clean, expressive code.
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
Get comfortable with Lean's syntax, basic types, functions, and the interactive environment.
Data Modeling
Structure your data with products, sums, and recursive types. Lean's type system shines here.
Control Flow & Logic
Pattern matching, recursion, higher-order functions, and error handling.
Type Classes
Polymorphism through type classes—similar to Rust traits or Haskell typeclasses.
Effectful Programming
The do notation, IO monad, and mutable state. Practical programming made functional.
Project Engineering
Build real projects with Lake, modules, and compiled binaries.
Ready to begin?
Start with the first lesson to learn about Lean's interactive environment.
Start Module 1