The Lean Programming Language and Theorem Prover

Leo de Moura
Senior Principal Applied Scientist, AWS
Chief Architect, Lean FRO
ETAPS | April 13, 2026
Lean

Last Month, Something Unexpected Happened

A general-purpose AI, with no special training for theorem proving, converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct.

Not tested. Proved. For every possible input. lean-zip

"This was not expected to be possible yet."

How? Let me show you.

Lean

What is Lean?

  • A programming language and a proof assistant

  • Same language for code and proofs. No translation layer.

  • Small trusted kernel. Proofs can be exported and independently checked.

  • Lean is implemented in Lean. Very extensible.

  • The math community made Lean their own: >50,000 lines of extensions.

def reverse : List α → List α | [] => [] | x :: xs => reverse xs ++ [x] theorem reverse_append (xs ys : List α) : reverse (xs ++ ys) = reverse ys ++ reverse xs := by induction xs with | nil => simp [reverse] | cons x xs ih => simp [reverse, ih] #eval reverse [1, 2, 3]
[3, 2, 1]
Lean

Propositions as Types

def odd (n : Nat) : Prop := ∃ k, n = 2 * k + 1

  • The type of odd 3 is Prop, a statement that can be true or false.

  • We can't evaluate it: odd returns a Prop, not a Bool.

  • But we can prove it by providing a witness.

example : odd 3 := ⟨1, by decide⟩
Lean

Theorem Proving Is a Game

"You have written my favorite computer game" — Kevin Buzzard

The "game board": you see goals and hypotheses, then apply "moves" (tactics).

theorem square_of_odd_is_odd : odd n → odd (n * n) := by intro ⟨k₁, e₁⟩ simp [e₁, odd] exists 2 * k₁ * k₁ + 2 * k₁ grind

Each tactic transforms the goal until nothing remains. The kernel checks the final proof term.

Lean

The Kernel Catches Mistakes

example : odd 3 := ⟨2, by decide⟩

You don't need to trust me, or my automation. You only need to trust the small kernel.

An incorrect proof is rejected immediately.

Lean has multiple independent kernels.

You can build your own and submit it to arena.lean-lang.org.

Lean

Success Stories: Mathlib

  • 200,000+ theorems. 750+ contributors.

  • From basic algebra to modern research mathematics.

  • The dataset every AI math system trains on.

Mathlib dependency graph

Lean

Success Stories: Mathematics

Six Fields Medalists engaged: Tao, Scholze, Viazovska, Gowers, Hairer, Freedman.

Lean

The Liquid Tensor Experiment

In 2020, Peter Scholze posed a formalization challenge.

"I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. I still have some small lingering doubts." — Peter Scholze

Johan Commelin led a team that verified the proof, with only minor corrections.

They verified and simplified it without fully understanding the proof. Lean was a guide.

"The Lean Proof Assistant was really that: an assistant in navigating through the thick jungle that this proof is." — Peter Scholze

Nature article on LTE

Lean

Cedar (AWS)

"We've found Lean to be a great tool for verified software development." — Emina Torlak

Cedar QED comparison

Lean

SymCrypt (Microsoft)

SymCrypt verification with Aeneas

Lean

Veil: Verified Distributed Protocols

  • Built on Lean by Ilya Sergey's group.

  • Combines model checking with full formal proof.

  • Found an inconsistency in a prior formal verification of Rabia consensus that went undetected across two separate tools.

Veil code

Lean

Success Stories: AI

To date, every AI system that solved IMO problems with formal proofs used Lean.

  • AlphaProof (Google DeepMind) — silver medal, IMO 2024

  • Aristotle (Harmonic) — gold medal, IMO 2025

  • SEED Prover (ByteDance) — silver medal, IMO 2025

Three independent teams. No competing platform was used by any of them.

Lean

AI Scoreboard

  • Axiom: 12/12 on Putnam 2025.

  • DeepSeek Prover-V2: 88.9% on MiniF2F-test. Open-source, 671B parameters.

  • Harmonic: Built the Aristotle AI — gold medal, IMO 2025

None of these systems existed in early 2024.

Startups using Lean

Lean

The Kernel as AI Safety Infrastructure

"It's really important with these formal proof assistants that there are no backdoors or exploits you can use to somehow get your certified proof without actually proving it, because reinforcement learning is just so good at finding these backdoors." — Terence Tao

The kernel's soundness is not just a theoretical property. It is AI safety infrastructure.

RL agents will find every shortcut. The kernel is the one thing they can't fake.

Who Watches the Provers? | Comparator | Validating a Lean Proof

Lean

Radix: 10 AI Agents, One Weekend

