Basics

True to the title of this article series, we start from zero. Not “Hello, World!” but an actual zero: the natural number that forms the foundation of arithmetic.

Zero

-- From Zero to QED: let's start at the very beginning
def zero : Nat := 0

#eval zero  -- Output: 0

-- The natural numbers are defined inductively:
-- Nat.zero is the base case
-- Nat.succ n is the successor of n
def one : Nat := Nat.succ Nat.zero
def two : Nat := Nat.succ (Nat.succ Nat.zero)

#eval one   -- Output: 1
#eval two   -- Output: 2

-- Of course, we can just write the literals directly
def fortyTwo : Nat := 42

-- The answer to life, the universe, and everything
theorem deep_thought : fortyTwo = 6 * 7 := rfl

This first example introduces three toplevel declarations that you will use constantly:

• def defines a named value or function. Here def zero : Nat := 0 declares that zero has type Nat (natural number) and equals 0. Every Lean program is built from def declarations.

• #eval evaluates an expression and prints the result. This command runs code immediately, useful for testing as you work. Commands starting with # are interactive queries that do not create permanent definitions.

• theorem declares a proposition to be proved. The name deep_thought labels the statement fortyTwo = 6 * 7, and rfl (reflexivity) proves it by computation: both sides reduce to 42. Unlike def, theorem proofs are opaque and never unfold during type checking.

The natural numbers are perhaps the most fundamental type in mathematics and programming. Lean represents them inductively: zero is the base case, and every other natural number is the successor of another. This simple construction gives us the entire infinite sequence 0, 1, 2, 3, and so on.

Natural Numbers

Natural numbers in Lean represent non-negative integers, defined inductively just as Peano intended in 1889. They support standard arithmetic operations, but subtraction truncates at zero since negative results would fall outside the type. This has caused approximately as many bugs as unsigned integers in C, which is to say: more than anyone wants to admit.

-- Natural numbers (Nat) are non-negative integers: 0, 1, 2, 3, ...
def myNat : Nat := 42
def anotherNat : Nat := 100

-- Basic arithmetic
#eval 3 + 5      -- 8
#eval 10 - 3     -- 7 (truncated subtraction: 3 - 10 = 0)
#eval 4 * 7      -- 28
#eval 17 / 5     -- 3 (integer division)
#eval 17 % 5     -- 2 (modulo)

-- Natural number subtraction truncates at zero
#eval 3 - 10  -- 0, not -7

-- Comparison returns Bool
#eval 5 < 10     -- true
#eval 5 ≤ 5      -- true
#eval 10 == 10   -- true

Lean has two equality operators. The == operator is decidable equality, returning a Bool for use in programs. The = operator is propositional equality, returning a Prop for use in proofs. For runtime computation, use ==. For stating theorems, use =. Both work with #eval because Lean can decide equality for natural numbers.

Integers

When you need negative numbers, use Int. Integer arithmetic behaves as you would expect from standard mathematics, unburdened by the horrors of two’s complement overflow that have plagued systems programmers since the PDP-11.

-- Integers (Int) include negative numbers
def myInt : Int := -17
def posInt : Int := 42

-- Integer arithmetic handles negatives properly
-- Starting with a negative infers Int automatically
#eval -5 + 3     -- -2
#eval -4 * -3    -- 12
#eval -17 / 5    -- -3
#eval -17 % 5    -- -2
-- But positive minus larger needs annotation
#eval (3 : Int) - 10     -- -7

-- Converting between Nat and Int
#eval Int.ofNat 42             -- 42 as Int
#eval (42 : Int).toNat         -- 42 as Nat
#eval (-5 : Int).toNat         -- 0 (negative becomes 0)
#eval (42 : Int).natAbs        -- 42 (absolute value as Nat)
#eval (-42 : Int).natAbs       -- 42

Modules and Namespaces

Lean organizes code into modules and namespaces. This section covers the practical syntax; we revisit the underlying mechanics in Type Theory.

Files and Modules. Each .lean file defines a module. The file Foo/Bar/Baz.lean defines module Foo.Bar.Baz. To use definitions from another module, import it at the top of your file with import Mathlib.Data.Nat.Prime or import Mathlib for an entire library. Imports are transitive: if A imports B and B imports C, then A has access to C’s definitions. The Lake build system (covered in Build System) manages dependencies and ensures modules are compiled in the correct order.

Namespaces. Namespaces group related definitions under a common prefix. They prevent name collisions and organize large codebases:

