Coming Soon

Interactive Course

Master Lean 4 through hands-on, gamified lessons. Write real proofs, solve puzzles, and level up your theorem-proving skills—all in your browser.

Live Coding

Write and run Lean code directly in your browser

10+ Levels

Progress from basics to advanced theorem proving

Instant Feedback

See proof states update as you type

Explore Language Docs Learn Tactics

theorem coming_soon : 
  ∀ (patience : Prop), 
  patience → 
  ∃ (course : Type), 
  Interactive course := by
  intro h
  use lean4_course
  exact awesome

#check @ComingSoon
-- ComingSoon : 
--   {α : Type} → 
--   Exciting α → 
--   Worth_The_Wait α