10 AI agents built a verified embedded DSL with proved optimizations in a single weekend.

  • Zero sorry — 52 theorems, all complete

  • 5 verified compiler optimizations

  • Determinism, type safety, memory safety — all proved

  • Interpreter correctness — sound and complete

  • 27 modules, ~7,400 lines of Lean

  • I did not touch the code. Zero lines. Full agent autonomy.

github.com/leodemoura/RadixExperiment

Today we'll build a simplified version of Radix together.

Lean

Do We Still Need Proof Automation?

"I thought AI would prove all theorems for us now."

  • When grind closes a goal in one step instead of fifty, the AI's search tree shrinks.

  • Compact proofs = better training data = better AI provers.

  • grind is a new tactic inspired by SMT solvers: congruence closure, E-matching, linear arithmetic — all cooperating.

40 lines replaced by one grind call

Lean

What is grind?

New proof automation (since Lean v4.22), developed by Kim Morrison and me.

A proof-automation tactic inspired by modern SMT solvers. Think of it as a virtual whiteboard:

  • Discovers new equalities, inequalities, etc.

  • Writes facts on the board and merges equivalent terms

  • Multiple engines cooperate on the same workspace

Cooperating Engines:

  • Congruence closure; E-matching; Constraint propagation; Guided case analysis

  • Satellite theory solvers (linear integer arithmetic, commutative rings, linear arithmetic, AC)

Supports dependent types, type-class system, and dependent pattern matching

Produces ordinary Lean proof terms for every fact.

Lean

Tao on grind

Tao on Grind

"I have been experimenting recently with the new tactic grind in Lean, which is a powerful tool inspired by 'good old-fashioned AI' such as satisfiability modulo theories (SMT) solvers... When I apply grind to a given subgoal, it can report a success within seconds... But, importantly, when this does not work, I quickly get a grind failed message."

Lean

How Does AI Affect Proof Automation?

  • I built heuristics for Z3: quantifier instantiation, case-split ordering, proof search.

  • AI can do this better. AI replaces the heuristics.

  • The algorithmic core (congruence closure, linear arithmetic, decision procedures) is more valuable than ever.

  • grind is designed this way: strong algorithms, AI-replaceable search.

example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := by grind => use [trig_identity] ring
Lean

The Ecosystem

Lean

elan: The Lean Toolchain Manager

  • Manages Lean versions (like rustup for Rust or ghcup for Haskell)

  • lean-toolchain file pins the version per project

  • Installation: curl https://elan.lean-lang.org/install.sh -sSf | sh

  • Each project can use a different Lean version. elan switches automatically.

Lean

Lake: The Lean Build System

  • Lakefile is written in Lean. Build configuration is a Lean program. Manual

  • Dependency management from Git repos.

  • lake new creates an initial Lean package in a new directory.

  • lake build compiles everything.

  • lake exe <name> looks for the executable target exe-target in the workspace, builds it if it is out of date, and then runs it with the given args in Lake's environment.

