An opinionated first tour

Dan Abramov writes the Lean introduction he wishes he'd gotten. Incomplete by admission, possibly wrong in places, but shaped around what actually confused him.

“this is how I wish I was introduced to it, and what I wish was clarified”

Definitions use colon equals

Top-level values look like def name := "Alice" and def age := 42. The := matters: Lean reserves plain = for comparison, the way Go and Pascal do.

“Note you have to write := (assignment) rather than = .”

Types are there even unwritten

Hover over name and you get String. Hover over 42 and you get Nat, a natural number that starts at zero and climbs as high as you want. You can spell types out, or let inference do it.

Nudging inference toward Int

Write -140 and Lean gives you an Int. Want 25 as an Int instead of a Nat? Annotate it as def roomTemperature : Int := 25, or wrap the expression as (25 : Int).

Two ways to use Lean

You can run code, or prove facts about code, or do both in the same file. The primer starts with running, then turns to proving.

“One way to use Lean is to run your code. Another way to use Lean is to prove some facts about your code.”

Eval prints into your editor

Add #eval birthYear and the answer appears on hover and in the InfoView panel. Keep the InfoView open permanently, it is the main feedback loop.

“Lean InfoView is incredibly useful and I suggest to keep it open at all times.”

Main makes it a real program

Define main and run lean, run Scratch.lean to get output in the terminal. Compile to C instead and you can see the literal 1983 baked into the generated function.

A theorem is a def with a goal

theorem my_theorem : age + birthYear = 2025 := by starts a claim. The declared type is the statement, and by drops you into tactic mode to build the proof interactively.

“A theorem is like a def, but aimed specifically at declaring proofs.”

Unfold until it's arithmetic

Each unfold swaps a name for its definition and the goal in the InfoView changes under you. 42 + birthYear, then 42 + (2025 - age), then 42 + (2025 - 42).

“It almost makes you feel like you're the computer, logically transforming the code towards the goal.”

Decide finishes the job

Once the goal is concrete arithmetic, the decide tactic closes it. No code ran. The fact was verified during typechecking, and simp [age, birthYear] does the unfolding for you in one line.

Break the formula, break the proof

Change age to any other number and the proof still holds. Change birthYear to 2023 - age and it stops typechecking. The claim is load-bearing, not decorative.

Namespaces open, sometimes locally

open IO lets you write println instead of IO.println for everything below that line. Add in to scope the shortcut to a single definition rather than the rest of the file.

No parens, no commas

Function calls are f a b c, never f(a, b, c). This is the thing that trips up everyone arriving from JavaScript, and the article says to read it several times.

“I need to emphasize this. No commas and no parens are used for function calls!”

Parens are only for grouping

IO.println 2025 - age parses as (IO.println 2025) - age, and Lean fails hunting for subtraction between IO Unit and Nat. Wrapping (2025 - age) fixes it. Parens group, they don't call.

“something (f x y) a (g z)”

Let bindings, no return

Definitions can't nest, but let breaks a long expression into readable pieces inside one. The last line is the value, so there is no return statement anywhere.

“There is no need for a return statement here.”

A dozen ways to write one function

def birthYear currentYear := ..., the fully annotated version, and several fun forms all produce the same Nat → Nat. The concise form reads best unless you need an anonymous function.

Add an argument, lose inference

Take age as a parameter and Lean gets stuck: it can't run typeclass search for subtraction when it doesn't know either type. The fix is to annotate, as in (currentYear age : Nat).

“typeclass instance is stuck”

Prove it for every input

Copy-pasting theorems for 42, 25 and 77 is just testing. Instead state a + birthYear cy a = cy for unknown cy and a. You get the types, never the values, because a proof covers all of them at once.

“it's a test for all possible inputs of that function that runs during typechecking”

Omega handles the unknowns

decide is a calculator and needs concrete numbers. omega checks equations containing variables, so unfold birthYear followed by omega closes the universal claim.

For all, and what's implicit

∀ cy a moves the arguments inside the proof, introduced later with intro. Braces and brackets in signatures like IO.println's are arguments too, filled in by inference and by typeclass search.

“in Lean generics are just arguments (often implicit)”