Module 1 · Lesson 1

The Environment

Lean 4 is a compiled language with a uniquely interactive development experience. Before writing your first program, let's understand the tools you'll use every day.

Setting Up

You do not install Lean directly. You install elan, a version manager that downloads the right Lean toolchain per project — the same idea as rustup or nvm. This matters because Lean and Mathlib move fast, and every project pins its own version.

Easiest path: install the Lean 4 extension in VS Code. If no toolchain is found it offers to install elanfor you, and gives you a "New Project" command.
Command line: on macOS/Linux run the elan install script from https://github.com/leanprover/elan; on Windows use winget install Lean.Elan or the same script under Git Bash.
Nothing to install: the Lean 4 Web Editor runs Lean (with Mathlib) in your browser. Every snippet on this site can be pasted straight into it.

bash

1# Check what you have
2elan --version
3lean --version
4
5# Create a new project (Lake is Lean's build tool)
6lake new myproject          # plain project
7lake new myproject math     # project with Mathlib preconfigured
8
9cd myproject
10lake build                  # build it
11lake exe myproject          # run the executable, if there is one

⚠

Open the project folder in your editor, not a single .lean file in isolation. The Lean extension finds the toolchain and dependencies by looking for lean-toolchain and lakefile.tomlat the workspace root. "Unknown identifier" errors on library names are almost always this mistake.

Interactive Evaluation with #eval

Unlike traditional compiled languages where you write code, compile, and run, Lean provides immediate feedback through the #eval command. This evaluates expressions directly in your editor and shows the result.

lean

1-- Evaluate simple expressions
2#eval 1 + 1           -- Output: 2
3#eval "Hello" ++ "!"  -- Output: "Hello!"
4#eval 2 ^ 10          -- Output: 1024
5
6-- Evaluate function calls
7#eval String.length "Lean 4"  -- Output: 6
8#eval List.reverse [1, 2, 3]  -- Output: [3, 2, 1]

The result appears in your editor's "Lean Infoview" panel (in VS Code) or inline as a comment. This makes exploration and learning incredibly fast—you never need to leave your editor.

Type Inspection with #check

While #eval runs code, #checkreveals types. This is essential for understanding what you're working with.

lean

1#check "Hello World"   -- String
2#check 42              -- Nat
3#check true            -- Bool
4#check [1, 2, 3]       -- List Nat
5
6-- Check function types
7#check String.length   -- String.length (b : String) : Nat
8#check List.reverse    -- List.reverse.{u} {α : Type u} (as : List α) : List α

ℹ

#check prints the full signature, including implicit arguments in braces and universe parameters after the dot (.{u}). You can ignore the universe part for now — it is Lean's way of saying "this works for types at any size level". Prefix a name with @ to see it in pure arrow form: #check @List.reverse.

Notice the arrow →in function types. This reads as "takes X and returns Y." For example, String → Natmeans "a function that takes a String and returns a Nat."

Key Takeaway

#eval executes code and shows results. #checkshows the type without executing. Use both constantly as you learn—they're your primary debugging tools.

The Infoview Panel

In VS Code with the Lean 4 extension, the Infoview panel is your companion. It shows:

Results from #eval and #check
Type information when you hover over expressions
Error messages with detailed explanations
Goal state when writing proofs (covered in Tactics)

💡

Position your cursor on any expression and the Infoview will show its type. This is faster than writing #check everywhere.

Other Useful Commands

Beyond #eval and #check, Lean offers additional introspection tools that help you understand existing definitions.

lean

1-- Print the definition of something
2#print Nat.add
3
4-- Reduce an expression using the logical definition
5#reduce 2 + 2        -- 4
6
7-- Assert something at compile time (fails the build if false)
8#guard 1 + 1 == 2
9
10-- Which axioms does this proof ultimately rely on?
11theorem two_eq : 1 + 1 = 2 := rfl
12#print axioms two_eq   -- 'two_eq' does not depend on any axioms
13
14-- sorry: an admitted proof. Compiles, but taints everything downstream.
15example : 1 = 1 := by sorry   -- warning: declaration uses 'sorry'

💡

#print axioms is your safety net. If a theorem you rely on secretly used sorry, this is how you find out — the output will list sorryAx. Run it on your top-level results before you trust them.

Searching for Lemmas

You will spend more time looking for existing lemmas than writing new ones. Lean and Mathlib give you several ways to search, all better than guessing names:

lean