import Lake open System Lake DSL require «verso-slides» from git "https://github.com/leanprover/verso-slides.git"@"main" package «etaps-tutorial» where version := v!"0.1.0" lean_lib MiniRadix lean_lib Slides @[default_target] lean_exe «etaps-tutorial» where root := `Main
Lean

VS Code Extension

  • Real-time feedback: errors, goals, and hints as you type.

  • Goal state panel: see what you need to prove at each tactic step.

  • Hover information: types, docstrings, source locations.

  • Go to definition. Find references. Code actions.

  • 200,000+ installs.

Lean IDE with Claude Code

The IDE is where you collaborate with AI now.

Lean

VS Code Extension

I asked Claude to prove append_length. It wrote the proof, Lean checked it. No goals remaining.

Claude proves append length

Lean

Lean Zulip: The Community Hub

  • leanprover.zulipchat.com

  • Active community of mathematicians, CS researchers, and engineers.

  • Streams: #general, #new members, #mathlib, #lean4

  • Best place to ask questions and get help.

  • Searchable archive — many common questions already answered.

Lean

Learning Resources

Lean

Loogle: Search for Lean Theorems

  • loogle.lean-lang.org

  • Search by type signature: List.map (_ ++ _) finds relevant lemmas

  • Indispensable for finding theorems in Mathlib's 200,000+ entries

  • Also available as a Zulip bot: just type #loogle followed by your query

Lean

Verso: Written in Lean. Checked by Lean.

  • Future math papers will have Lean code that is checked.

  • Lecture notes, papers, and slides — all in one tool.

  • These slides are written in Verso.

  • lean-lang.org is written in Verso.

  • Pure Lean. Built by David Thrane Christiansen (Lean FRO).

Verso: source and rendered output

Lean

Verso Blueprint: A Map for Large Formalizations

  • Large projects like FLT (50+ contributors) and sphere packing need more than proofs. They need a map.

  • Tracks definitions, lemmas, and dependencies.

  • The blueprint is a Lean document with inline code that is type-checked.

  • When AI generates 200,000+ lines of formalization, humans need tools to visualize and understand what was built.

  • Pure Lean. Built by Emilio Jesús Gallego Arias (Lean FRO).

  • Emilio ported: FLT, Carleson, Sphere Packing, Noperthedron.

  • Released this week.

verso-blueprint

Lean

Verso Blueprint: Noperthedron

Verso Blueprint: Noperthedron

Lean

lean-lang.org

Lean

The Lean FRO

Nonprofit. 20 engineers. Open source. Controlled by no single company.

Sebastian Ullrich and I launched it in August 2023.

28 releases and 8,000+ pull requests merged since its launch.

ACM SIGPLAN Award 2025: "Lean has become the de facto choice for AI-based systems of mathematical reasoning."

Lean

Lean by Example

Lean

Types and Pattern Matching

inductive Tree (α : Type u) where | leaf | node (left : Tree α) (value : α) (right : Tree α) deriving Inhabited, Repr def Tree.map (f : α → β) : Tree α → Tree β | .leaf => .leaf | .node left value right => .node (map f left) (f value) (map f right) #eval Tree.map (2*·) (.node .leaf 3 (.node .leaf 5 .leaf))
Tree.node (Tree.leaf) 6 (Tree.node (Tree.leaf) 10 (Tree.leaf))
Lean

Theorems

Three proofs of the same theorem.

theorem Tree.map_id₁ (tree : Tree α) : tree.map id = tree := by induction tree with | leaf => rfl | node l v r ih_l ih_r => simp [map, *] theorem Tree.map_id₂ (tree : Tree α) : tree.map id = tree := by fun_induction Tree.map <;> simp [*] theorem Tree.map_id₃ (tree : Tree α) : tree.map id = tree := by try?
Lean

Theorems

Three proofs of the same theorem.

theorem Tree.map_compose₁ (tree : Tree α) (f : α → β) (g : β → γ) : (tree.map f).map g = tree.map (g ∘ f) := by induction tree with | leaf => rfl | node l v r ih_l ih_r => simp [map, *] theorem Tree.map_compose₂ (tree : Tree α) (f : α → β) (g : β → γ) : (tree.map f).map g = tree.map (g ∘ f) := by fun_induction Tree.map f tree <;> simp [map, *] theorem Tree.map_compose₃ (tree : Tree α) (f : α → β) (g : β → γ) : (tree.map f).map g = tree.map (g ∘ f) := by try?
Lean

Structures

structure Point (α : Type u) where x : α y : α inductive Color where | red | green | blue structure ColorPoint (α : Type u) extends Point α where c : Color def p : ColorPoint Nat := { x := 10, y := 20, c := .red } example : p.x = 10 := rfl example : p.y = 20 := rfl example : p.c = .red := rfl #eval p.x + p.y
30
Lean

Typeclasses

class Add (α : Type) where add : α → α → α export Add (add) #check add
Ex.Add.add {α : Type} [self : Add α] : α → α → α
instance : Add Nat where add := Nat.add instance : Add Float where add := Float.add instance [Add α] [Add β] : Add (α × β) where add := fun (x₁, y₁) (x₂, y₂) => (add x₁ x₂, add y₁ y₂) def double [Add α] (a : α) : α := Add.add a a #eval double (2, 3.14, -2.1)
(4, 6.280000, -4.200000)
Lean

Typeclasses

class Monoid (α : Type u) extends Mul α, One α where assoc : ∀ a b c : α, a * (b * c) = (a * b) * c one_mul : ∀ a : α, 1 * a = a mul_one : ∀ a : α, a * 1 = a def pow [Monoid α] (a : α) (n : Nat) : α := match n with | 0 => 1 | n+1 => a * pow a n theorem pow_add [Monoid α] (a : α) (n m : Nat) : pow a (n+m) = pow a n * pow a m := by induction n with | zero => simp [pow, Monoid.one_mul] | succ n ih => grind [pow, Monoid.assoc]
Lean

Option and do Notation

def find? (p : α → Bool) (xs : List α) : Option α := do for x in xs do if not (p x) then continue return x failure #eval find? (· > 5) [1, 3, 5, 7, 10]
some 7
Lean

Inductive Predicates

Inductive propositions define relations by their introduction rules. This is the key idea behind our big-step semantics.

mutual inductive Even : Nat → Prop | zero : Even 0 | succ : Odd n → Even (n+1) inductive Odd : Nat → Prop | succ : Even n → Odd (n+1) end example : Odd 3 := .succ (.succ (.succ .zero)) example : Odd 17 := by repeat constructor theorem Even.add_two (h : Even n) : Even (n + 2) := .succ (.succ h) theorem even_or_odd (n : Nat) : Even n ∨ Odd n := by induction n with | zero => exact .inl .zero | succ n ih => cases ih with | inl h => exact .inr (.succ h) | inr h => exact .inl (.succ h)
Lean

Metaprogramming: Syntax Extensions

Lean lets you define new syntax and elaborate it into Lean terms. Example: Idiom brackets are an alternative syntax for working with applicative functors.

syntax (name := idiom) "⟦" (term:arg)+ "⟧" : term -- ⟦f a b⟧ ==> f <*> a <*> b macro_rules | `(⟦$f $args*⟧) => do let mut out ← `(pure $f) for arg in args do out ← `($out <*> $arg) return out def addFirstThird [Add α] (xs : List α) : Option α := ⟦Add.add xs[0]? xs[2]?⟧ #eval addFirstThird [10]
none
#eval addFirstThird [10,20,30,40]
some 40

