What's Next?

Congratulations

You have completed all 15 lessons. You now know the core of Lean 4 as a functional programming language: definitions, functions, recursion, pattern matching, and higher-order functions.

What to Explore Next

• Theorem proving — Lean's real superpower. Start with the Natural Number Game to learn tactic-based proving interactively.
• Dependent types — Types that depend on values. Vector Nat n is a list of exactly n elements, verified at compile time.
• Mathlib — The world's largest library of formalized mathematics. Contribute a proof.

References

• Lean 4 Documentation — Official language reference.
• Functional Programming in Lean — Free book, covers Lean as a programming language.
• Mathematics in Lean — Free book, the bridge from programming to formal proofs.
• Natural Number Game — The best hands-on introduction to Lean proofs.
• Mathlib4 — 1M+ lines of formalized mathematics.