namespace Geometry2
  structure Point2 where
    x : Float
    y : Float

  def theOrigin : Point2 := ⟨0.0, 0.0⟩

  def dist (p q : Point2) : Float :=
    let dx := p.x - q.x
    let dy := p.y - q.y
    Float.sqrt (dx * dx + dy * dy)
end Geometry2

-- Access with full path
#eval Geometry2.dist Geometry2.theOrigin ⟨3.0, 4.0⟩  -- 5.0

The angle brackets ⟨ and ⟩ are shorthand for structure constructors. These two lines are equivalent:

def explicit : Point2 := Point2.mk 3.0 4.0
def shorthand : Point2 := ⟨3.0, 4.0⟩

The open command brings namespace contents into scope, so you can write dist instead of Geometry2.dist:

-- Open brings namespace contents into scope
open Geometry2 in
#eval dist theOrigin ⟨3.0, 4.0⟩  -- 5.0

-- Open for a definition
open Geometry2 in
def unitCirclePoint (θ : Float) : Point2 := ⟨Float.cos θ, Float.sin θ⟩

Sections and Variables. The section command creates a scope for temporary declarations. Variables declared with variable inside a section are automatically added as parameters to definitions that use them:

section VectorOps
  variable (α : Type) [Add α] [Mul α]

  -- α and the instances are automatically added as implicit parameters
  def doubleIt (x : α) : α := x + x
  def squareIt (x : α) : α := x * x
end VectorOps

#eval doubleIt Nat 21    -- 42
#eval squareIt Nat 7     -- 49

The bracket notation deserves explanation. Round brackets mark explicit arguments you pass directly. Square brackets mark instance arguments that Lean finds automatically through type class resolution. Here, [Add α] means the type must have an Add instance, which provides the + operator. Curly braces mark implicit arguments that Lean infers from context.

Visibility. By default, all definitions are public. Mark definitions as private to hide them outside the current file:

namespace Internal
  private def helperVal : Nat := 42

  def publicApi : Nat := helperVal * 2
end Internal

#eval Internal.publicApi          -- 84
-- helperVal is not accessible outside this file

Export. The export command re-exports definitions from one namespace into another, making them available without opening the original:

namespace Math
  def square (x : Nat) : Nat := x * x
  def cube (x : Nat) : Nat := x * x * x
end Math

namespace Prelude
  -- Re-export square from Math into Prelude
  export Math (square)
end Prelude

-- Now square is available via Prelude without opening Math
#eval Prelude.square 5  -- 25

Functions

Functions are first-class values in Lean. You can define them in multiple ways and partially apply them to create new functions.

def add (x : Nat) (y : Nat) : Nat :=
  x + y

def double : Nat → Nat :=
  fun x => 2 * x

def addFive := add 5  -- Partially applied function

#eval add 3 4        -- Output: 7
#eval double 21      -- Output: 42
#eval addFive 10     -- Output: 15

When declaring multiple parameters of the same type, you can group them: (x y z : Nat) is identical to (x : Nat) (y : Nat) (z : Nat). Use whichever reads better.

Pattern Matching

Pattern matching is a powerful feature for destructuring data and defining functions by cases.

def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

def describe : Nat → String
  | 0 => "zero"
  | 1 => "one"
  | 2 => "two"
  | n => s!"many ({n})"

#eval factorial 5    -- Output: 120
#eval describe 0     -- Output: "zero"
#eval describe 100   -- Output: "many (100)"

The factorial definition uses n + 1 rather than the seemingly more natural | n => n * factorial (n - 1). This is not a style choice. Lean must verify that recursive calls terminate, and it does this by checking that arguments decrease structurally. The pattern n + 1 desugars to Nat.succ n, explicitly matching a successor. When you recurse on n, Lean sees that n is structurally smaller than Nat.succ n. With | n => ... factorial (n - 1), Lean cannot immediately see that n - 1 is smaller than n (subtraction is a function, not a constructor), so termination checking fails.

The describe function uses string interpolation with s!"many ({n})". The s! prefix enables interpolation: expressions inside {...} are evaluated and converted to strings. Without the prefix, curly braces are literal characters.

More Declarations

Abbreviations are transparent definitions that unfold automatically during elaboration. Use them for type aliases:

-- abbrev creates a transparent abbreviation (always unfolded)
abbrev NatPair := Nat × Nat
abbrev Predicate' (α : Type) := α → Bool