This is how we'll build the Mini-Radix DSL syntax.

Lean

Summary: Lean Features We'll Use

  • Inductive types — AST: Expr, Stmt, Value

  • Pattern matching — Evaluator, interpreter

  • Option + do — Expression evaluation

  • Syntax macros — [RExpr\|...], [RStmt\|...]

  • Inductive propositions — Big-step semantics

  • simp, omega, cases — Correctness proofs

Lean

Let's Build Something Real

Lean

What We're Building

A simplified version of Radix. Each layer teaches a Lean concept:

MiniRadix layers

Lean

Layer 1: The AST — What Programs Look Like

Lean

Types and Values

Two types: 64-bit unsigned integers and booleans. That's enough to build interesting programs.

inductive Ty where | uint64 | bool deriving DecidableEq, Repr inductive Value where | uint64 : UInt64 → Value | bool : Bool → Value deriving DecidableEq, Repr, BEq
Lean

Operators

Seven binary operators and one unary operator.

inductive BinOp where | add | sub | mul | lt | eq | and | or deriving DecidableEq, Repr inductive UnaryOp where | not deriving DecidableEq, Repr
Lean

Expressions

Four constructors: literal values, variable lookup, binary operations, unary operations.

inductive Expr where | lit : Value → Expr | var : String → Expr | binop : BinOp → Expr → Expr → Expr | unop : UnaryOp → Expr → Expr deriving Repr, DecidableEq
Lean

Statements

Five statement forms: skip, assignment, sequencing, if-then-else, while. No heap, no function calls. The ;; notation lets us write s₁ ;; s₂.

inductive Stmt where | skip | assign : String → Expr → Stmt | seq : Stmt → Stmt → Stmt | ite : Expr → Stmt → Stmt → Stmt | while : Expr → Stmt → Stmt deriving Repr, DecidableEq infixr:130 " ;; " => Stmt.seq
Lean

Layer 2: Concrete Syntax — Making It Readable

Lean

Expression Syntax

Reuses Lean's term parser for expressions. Each macro_rules pattern translates concrete syntax to AST constructors.

