The Lean Programming Language and Theorem Prover

Slides and code for the ETAPS 2026 tutorial on Lean.

Overview

A 90-minute tutorial introducing Lean to PL/FM researchers. The tutorial walks through MiniRadix, a simplified verified DSL built layer by layer, teaching Lean concepts along the way.

MiniRadix is a simplified version of Radix, a verified DSL built entirely by AI agents in a single weekend (52 theorems, 0 sorry).

Structure

• Slides.lean -- Verso slide deck
• MiniRadix/ -- verified DSL (~950 lines, 0 sorry)
  • AST.lean -- types, values, expressions, statements
  • Syntax.lean -- [RExpr|...] and [RStmt|...] macros
  • Eval.lean -- environment and expression evaluation
  • BigStep.lean -- relational big-step semantics (7 rules)
  • Interp.lean -- fuel-based interpreter
  • Opt/ConstFold.lean -- constant folding with type-guarded identity rules
  • Proofs/ConstFoldCorrect.lean -- constant folding preserves semantics
  • Proofs/InterpCorrectness.lean -- interpreter soundness, completeness, fuel monotonicity
  • Examples.lean -- factorial, fibonacci, sum with #guard assertions

Prerequisites

Install elan:

curl https://elan.lean-lang.org/install.sh -sSf | sh

elan will automatically download the correct Lean toolchain when you build.

Building

Build everything:

lake build

Generating Slides

Generate the HTML slide deck:

lake build && lake exe etaps-tutorial

The slides are written to _slides/index.html. To view them locally:

python3 -m http.server 9090 --directory _slides

Then open http://localhost:9090.

License

Apache 2.0