def isEvenPred : Predicate' Nat := fun n => n % 2 == 0
def sumPair (p : NatPair) : Nat := p.1 + p.2

#eval isEvenPred 4       -- true
#eval sumPair (3, 7)     -- 10

The interactive commands #check, #print, and #reduce help you explore code:

-- #check shows the type of an expression
#check (fun x : Nat => x + 1)  -- Nat → Nat
#check @List.map              -- shows full polymorphic type

-- #print shows information about a declaration
#print Nat.add
#print List

-- #reduce reduces an expression to normal form
#reduce (fun x => x + 1) 5    -- 6
#reduce List.map (· + 1) [1, 2, 3]  -- [2, 3, 4]

A complete reference of all declarations appears at the end of this chapter. Advanced declarations like axiom, opaque, universe, notation, and set_option are covered in later chapters where they arise naturally.

Functional Programming Essentials

Lean is a functional language. Functions compose, pipelines chain, and higher-order functions do the heavy lifting.

Composition combines functions right-to-left: (f ∘ g) x means f (g x). Pipelines chain left-to-right: x |> f |> g means g (f x). Both express the same computation; choose whichever reads better.

Higher-order functions take functions as arguments. The classics: map transforms each element, filter keeps elements matching a predicate, foldl reduces a list to a single value by accumulating from the left. In foldl (· + ·) 100 [1,2,3,4,5], the 100 is the initial accumulator; the function adds each element in turn, producing 115.

And because Lean is also a theorem prover, we can prove properties by computation. The theorem add_comm_example states that 2 + 3 = 3 + 2, and rfl proves it because both sides reduce to 5. The examples at the end go further: reversing a list twice returns the original, list lengths add correctly, mapping a function produces the expected result.

What is the difference between #eval [1,2,3].reverse.reverse = [1,2,3] and example : [1,2,3].reverse.reverse = [1,2,3] := rfl? The #eval runs at runtime and prints true. The example is verified at compile time by the type checker, and if the equality did not hold, compilation would fail. Both check the same fact, but example catches the error before you ship. Note that this rfl proof verifies this specific list; proving it for all lists requires a theorem with induction. We cover proofs properly in Proofs.

-- Function composition: (f ∘ g) x = f (g x)
def twice (n : Nat) := n * 2
def square (n : Nat) := n * n

#eval (square ∘ twice) 3           -- 36: square(twice(3))
#eval (twice ∘ square) 3           -- 18: twice(square(3))

-- Pipelines: x |> f |> g = g (f x)
#eval 5 |> twice |> square         -- 100
#eval [1, 2, 3] |> List.map twice  -- [2, 4, 6]

-- Higher-order functions
#eval [1, 2, 3, 4, 5].map (· * 2)         -- [2, 4, 6, 8, 10]
#eval [1, 2, 3, 4, 5].filter (· > 2)      -- [3, 4, 5]
#eval [1, 2, 3, 4, 5].foldl (· + ·) 100   -- 115 (100 + 1 + 2 + 3 + 4 + 5)

-- Programs are proofs: addition is commutative
theorem add_comm_example : 2 + 3 = 3 + 2 := rfl

-- Computation IS proof: complex operations verified by evaluation
example : [1, 2, 3].reverse.reverse = [1, 2, 3] := rfl
example : [1, 2, 3].length + [4, 5].length = 5 := rfl
example : [1, 2, 3].map (· + 10) = [11, 12, 13] := rfl

Toplevel Declarations Reference

You do not need to memorize all of this. This section is a reference for every toplevel declaration in Lean, with links to where each is explained in later chapters. Skim it now, come back when you need it.

Every Lean file is a sequence of toplevel declarations. These are the building blocks of every program and proof.

Definitions and Proofs:

Type Declarations:

Organization:

Interactive Commands:

The distinction between def and theorem matters for performance. Lean marks theorem proofs as opaque, meaning they are never unfolded during type checking. This keeps proof terms from bloating computations. Use def for values you need to compute with and theorem for propositions you need to prove.

From Values to Structure

You now have the building blocks: numbers, functions, modules, and the fundamental declarations. Next we cover the data structures that make programs useful: lists, arrays, maps, and user-defined types. After that, we explore control flow, polymorphism, effects, and IO. By the end of Arc I, you will have built a D&D character generator, which is either a useful demonstration of structured programming or an excuse to start a D&D campaign. Possibly both.