syntax "`[RExpr|" term "]" : term macro_rules | `(`[RExpr| true]) => `(Expr.lit (.bool true)) | `(`[RExpr| false]) => `(Expr.lit (.bool false)) | `(`[RExpr| $n:num]) => `(Expr.lit (.uint64 $n)) | `(`[RExpr| $x:ident]) => `(Expr.var $(Lean.quote x.getId.toString)) | `(`[RExpr| ($x)]) => `(`[RExpr| $x]) | `(`[RExpr| $x + $y]) => `(Expr.binop .add `[RExpr| $x] `[RExpr| $y]) | `(`[RExpr| $x - $y]) => `(Expr.binop .sub `[RExpr| $x] `[RExpr| $y]) | `(`[RExpr| $x * $y]) => `(Expr.binop .mul `[RExpr| $x] `[RExpr| $y]) | `(`[RExpr| $x < $y]) => `(Expr.binop .lt `[RExpr| $x] `[RExpr| $y]) | `(`[RExpr| $x == $y]) => `(Expr.binop .eq `[RExpr| $x] `[RExpr| $y]) | `(`[RExpr| $x && $y]) => `(Expr.binop .and `[RExpr| $x] `[RExpr| $y]) | `(`[RExpr| $x || $y]) => `(Expr.binop .or `[RExpr| $x] `[RExpr| $y]) | `(`[RExpr| !$x]) => `(Expr.unop .not `[RExpr| $x])
Lean

Statement Syntax

A custom syntax category rstmt with its own grammar rules. Semicolons terminate assignments. Braces delimit blocks.

syntax ident " := " term ";" : rstmt syntax "skip" ";" : rstmt syntax "if" " (" term ")" " {" rstmt* "}" " else" " {" rstmt* "}" : rstmt syntax "while" " (" term ")" " {" rstmt* "}" : rstmt syntax "`[RStmt|" rstmt* "]" : term macro_rules | `(`[RStmt| ]) => `(Stmt.skip) | `(`[RStmt| skip;]) => `(Stmt.skip) | `(`[RStmt| $x:ident := $e:term;]) => `(Stmt.assign $(Lean.quote x.getId.toString) `[RExpr| $e]) | `(`[RStmt| if ($c) { $ts* } else { $es* }]) => `(Stmt.ite `[RExpr| $c] `[RStmt| $ts*] `[RStmt| $es*]) | `(`[RStmt| while ($c) { $bs* }]) => `(Stmt.while `[RExpr| $c] `[RStmt| $bs*]) | `(`[RStmt| $s $ss*]) => `(Stmt.seq `[RStmt| $s] `[RStmt| $ss*])
Lean

Using the DSL

Same AST, readable syntax. This is exactly how the full Radix DSL works, just with more statement forms.

def sumTo := `[RStmt| n := 100; sum := 0; while (0 < n) { sum := sum + n; n := n - 1; } ]
Lean

Layer 3: Expression Evaluation — Running Expressions

Lean

Why Functions as Data Structures?

We could use HashMap String Value for the environment. Instead:

def Env := String → Option Value

  • No HashMap, no RBMap. Just a function.

  • set returns a new function: fun y => if y = x then some v else σ y

  • This gives us @[simp] lemmas for free: simp can reason about variable lookup without any data structure internals.

  • The proofs essentially write themselves.

  • We use efficient data-structures in Radix.

Lean

The Environment

def Env := String → Option Value namespace Env def empty : Env := fun _ => none def set (σ : Env) (x : String) (v : Value) : Env := fun y => if y = x then some v else σ y @[simp] theorem set_same (σ : Env) (x : String) (v : Value) : (σ.set x v) x = some v := by simp [set] @[simp] theorem set_other (σ : Env) (x y : String) (v : Value) (h : y ≠ x) : (σ.set x v) y = σ y := by simp [set, h] end Env
Lean

Operator Evaluation

Returns none on type mismatch (e.g. true + 3). Marked @[simp] so proofs can reduce these automatically.

@[simp] def BinOp.eval : BinOp → Value → Value → Option Value | .add, .uint64 a, .uint64 b => some (.uint64 (a + b)) | .sub, .uint64 a, .uint64 b => some (.uint64 (a - b)) | .mul, .uint64 a, .uint64 b => some (.uint64 (a * b)) | .lt, .uint64 a, .uint64 b => some (.bool (decide (a < b))) | .eq, a, b => some (.bool (a == b)) | .and, .bool a, .bool b => some (.bool (a && b)) | .or, .bool a, .bool b => some (.bool (a || b)) | _, _, _ => none @[simp] def UnaryOp.eval : UnaryOp → Value → Option Value | .not, .bool b => some (.bool !b) | _, _ => none
Lean

Expression Evaluation

Uses do notation for Option. If any sub-expression fails, the whole evaluation fails. Expressions are pure: they read σ but never modify it.

@[simp] def Expr.eval (σ : Env) (e : Expr) : Option Value := do match e with | .lit v => some v | .var x => σ x | .binop op l r => let vl ← l.eval σ let vr ← r.eval σ op.eval vl vr | .unop op e => let v ← e.eval σ op.eval v def e₁ : Expr := `[RExpr| 2*a + 1 ] #eval e₁.eval .empty
none
def env : Env := Env.empty.set "a" (.uint64 3) #eval e₁.eval env
some (Value.uint64 7)
Lean

Layer 4: Big-Step Semantics — What Programs Mean

Lean

What Are Big-Step Semantics?

A relation BigStep σ s σ' defined by rules:

"Starting in state σ, statement s terminates and produces state σ'."

  • It is a specification, not an executable program.

  • Each rule describes one statement form.

  • We can prove properties about the semantics.

  • This is the ground truth for correctness proofs.

Lean

The BigStep Relation

inductive BigStep : Env → Stmt → Env → Prop where | skip : BigStep σ .skip σ | assign (he : e.eval σ = some v) : BigStep σ (.assign x e) (σ.set x v) | seq (h₁ : BigStep σ₁ s₁ σ₂) (h₂ : BigStep σ₂ s₂ σ₃) : BigStep σ₁ (s₁ ;; s₂) σ₃ | ifTrue (hc : c.eval σ = some (.bool true)) (ht : BigStep σ t σ') : BigStep σ (.ite c t f) σ' | ifFalse (hc : c.eval σ = some (.bool false)) (hf : BigStep σ f σ') : BigStep σ (.ite c t f) σ' | whileTrue (hc : c.eval σ₁ = some (.bool true)) (hb : BigStep σ₁ b σ₂) (hw : BigStep σ₂ (.while c b) σ₃) : BigStep σ₁ (.while c b) σ₃ | whileFalse (hc : c.eval σ = some (.bool false)) : BigStep σ (.while c b) σ notation:60 "⟨" σ ", " s "⟩" " ⇓ " σ':60 => BigStep σ s σ'
Lean

The BigStep Relation (Example)

def σ₁ : Env := .empty def s₁ : Stmt := `[RStmt| a := 0; skip; b := a + 1; ] def σ₂ : Env := σ₁.set "a" (.uint64 0) |>.set "b" (.uint64 1) example : BigStep σ₁ s₁ σ₂ := by apply BigStep.seq apply BigStep.assign simp rfl apply BigStep.seq apply BigStep.skip apply BigStep.assign rfl
Lean

Why Both a Relation and an Interpreter?

  • The relation (BigStep) is the specification. It says what is correct.

  • The interpreter is the implementation. It runs programs.

  • We prove they agree: soundness and completeness.

  • This separation is standard in PL: you can change the interpreter without changing the spec.

The relational semantics is the ground truth. Everything else is verified against it.

Lean

Progress Check

What we have so far:

  • AST: Expr, Stmt, Value, BinOp, UnaryOp

  • Syntax: [RExpr\|...], [RStmt\|...]

  • Evaluator: Expr.eval

  • Semantics: BigStep (7 rules)

What's left:

  • Interpreter: make it run (Stmt.interp)

  • Constant folding: optimize safely (Stmt.constFold)

  • Proofs: show everything agrees

Lean

Layer 5: The Interpreter — Making It Run

Lean

Why the Fuel Pattern?

  • BigStep is a relation. You can't run it — it is not a program.

  • We need an executable version for testing and #eval.

  • While loops may not terminate. We use the fuel pattern: pass a Nat that decreases on each step.

  • fuel = 0 means "give up" (return none).

  • Simple and well-understood. Makes the soundness/completeness proofs straightforward.

  • Then we prove the interpreter agrees with BigStep.

Lean

The Fuel-Based Interpreter

def Stmt.interp (fuel : Nat) (s : Stmt) (σ : Env) : Option Env := match fuel with | 0 => none | fuel + 1 => match s with | .skip => some σ | .assign x e => match e.eval σ with | some v => some (σ.set x v) | none => none | .seq s₁ s₂ => match s₁.interp fuel σ with | some σ' => s₂.interp fuel σ' | none => none | .ite c t f => match c.eval σ with | some (.bool true) => t.interp fuel σ | some (.bool false) => f.interp fuel σ | _ => none | .while c b => match c.eval σ with | some (.bool true) => match b.interp fuel σ with | some σ' => s.interp fuel σ' | none => none | some (.bool false) => some σ | _ => none def Stmt.run (s : Stmt) (fuel : Nat := 1000) : Option Env := s.interp fuel Env.empty
Lean

Computation Rules

All proved by rfl. These are the equations we use in proofs instead of unfold.

@[simp] theorem Stmt.interp_zero : Stmt.interp 0 s σ = none := rfl @[simp] theorem Stmt.interp_skip : Stmt.interp (n + 1) .skip σ = some σ := rfl @[simp] theorem Stmt.interp_assign : (Stmt.assign x e).interp (n + 1) σ = match e.eval σ with | some v => some (σ.set x v) | none => none := rfl @[simp] theorem Stmt.interp_seq : (s₁ ;; s₂).interp (n + 1) σ = match s₁.interp n σ with | some σ' => s₂.interp n σ' | none => none := rfl @[simp] theorem Stmt.interp_ite : (Stmt.ite c t f).interp (n + 1) σ = match c.eval σ with | some (.bool true) => t.interp n σ | some (.bool false) => f.interp n σ | _ => none := rfl @[simp] theorem Stmt.interp_while : (Stmt.while c b).interp (n + 1) σ = match c.eval σ with | some (.bool true) => match b.interp n σ with | some σ' => (Stmt.while c b).interp n σ' | none => none | some (.bool false) => some σ | _ => none := rfl
Lean

Running Programs

def Stmt.runGet (s : Stmt) (x : String) (fuel : Nat := 1000) : Option Value := s.run fuel |>.bind (· x) def factorial := `[RStmt| n := 10; result := 1; while (0 < n) { result := result * n; n := n - 1; } ] #eval factorial.runGet "result"
some (Value.uint64 3628800)
#eval factorial.runGet "result" (fuel := 0)
none
Lean

Layer 6: Constant Folding — Optimizing Safely

Lean

What is Constant Folding?

An optimization pass that evaluates constant expressions at compile time:

  • 3 + 4 becomes 7

  • true && e becomes e (if e is boolean)

  • e + 0 becomes e (if e is uint64)

  • if (true) { s₁ } else { s₂ } becomes s₁

The challenge: identity simplifications like e + 0 → e require type information. We need to know e produces a uint64.

Lean

Quiz: Is e * 0 → 0 a Valid Optimization?

It looks safe: anything times zero is zero. But consider:

  • What if e.eval σ = none (e.g., e uses an undefined variable)?

  • Original: (e * 0).eval σ = none (evaluation fails at e)

  • Optimized: (0).eval σ = some (.uint64 0) (succeeds!)

The optimization changes the behavior: it turns a failing program into a succeeding one.

This is why we need inferTag: identity rules like e + 0 → e are only safe when we know e will produce a value of the right type.

def buggy := `[RStmt| n := e * 0; ] #eval buggy.runGet "n"
none
Lean

Type Tags and Inference

inductive ValTag where | uint64 | bool deriving DecidableEq, Repr @[simp] def Value.tag : Value → ValTag | .uint64 _ => .uint64 | .bool _ => .bool @[simp] def BinOp.resultTag : BinOp → ValTag → ValTag → Option ValTag | .add, .uint64, .uint64 | .sub, .uint64, .uint64 | .mul, .uint64, .uint64 => some .uint64 | .lt, .uint64, .uint64 => some .bool | .eq, _, _ => some .bool | .and, .bool, .bool | .or, .bool, .bool => some .bool | _, _, _ => none @[simp] def UnaryOp.resultTag : UnaryOp → ValTag → Option ValTag | .not, .bool => some .bool | _, _ => none
Lean

Type Tags and Inference

Variables return none: we don't track types in the environment. Conservative but sound.

def Expr.inferTag : Expr → Option ValTag | .lit v => some v.tag | .var _ => none | .binop op l r => do let tl ← l.inferTag let tr ← r.inferTag op.resultTag tl tr | .unop op e => do let t ← e.inferTag op.resultTag t def c₁ : Expr := `[RExpr| 2*3 - 2 ] def c₂ : Expr := `[RExpr| true && false ] #eval c₁.inferTag
some (ValTag.uint64)
#eval c₂.inferTag
some (ValTag.bool)
Lean

BinOp Simplification

The if e.inferTag = some .uint64 guard ensures we only simplify when type-safe.

def BinOp.simplify : BinOp → Expr → Expr → Expr -- Constant folding (both literals) | .add, .lit (.uint64 a), .lit (.uint64 b) => .lit (.uint64 (a + b)) -- ... 5 more literal cases ... -- Identity: e + 0 = e (guarded by type tag) | .add, e, .lit (.uint64 0) => if e.inferTag == some .uint64 then e else .binop .add e (.lit (.uint64 0)) -- ... more identity cases ... | op, a, b => .binop op a b
Lean

Statement-Level Folding

def Expr.constFold : Expr → Expr | .lit v => .lit v | .var x => .var x | .binop op l r => BinOp.simplify op l.constFold r.constFold | .unop op e => UnaryOp.simplify op e.constFold def Stmt.constFold : Stmt → Stmt | .skip => .skip | .assign x e => .assign x e.constFold | .seq s₁ s₂ => .seq s₁.constFold s₂.constFold | .ite c t f => match c.constFold with | .lit (.bool true) => t.constFold | .lit (.bool false) => f.constFold | c' => .ite c' t.constFold f.constFold | .while c b => match c.constFold with | .lit (.bool false) => .skip | c' => .while c' b.constFold
Lean

Constant Folding in Action

def deadBranch := `[RStmt| if (true) { x := 3 + 4; } else { x := 0; } ] -- After constant folding: just `x := 7` example : deadBranch.constFold = Stmt.assign "x" (.lit (.uint64 7)) := by decide
Lean

Layer 7: Correctness Proofs — Trusting the Code

Lean

What We Prove

  • Expr.eval_constFold: folded expression evaluates the same

  • Stmt.constFold_correct: folded statement has same BigStep behavior

  • Stmt.interp_sound: interpreter success implies BigStep

  • Stmt.interp_fuel_mono: more fuel never breaks a successful run

  • Stmt.interp_complete: BigStep implies interpreter success (with enough fuel)

MiniRadix proof architecture

Lean

Expression-Level Correctness

Structural induction. Once we have BinOp.simplify_correct as a @[simp] lemma, the proof is straightforward.

theorem expr_eval_constFold (e : Expr) (σ : Env) : e.constFold.eval σ = e.eval σ := by induction e with | lit v => simp [Expr.constFold, Expr.eval] | var x => simp [Expr.constFold, Expr.eval] | binop op l r ihl ihr => simp only [Expr.constFold, BinOp.simplify_correct, Expr.eval, ihl, ihr] | unop op e ih => simp only [Expr.constFold, UnaryOp.simplify_correct, Expr.eval, ih]
Lean

Statement-Level Correctness

Induction on BigStep. Rewrite condition using Expr.eval_constFold, then case-split on what c.constFold reduces to.

theorem constFold_correct (h : BigStep σ s σ') : BigStep σ s.constFold σ' := by induction h with | skip => exact BigStep.skip | assign he => simp only [Stmt.constFold] exact BigStep.assign (by rw [expr_eval_constFold]; exact he) | seq _ _ ih₁ ih₂ => simp only [Stmt.constFold]; exact BigStep.seq ih₁ ih₂ | ifTrue hc _ ih => simp only [Stmt.constFold] have hc' := hc; rw [← expr_eval_constFold] at hc' split · exact ih · next heq => rw [heq, Expr.eval] at hc'; cases hc' · exact BigStep.ifTrue hc' ih | ifFalse hc _ ih => simp only [Stmt.constFold] have hc' := hc; rw [← expr_eval_constFold] at hc' split · next heq => rw [heq, Expr.eval] at hc'; cases hc' · exact ih · exact BigStep.ifFalse hc' ih -- .. | whileTrue hc _ _ ihb ihw => simp only [Stmt.constFold] at ihw ⊢ have hc' := hc; rw [← expr_eval_constFold] at hc' split at * · next heq => rw [heq, Expr.eval] at hc'; cases hc' · exact BigStep.whileTrue hc' ihb ihw | whileFalse hc => simp only [Stmt.constFold] have hc' := hc; rw [← expr_eval_constFold] at hc' split · exact BigStep.skip · exact BigStep.whileFalse hc'
Lean

Interpreter Soundness

Full proof here

theorem interp_sound {fuel : Nat} {s : Stmt} {σ σ' : Env} (h : s.interp fuel σ = some σ') : BigStep σ s σ' := by apply Stmt.interp_sound h
Lean

Interpreter Completeness

The seq case is the most interesting: take the max of both fuels, then use fuel monotonicity to lift both results.

Full proofs here

theorem interp_fuel_mono {n m : Nat} (h : n ≤ m) {s : Stmt} {σ σ' : Env} (hok : s.interp n σ = some σ') : s.interp m σ = some σ' := by apply Stmt.interp_fuel_mono h hok theorem interp_complete {σ : Env} {s : Stmt} {σ' : Env} (h : BigStep σ s σ') : ∃ fuel : Nat, s.interp fuel σ = some σ' := by apply Stmt.interp_complete h
Lean

Proof Techniques Summary

  • Induction on expressions for evaluation lemmas

  • Induction on BigStep for statement correctness

  • Induction on fuel for interpreter proofs

  • simp only [...] with @[simp] computation rules

  • cases on Option values to handle success/failure

  • omega for natural number arithmetic

  • decide for decidable propositions (testing)

Lean

What We Left Out

Mini-Radix is deliberately minimal. We excluded:

  • Heap allocation: malloc, free, arrays — adds memory safety proofs

  • Function calls: call stack, scoping — adds determinism complexity

  • Linear ownership: tracking who owns what — prevents use-after-free

  • More optimizations: copy propagation, dead code elimination, inlining

  • String type

The full Radix handles all of them.

Lean

What the Full Radix Adds

  • Types: uint64, bool → + string

  • Heap: No → malloc, free, arrays

  • Functions: No → function calls, stack

  • Ownership: No → linear ownership typing

  • Optimizations: 1 (const fold) → 5 verified passes

  • BigStep rules: 7 → 16

  • Lines: ~950 → ~7,400

  • Theorems: 5 → 52

  • sorry: 0 → 0

Lean

Where to Go Next

Lean

What We Built Today

  • A complete verified DSL in ~950 lines of Lean

  • Custom syntax, expression evaluation, big-step semantics

  • A fuel-based interpreter, proved sound and complete

  • An optimization pass, proved correct

  • Zero sorry. Every claim is machine-checked.

AI built the full Radix in a weekend. You can build Mini-Radix in an afternoon.

Fork the repo. Add function calls. Prove it correct.

Thank You

Leo de Moura
lean-lang.org
leanprover.zulipchat.com

X: @leanprover
LinkedIn: Lean FRO
Mastodon: @leanprover@functional.cafe
#leanlang #leanprover

leodemoura.github.io
ETAPS 2026