Have you ever wondered what happens when you formally verify code against the wrong specification? We built a workshop repository to explore exactly that question—and to provide a comprehensive learning path for Lean 4, the functional programming language and interactive theorem prover.
This workshop contains 17 runnable examples, 55+ exercises with solutions, and a satirical proof series that demonstrates why specifications matter more than proofs.
Lean 4 occupies a unique position in the programming landscape. It’s simultaneously:
- A functional programming language with dependent types
- An interactive theorem prover for mathematical proofs
- A metaprogramming platform where you can extend the language itself
Unlike proof assistants that feel academic, Lean 4 is designed for real software development. The same language you use to prove theorems is the language you use to write programs.
The heart of our workshop is a series of “O(1)” algorithms that technically satisfy their specifications while being completely useless.
-- The "fastest" sorting algorithm ever proven correct
def sort {α : Type} : List α → List α := id
-- Our "specification" for permutation
def isPermutation : List α → List α → Bool
| xs, ys => xs.length == ys.length -- Only checks length!
-- Proof: sort produces a permutation
theorem sort_is_permutation (xs : List α) :
isPermutation xs (sort xs) = true := by simp [sort, isPermutation]The proof is valid. The specification is garbage.
sort [3, 1, 4, 1, 5] returns =[3, 1, 4, 1, 5]=—unchanged. Our “permutation check” passes because the lengths match. We’ve proven our code matches our spec; we just forgot to make our spec meaningful.
| Algorithm | Implementation | Weak Specification |
|---|---|---|
| O1Sort | Identity function | Permutation = same length |
| O1Search | Return first element | “Returns element from list” |
| O1Hash | Return list length | “Deterministic” |
| O1Compress | Return empty list | “Output ≤ input size” |
| O1Encrypt | Identity function | “Reversible” |
Each “proof” is technically correct. Each algorithm is worthless.
The lesson: Formal verification proves your code matches your spec. It doesn’t prove your spec captures your intent.
After the satirical examples, we show proper specifications. Here’s correct sorting:
-- Correct permutation: same elements with same counts
def count (n : Nat) : List Nat → Nat
| [] => 0
| x :: xs => (if x == n then 1 else 0) + count n xs
def isPermutation (xs ys : List Nat) : Prop :=
∀ n, count n xs = count n ys
-- Now sort [3,1,4] cannot equal [4,5,6] even though lengths matchBeyond proofs, the repository teaches Lean 4 as a programming language:
-- Safe division that can't crash
def safeDiv (a b : Nat) : Option Nat :=
if b == 0 then none else some (a / b)
-- Chain operations with do-notation
def compute (a b c : Nat) : Option Nat := do
let x ← safeDiv a b
let y ← safeDiv x c
return y + 1
#eval compute 100 5 2 -- some 11
#eval compute 100 0 2 -- none (no crash!)-- Define what "doubleable" means
class Doubleable (α : Type) where
double : α → α
-- Implement for different types
instance : Doubleable Nat where
double := (· * 2)
instance : Doubleable String where
double := fun s => s ++ s
-- Use polymorphically
#eval Doubleable.double 5 -- 10
#eval Doubleable.double "ab" -- "abab"-- Stack operations with state
def push (x : α) : StateM (List α) Unit :=
modify (x :: ·)
def pop : StateM (List α) (Option α) := do
let stack ← get
match stack with
| [] => return none
| x :: xs => set xs; return some x
-- Run it
#eval (do push 1; push 2; push 3; pop).run []
-- (some 3, [2, 1])The proof examples cover the core techniques:
-- Prove reverse(reverse(xs)) = xs
theorem reverse_reverse (xs : List α) : xs.reverse.reverse = xs := by
induction xs with
| nil => rfl
| cons x xs ih => simp [ih]-- De Morgan's law
theorem demorgan (h : ¬(P ∨ Q)) : ¬P ∧ ¬Q := by
constructor
· intro hp; exact h (Or.inl hp)
· intro hq; exact h (Or.inr hq)The repository includes 55+ exercises across three difficulty levels:
| File | Topics | Difficulty |
|---|---|---|
| Ex01_Basics.lean | rfl, simp, exact, constructor | Beginner |
| Ex02_NaturalNumbers.lean | induction, omega, arithmetic | Intermediate |
| Ex03_Lists.lean | list operations, recursion | Intermediate |
Each exercise has a corresponding solution file. The exercises use sorry as placeholders for students to fill in.
# Clone the repository
git clone https://github.com/aygp-dr/lean4-workshop
# Check your Lean installation
cd lean4-workshop
make deps
# Verify all examples compile
make verify-examples
# Start with the satirical examples
lean examples/satirical/01_O1Sort.lean- Play the Natural Number Game - Interactive introduction to proofs
- Read the satirical examples - Understand why specifications matter
- Study =examples/correct/01_CorrectSort.lean= - See proper specifications
- Work through =examples/fp/= - Learn Lean as a programming language
- Complete the exercises - Practice proof techniques
- Read Functional Programming in Lean - Deeper dive
Formal verification is increasingly important in critical systems. But verification is only as good as your specification. The O(1) examples aren’t just jokes—they’re warnings:
- Smart contracts have lost millions due to correct code with wrong specs
- Security proofs can verify the wrong threat model
- Algorithm correctness depends entirely on what “correct” means
Lean 4 gives us the tools to write precise specifications and prove our code meets them. The hard part isn’t the proof—it’s getting the specification right.
- Lean 4 Official Site
- Functional Programming in Lean (FPIL)
- Theorem Proving in Lean 4 (TPIL)
- Mathematics in Lean (MIL)
- Lean Zulip Chat - Active community
The repository is open source. Contributions welcome:
- Additional satirical examples
- More exercises
- Improved explanations
- Bug fixes
See the repository for details.
—
Formal verification: proving your code does exactly what you said, even when what you said was wrong.