Lean4
LanguageTactics
Professional Curriculum

Lean 4 Professional Course

A structured, hands-on learning path that blends programming, proof engineering, and practical Lean tooling. Built for a mixed audience of programmers and mathematicians.

Each level combines guided explanation, runnable Lean snippets, and exercises. The first seven levels are the free core curriculum. Levels 8-10 dive into advanced proof patterns and are positioned as premium modules for future monetization.

How to use this course

  • Read the lesson once, then run every code block in your editor.
  • Complete the exercise before moving on (even small ones matter).
  • Use #eval and #check to explore freely.
  • Keep a scratch file for experiments; Lean rewards iteration.

Learning Outcomes

By the end of the core track, you will be able to build Lean programs, model data precisely, and reason about correctness. The premium track adds proof engineering depth and reusable abstraction patterns.

Programming Mastery

  • Write clean functional code using def and recursion.
  • Model domain data with structures, sums, and collections.
  • Build small utilities that compile with lake.

Proof Fundamentals

  • Understand propositions as types and the role of tactics.
  • Prove basic properties with induction and rewriting.
  • Design simple type classes for reusable abstractions.

Course Modules

The course is divided into three free modules plus a premium mastery track.

1

Module 1: Foundations

Set up your Lean environment, learn core syntax, and write your first programs.

2

Module 2: Data & Logic

Model real data and understand Lean's logical foundations without getting lost.

3

Module 3: Proof & Abstraction

Introduce recursion patterns and mental models for proof-driven development.

4

Module 4: Premium Mastery

Deep proof engineering, type class design, and list proofs for real projects.

Premium Track

Premium Mastery Modules

Levels 8-10 are designed to be monetizable in the future. They add advanced proof engineering, deeper Lean abstractions, and capstone-style exercises.

  • Extra exercises with full proof walkthroughs.
  • Reusable proof patterns for lists, trees, and algebra.
  • Type class design patterns used in production Lean projects.
Start Premium Track

Ready to begin?

Start with Level 1 and work sequentially. Each lesson builds on the one before it.

Start Level 1
Hands-on

Every lesson includes runnable Lean code and checkpoints.

Exercises

Short prompts reinforce key ideas without overwhelming you.

Proof Mindset

Learn how Lean encodes logic so you can scale up to mathlib.