Reading Lean Code | Cryptography Academy

The Basics

Lean code looks like a mix of mathematics and programming. Here's a simple example—a definition of what it means for a natural number to be even:

def isEven (n : Nat) : Prop :=
  ∃ k, n = 2 * k

Let's break this down:

def Introduces a new definition
isEven The name we're defining
(n : Nat) Takes a parameter n of type Nat (natural number)
Prop Returns a proposition (something that can be true or false)
∃ "There exists" — the existential quantifier

Reading tip: Read ∃ k, n = 2 * k as "there exists some k such that n equals 2 times k" — exactly the mathematical definition of even!

Definitions vs Theorems

Lean distinguishes between definitions (what things are) and theorems (facts we can prove about them).

A Definition

-- A group is a structure with an operation and identity
structure Group (G : Type) where
  mul : G → G → G        -- multiplication operation
  one : G                -- identity element
  inv : G → G            -- inverse function
  mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a, mul one a = a
  mul_inv : ∀ a, mul (inv a) a = one

This structure bundles together the data (mul, one, inv) and the axioms (mul_assoc, one_mul, mul_inv) that make something a group.

A Theorem

theorem even_plus_even (m n : Nat)
    (hm : isEven m) (hn : isEven n) : isEven (m + n) := by
  -- proof goes here
  sorry

This says: if m is even (we have proof hm) and n is even (proof hn), then m + n is also even.

Common Symbols

Lean uses Unicode symbols. In the editor, type a backslash followed by the abbreviation—it will autocomplete to the symbol.

Symbol	Type	Name	Meaning
`∀`	`\forall`	For all	"For every..." (universal quantifier)
`∃`	`\exists`	Exists	"There exists..." (existential quantifier)
`→`	`\to` or `\r`	Arrow	Function type or "implies"
`↔`	`\iff`	Iff	"If and only if"
`∧`	`\and`	And	Logical conjunction
`∨`	`\or`	Or	Logical disjunction
`¬`	`\not`	Not	Logical negation
`:=`	`:=`	Defined as	Definition assignment
`by`	`by`	By	Start a tactic proof

Reading a Real Example

Here's an example from our cryptography library—the definition of a commitment scheme:

structure CommitmentScheme (M R C : Type) where
  -- Commit takes a message and randomness, returns a commitment
  commit : M → R → C

  -- Reveal extracts the message
  reveal : C → R → M

  -- Correctness: revealing a commitment returns the original message
  correctness : ∀ (m : M) (r : R),
    reveal (commit m r) r = m

Reading this:

M is the message type
R is the randomness type
C is the commitment type
commit takes a message and randomness, produces a commitment
reveal takes a commitment and randomness, extracts the message
correctness states that the scheme works: revealing always gives back the original

Key insight: The structure bundles the operations (commit, reveal) with the properties (correctness) they must satisfy. This is how we formally specify what a commitment scheme is.

Try It Yourself

Here's a live Lean editor. Try modifying the code and see what happens:

Lean 4Open in new tab ↗

Loading Lean editor...

The Lean server runs remotely. Changes you make are evaluated in real-time.

Next Steps

You can now read basic Lean definitions! Continue to:

Next: Types and Terms →