THE COMPUTABLE SECRETS CLASSROOM · BETA
Make the ideas your own.
Write a little code. Make a conjecture. Build a proof. Learn Lean 4 through small exercises, with feedback as you go.
Start without an account. Your browser keeps your work on this device. Sign in to save it across devices.
START HERE · BETA
Introduction to Lean 4
Programming and theorem proving fundamentals — 70 exercises across 27 units.
02CONTINUE EXPLORING
Natural Number Game
Build ℕ from scratch and prove its basic theory — 78 levels across 9 worlds.
03CONTINUE EXPLORING
Abstract Algebra
Climb the Bourbaki hierarchy — magma to field — proving each level from its axioms.
04CONTINUE EXPLORING
Real Analysis from Scratch
Construct ℚ, then ℝ via Cauchy sequences — no Mathlib — and prove their theory.
Have an idea of your own? Open a Lean project →
Curriculum from Leanlings. Learn at your own pace. Every hint and worked solution is there when you need it.