Lean from the Inside
A learning log about how Lean 4 works. I'm writing it to learn Lean properly and to have notes I can come back to. Start with the deep dives in order, or pick up a short log entry when you're curious about one particular detail.
Every code example is checked by Lean when the site builds. Hover over code to explore types and proof states.
Start here
Why I'm writing this introduces the series, the toolchain, and how to read the examples.
Deep dives
-
Foundations: what an inductive type gives you — dependent types, universes,
PropvsType, and recursors. -
Elaboration: from syntax to Expr — metavariables, unification, implicit arguments, instances, and coercions.
-
Tactics: what a tactic proof builds — proof terms, goals, automation, and writing a tactic in
TacticM.
Learning log
rfl proves equations, decide proves decidable propositions — a small experiment in why two ways to close a proof aren't interchangeable.
Up next
These parts are still in progress:
-
Kernel and trust: what the kernel checks, axioms, and the trusted base.
-
Programming: recursion, termination proofs,
donotation, and the compiler. -
Metaprogramming: macros, elaborators, and small embedded languages.