1-- exact? : "find me a single lemma that closes this goal"
2example (n : Nat) : n + 0 = n := by exact?
3
4-- apply? : "find me a lemma whose conclusion matches, leave the rest as goals"
5example (n : Nat) : 0 ≤ n := by apply?
6
7-- Autocomplete-by-namespace: type the type's name and a dot, then Ctrl+Space
8-- Nat.  → shows everything in the Nat namespace
9
10-- With Mathlib, exact? and apply? search the whole library.
11-- Outside a proof, the website https://loogle.lean-lang.org lets you search
12-- by shape, e.g.  |- _ + 0 = _   or   Nat.succ, _ + _

#eval vs #reduce

Both commands evaluate expressions, but they work differently:

	#eval	#reduce
How it works	Runs the compiled implementation in an interpreter	Unfolds the logical definition, the way the kernel would
Arithmetic	Uses GMP bignums — `2 ^ 100` is instant	Unary `Nat.succ` — `2 ^ 100` will never finish
IO operations	Can run IO	Cannot run IO
Sees through	`@[implemented_by]`, `partial`, native code	Nothing — only the definition Lean actually reasons about
Use case	Day-to-day coding and testing	Understanding why a proof by `rfl` does or doesn't work

lean

1-- #eval: fast, practical
2#eval 2 ^ 100    -- 1267650600228229401496703205376, instantly
3
4-- #reduce: shows how the definition unfolds
5#reduce 2 + 2    -- 4
6
7-- ...but do NOT try this — it reduces Nat unarily and hangs:
8-- #reduce 2 ^ 100
9
10-- #eval can do IO
11#eval IO.println "Hello"  -- Prints to the infoview
12
13-- #reduce cannot
14-- #reduce IO.println "Hello"  -- Meaningless: IO has no logical reduction

⚠

The important difference is not speed, it is trust. #eval runs the efficient implementation Lean compiles — which for Nat is GMP arithmetic, not the inductive definition. So #eval is a great debugger but is not evidence about what the kernel will accept in a proof. If #eval e says true but example : e = true := rfl times out, #reduce will usually show you why.

Understanding Error Messages

Lean's error messages are detailed and helpful. Here's how to read them:

lean

1-- Type mismatch example
2def badAdd : Nat := "hello"
3-- Error: Type mismatch
4--   "hello"
5-- has type
6--   String
7-- but is expected to have type
8--   Nat

Error messages typically show: what you provided (in this case "hello"), its type (String), and what was expected (Nat).

lean

1-- Unknown identifier
2#eval unknownFunction 5
3-- Error: unknown identifier 'unknownFunction'
4
5-- A numeric literal in a place that wants a String
6#eval String.length 42
7-- Error: failed to synthesize instance of type class
8--   OfNat String 42
9-- numerals are polymorphic in Lean, but the numeral `42` cannot be used
10-- in a context where the expected type is String

ℹ

That second error is worth decoding, because you will see its shape constantly. Lean did not say "42 is a Nat, you need a String" — it said it could not find an OfNat String 42 instance. Numeric literals in Lean are polymorphic: 42means "whatever the expected type's OfNatinstance says 42 is". When the expected type has no such instance, you get this message instead of a plain type mismatch. Read failed to synthesize C Xas "X does not support C".

Key Takeaway

When you see an error, focus on: (1) the expected type, (2) the actual type, and (3) where the mismatch occurred. Lean's precision helps you fix issues quickly.

Practice the Loop

The fastest way to learn Lean is a tight feedback loop: write a line, check a type, evaluate a value, and adjust. This exercise builds that habit.

Exercise: Inspect and Evaluate

Use #check and #eval on the same definition, then explain why the outputs are different.

lean

1def greeting := "Hello, Lean!"
2
3#check greeting
4#eval greeting

Deep Dive: Compiled vs Interpreted

When you run a Lean program as an executable, it compiles to efficient C code and then to native machine code. However, #eval runs in an interpreter for immediate feedback.

This means #eval is great for learning and debugging, but performance-critical code should be tested with actual compilation usinglake build.

Your First File

Create a file called Hello.lean and add:

lean|Hello.lean

1-- My first Lean file
2#eval "Hello, Lean 4!"
3
4-- Check some types
5#check Nat
6#check String → Bool
7
8-- A simple definition (we'll cover this next)
9def greeting := "Welcome to Lean!"

Save the file and watch the Infoview update. You should see "Hello, Lean 4!" appear as the result of the #eval.

Module 1: Foundations

Next: Primitives & Basic Types