Learning Lean

I'm Learning Lean. Here's how I started.

I decided to learn a bit about Lean. I know a lot more about programming than mathematics; if you are like me, this post might have some value to you. If you're more on the math-focused side of the spectrum, your mileage may vary! There are great Lean introductions out there for both math people and programming people.

This sequence reflects my own favorite way to learn new things. I like to start in an empty-ish sandbox with just a few basic building blocks and create a few simple structures and functions from those primitives. AI agent tutors make this very approach very tractable for almost anything nowadays.

What follows is roughly my own progression into learning the basics of how Lean works.

This exercise has the following goal: after an hour or two of stumbling around, how can I move as quickly as possible toward the concepts I found most interesting or distinctive about Lean, using as few assumptions or givens as possible?

Nat and Prop

Lean doesn't have expressions. You can't type 2 + 2 alone in a REPL, hit enter, and see 4. You have to use "commands" instead.

#eval 2 + 2
  | 4

I learned right away that another important command is #check.

#check Nat
  | Nat : Type
#check Prop
  | Prop : Type

Nat and Prop were the first two types I checked.

I saw that Prop had type Type. So what type does Type have?

#check Type
  | Type : Type 1

This result took me on a brief tangent about Lean's "universes" before I realized I was getting away from my goal of covering basic programming constructs first. We'll put a pin in universes for now.

In short: to run code, use #eval. To check the type of an expression, use #check. That was my first self-contained 5-minute lesson.

Build something small

Lean lets you build new types and specify ways of constructing them using pipe characters. It's called an inductive.

-- Build a compass direction in one of four ways
inductive Direction where
  | north : Direction
  | south : Direction
  | east  : Direction
  | west  : Direction

A Direction is built in exactly one of four ways, and there are exactly four values of the type. To refer to one of them you write Direction.north.

Constructors carry data

A constructor can also take arguments, which lets the value it builds carry information.

-- A shape is either a circle or a rectangle, each carrying its dimensions
inductive Shape where
  | circle    (radius : Nat)        : Shape
  | rectangle (width height : Nat)  : Shape

So circle is a constructor that takes one Nat, a radius, before it will produce a Shape, and rectangle takes two. So Shape.circle 5 is a value, and so is Shape.rectangle 3 4. The arguments in parentheses are the data a constructor needs before it will hand you back a value.

Now we can make sense of a statement like this:

#eval Nat.zero + 1
  | 1

Functions

Check the type Nat → Nat and we'll see functions (arrows!) that take a Nat and produce a Nat.

#check (Nat → Nat)
  | Nat → Nat : Type

The result is Type, the type of functions from Nat to Nat.

#check (fun (n : Nat) => n)
  | fun n => n : Nat → Nat

→ and => are both arrows, but they signify different things. We use → to specify the function as a type, and => when we're writing the function itself, i.e. the function as a value.

The function value, fun n => n, is on the left of the colon, and the function type we saw earlier Nat → Nat is on the right.

We use fun to signify an anonymous function. If we want to name the function and use it later, we use def instead.

Dependent function types

To understand dependent function types and why they're interesting, let's compare them against non-dependent function types to build some contrast.

Nat → Nat is a non-dependent function type. Let's make up a specific function of that type.

def add2 (x : Nat) := x + 2

#eval add2 2
  | 4

Now check it.

#check add2
  | add2 (x : Nat) : Nat

add2 (x : Nat) : Nat is equivalent to Nat → Nat if you squint. When you #check one of our own definitions, Lean expresses the signature the way we originally declared it.

Here is how we can verify that they're equivalent. Put the type we think add2 has on the right of a colon, and #check it.

#check (add2 : Nat → Nat)
  | add2 : Nat → Nat

Try it with a different type on the right of the colon and see what the error says.

#check (add2 : Nat)
  | Type mismatch
  |   add2
  | has type
  |   Nat → Nat
  | but is expected to have type
  |   Nat

Ok, so hopefully it's clear now that our function add2 has type Nat → Nat. It takes a Nat and produces a Nat.

Imagine feeding add2 different inputs. With type Nat → Nat, does the type of the output change depending on which Nat you put in? Nope, it doesn't. No matter what you put in, you get a Nat out.

With this non-dependent function type example in mind, we can drive home the idea of a dependent function type by asking: what if the type of the output did change depending on what you put in?

Types are terms

Consider a function that takes a type as its argument. The result type can then mention that argument.

def pick (t : Type) (x : t) : t := x

In prose, this says: "given a type t, and given a value x of that type t, return x."

Let's go term by term.

def

Define a name.

pick

The name being defined.

(t : Type)

The first argument is called t, and t has type Type. In other words, t is itself a type.

(x : t)

The second argument is called x, and x has type t. So x is a value whose type is whatever t was just handed in as.

: t

The result has type t. Whatever comes back is a value of that same type t.

:= x

The body. It returns x.

In short: we just made a function that hands back whatever you gave it. In math, we call this the identity function.

Check it.

#check pick
  | pick (t : Type) (x : t) : t

This result was a point of confusion for me! When I read that prose description, my programmer's interpretation was: "given a type t, and given a value x of that type t, return x." I thought: "oh, so the function takes two arguments, a type and a value, and returns the value." Not quite so.

Arrows count givens, not returns

In Lean, arrows count the "given"s, not the "return"s. Look at our own sentence and the type side by side.

Each argument the function consumes adds an arrow; the single return is whatever sits after the final arrow.

Lean reads the two parameters as nested functions. It expands to:

def pick : (t : Type) → t → t := fun t => fun x => x

This is currying: a two-argument function is "a function that takes the first argument and returns a function that takes the second."

pick consumes a type and produces a function on that type.

#check (pick : (t : Type) → t → t)
  | pick : (t : Type) → t → t

In short: the result type mentions the argument, so we say it "depends on" the argument. This is a dependent function type. The type of the output depends on the value of the input.

Pi types

One of the first points I read about functions in Lean was the very interesting fact that → (functions) and ∀ (for-all) are the same thing.

∀ x, stuff is just another spelling of (x : t) → stuff. It's the same Lean primitive: the dependent function type.

There are three ways to spell one out.

t → β

This is the bare arrow, used when the result β doesn't mention the argument (the non-dependent case, like add2).

(a : t) → β

The named-binder form is needed when β mentions a (like pick).

∀ a, β

For-all is identical to the named-binder form, just spelled ∀. This form is usually chosen when the result is an interesting proposition about a.

The loose heuristic I figured out was: write → when the argument doesn't appear in the result, write ∀ (or the named arrow) when it does. A statement like "for all n, something-about-n" uses ∀ because the result genuinely depends on n.