Introduction

Why Lean?

Lean is a programming language and interactive theorem prover. It is used by mathematicians to write machine-verified proofs and by programmers who want the strongest possible guarantees about their code.

  • Functional at its core — Lean is a pure functional language with algebraic data types, pattern matching, and higher-order functions.
  • Types as propositions — In Lean, types and logical propositions are the same thing. A function that returns a proof is just a function.
  • Mathlib — The Lean community has formalized over 1,000,000 lines of mathematics. Real analysis, number theory, algebraic geometry — all machine-verified.
  • Used in industry — AWS uses Lean to verify the Cedar authorization language. Lean is increasingly used to verify critical software.

What You Will Learn

This course contains 15 lessons organized into 4 chapters:

  1. Foundations — The basics: output, numbers, strings, booleans, and named definitions.
  2. Functions — Defining functions, multiple parameters, conditionals, and recursion.
  3. Lists & Pattern Matching — Working with lists and matching on structure.
  4. Functional Programming — Lambdas, map, filter, and foldl.

Each lesson introduces a concept, shows an example, and gives you a hands-on exercise.

Let's get started.

Next →