Lean Academy Lean book Try Lean online

Learn Lean 4 · for total beginners

Lean Academy

Brother Lemma teaches you Lean, one small step at a time, using Age of Empires II units.

Age of Empires II © Microsoft Corporation. Lean Academy was created under Microsoft’s “Game Content Usage Rules” using assets from Age of Empires II, and it is not endorsed by or affiliated with Microsoft.

Free, non-commercial fan project: no ads, no sales. Unit sprites and icons are Age of Empires II artwork, sourced from community sites; every source is listed in ASSETS.md. Age of Empires is a trademark of Microsoft. Lean 4 v4.35.0, core only (no Mathlib). Fonts: Cinzel, EB Garamond, JetBrains Mono (SIL OFL). Every Lean snippet and every error message in the lessons comes from the real Lean compiler (aoe2-lean/AoE2/Tutorial.lean).