Cours

Track: programmer

Implement a map, heap, trie, or interval structure and prove a central operation preserves its invariant.

Milestones

• Abstract invariant
• Executable operation
• Preservation and lookup theorems
• Benchmark and API documentation

Track: mathematician

Formalize one coherent topic—such as finite group actions, graph connectivity, elementary number theory, or linear algebra—using Mathlib style.

Milestones

• Definitions aligned with existing APIs
• Supporting lemmas at useful generality
• One substantial theorem
• Examples, docs, and contribution analysis

Track: balanced

Implement an algorithm with mathematical content and prove its specification, such as Euclid, sorting, finite search, or matrix computation.

Milestones

• Executable implementation
• Clean relational specification
• Termination and correctness proofs
• Package, examples, and presentation

Six-week on-ramp for newcomers: orientation to track choice. study plan.

Twelve-week route from core fluency to a defended capstone. study plan.

From first theorem to professional Lean 4 proof engineering

An independent, source-guided curriculum for programmers and mathematicians.

Disclaimer

Independent learning and assessment project. It is not affiliated with Lean FRO and does not issue an official Lean credential.

Track: common — Level: foundation — ~30 min — kernel, trust, architecture

Build the correct mental model: Lean is simultaneously a language, elaborator, tactic framework, and small proof-checking kernel.

Objectives

• Distinguish source syntax, elaborated terms, tactics, and kernel checking
• Explain why tactic bugs need not compromise proof soundness
• Separate definitional equality from a proved proposition

Definition

A proof assistant accepts a theorem only when it can construct a term whose type is the theorem statement. The trusted kernel checks that term using a small dependent type theory.

Lean source is convenient notation, not the final proof object. The elaborator fills implicit arguments, resolves type classes, expands notation, and produces a core expression. Tactics are programs that help build this expression. The kernel then checks it independently.

This architecture gives a useful engineering rule: automation may be sophisticated, but accepted results still reduce to a term checked by the kernel. External code, native evaluation, unsafe declarations, and axioms require separate trust analysis.

Code

#check Nat
#check Nat → Nat
#check True
#check True.intro

-- A theorem is a definition whose result type is a proposition.
theorem truth : True := True.intro

Challenge

Write one sentence describing the role of each layer: parser, elaborator, tactic engine, kernel.

Sources

• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.
• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• The Lean 4 Theorem Prover and Programming Language — Concise architectural context for advanced users.

Track: common — Level: foundation — ~35 min — setup, elan, lake, vscode

Learn the minimal working environment and why every serious Lean file should live in a version-pinned Lake project.

Objectives

• Identify elan, Lean, Lake, VS Code, and InfoView
• Explain why lean-toolchain belongs in a project
• Use the browser playground appropriately

Definition

Elan selects and installs Lean toolchains. Lake builds packages and manages dependencies. The VS Code extension connects the editor to Lean and exposes goals, diagnostics, hovers, and search.

For a quick experiment, the official web playground is enough. For a course, library, or application, create a project and pin its Lean version. Mathlib projects also pin a matching Mathlib revision, which avoids accidental breakage as the language evolves.

Professional work is interactive: edit a small region, read the goal state, inspect a declaration, and make the next local change. Treat errors as structured information rather than as a final verdict.

Code

-- Typical shell workflow (run outside Lean):
-- lake init my_project
-- cd my_project
-- lake build

-- Main.lean
def main : IO Unit := do
  IO.println "Lean is ready"

Challenge

Create a project checklist containing toolchain pinning, build command, editor extension, and a first successful file.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Lean 4 VS Code Extension Manual — Professional fluency depends on using the editor feedback loop well.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.
• Lean 4 Web Playground — Real verification without a local install; use local projects for serious development.

Track: common — Level: foundation — ~40 min — goals, infoview, tactics

Turn the InfoView into a precise dialogue: local context above the turnstile, target below it.

Objectives

• Read hypotheses and target types
• Predict the effect of intro and exact
• Use named intermediate facts to control complexity

Definition

A tactic proof transforms a list of goals. A goal consists of a local context Γ and a target T, often written Γ ⊢ T.

When the target is an implication or a universal quantifier, intro usually moves a binder into the local context. When an available term has exactly the target type, exact closes the goal. apply works backward from a theorem whose conclusion matches the target.

Do not begin by searching randomly for tactics. First classify the outermost constructor of the goal: implication, conjunction, existential, equality, inductive proposition, or algebraic relation. That classification narrows the next legal moves.

Code

theorem compose_implications (P Q R : Prop)
    (hPQ : P → Q) (hQR : Q → R) : P → R := by
  intro hP
  have hQ : Q := hPQ hP
  exact hQR hQ

Challenge

Before revealing the proof, write the goal state after each of the three tactic lines.

Sources

• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Lean 4 VS Code Extension Manual — Professional fluency depends on using the editor feedback loop well.

Track: common — Level: foundation — ~50 min — types, evaluation, functions

Map familiar functional-programming ideas to Lean syntax and its universe of types.

Objectives

• Use #check, #eval, and explicit type annotations
• Recognize function types and application
• Distinguish evaluation from theorem proving

Definition

Every well-formed Lean expression has a type. Function application is written by juxtaposition, and arrows associate to the right.

#check asks Lean to elaborate an expression and report its type. #eval compiles and runs an expression that has executable content. A proposition may be computed in some cases, but proving it means constructing evidence, not merely observing a runtime Boolean.

Lean often infers types, implicit parameters, and overloaded operations from context. Add type annotations when inference has too many possibilities or when documentation clarity matters.

Code

#check 42                 -- Nat
#check (42 : Int)
#check fun x : Nat => x + 1
#check Nat → Nat → Nat

#eval (fun x : Nat => x + 1) 41
#eval [1, 2, 3].map (· * 2)

Challenge

Predict the type and value of (fun f : Nat → Nat => f (f 3)) (· + 2).

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: common — Level: foundation — ~55 min — polymorphism, higher-order, implicit-arguments

Write reusable functions and read implicit parameters without treating them as magic.

Objectives

• Define named and anonymous functions
• Use polymorphic type parameters
• Understand implicit arguments and point-free composition

Definition

A polymorphic function abstracts over a type. Lean writes implicit parameters in braces and infers them from explicit arguments when possible.

The identity function does not need to inspect its input, so its implementation works for any type. Higher-order functions receive or return functions and are central both to programs and to proof terms.

Lean supports concise section variables and Unicode notation, but explicit signatures remain valuable. A professional codebase uses inference to remove noise, not to hide important design constraints.

Code

def identity {α : Type} (x : α) : α := x

def twice {α : Type} (f : α → α) (x : α) : α :=
  f (f x)

def compose {α β γ : Type}
    (g : β → γ) (f : α → β) : α → γ :=
  fun x => g (f x)

#eval twice (· + 3) 10

Challenge

Implement flip, which converts a function α → β → γ into β → α → γ.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: common — Level: foundation — ~60 min — inductive, patterns, option

See algebraic data types and propositions as instances of the same inductive mechanism.

Objectives

• Declare an inductive type
• Pattern-match exhaustively
• Use Option and Except instead of partial behavior

Definition

An inductive type is generated by a finite collection of constructors. To consume a value, define behavior for each possible constructor.

Lean checks that pattern matching is exhaustive. This makes impossible states and missing cases visible during development. Recursive containers such as List α are inductive: nil is the base constructor and cons adds one element.

Use Option α when a result may be absent and Except ε α when failure needs information. These types make control flow explicit and combine naturally with monadic syntax later.

Code

inductive TrafficLight where
  | red | amber | green
  deriving Repr, DecidableEq

def instruction : TrafficLight → String
  | .red => "stop"
  | .amber => "prepare"
  | .green => "go"

def mapOption (f : α → β) : Option α → Option β
  | none => none
  | some x => some (f x)

Challenge

Define a binary tree and a function that counts its leaves.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: common — Level: foundation — ~65 min — recursion, termination, induction

Connect recursive programs to inductive proofs and understand Lean’s termination obligation.

Objectives

• Write structural recursion
• Explain why recursive calls must decrease
• Relate recursion on data to induction on data

Definition

A structurally recursive function calls itself on an immediate substructure of its input. Lean can see that these calls terminate.

Termination is part of accepting a total definition. Simple recursive functions reduce structurally; more complex algorithms may need a measure and a proof that recursive calls decrease it.

The induction principle for a datatype mirrors its constructors. A proof about every list usually has a nil case and a cons case with an induction hypothesis for the tail. This is not a coincidence: proofs and programs share the same eliminators.

Code

def length : List α → Nat
  | [] => 0
  | _ :: xs => length xs + 1

def countdown : Nat → List Nat
  | 0 => []
  | n + 1 => (n + 1) :: countdown n

#eval countdown 5

Challenge

Write sum : List Nat → Nat, then state the theorem that sum distributes over append.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: common — Level: foundation — ~55 min — structures, namespaces, subtypes

Package related fields and invariants into readable interfaces.

Objectives

• Declare structures and construct values
• Use projections and namespace-qualified names
• Choose between a structure, subtype, and inductive type

Definition

A structure is an inductive type with one constructor and named fields. Projections retrieve those fields.

Structures are the basic unit for records, algebraic objects, configurations, and bundled morphisms. A namespace groups names without changing runtime representation.

A subtype {x : α // P x} pairs data with evidence of a property. Use it when there is one underlying value plus an invariant. Use a structure when multiple named components form the object.

Code

structure Point where
  x : Int
  y : Int
  deriving Repr, DecidableEq

namespace Point

def translate (p : Point) (dx dy : Int) : Point :=
  { x := p.x + dx, y := p.y + dy }

end Point

#eval Point.translate { x := 2, y := 3 } 10 (-1)

Challenge

Design a NonEmptyList α structure and a conversion to List α.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: common — Level: intermediate — ~70 min — typeclasses, instances, overloading

Understand instance search as interface resolution, not object-oriented inheritance.

Objectives

• Declare a class and instance
• Read square-bracket instance parameters
• Diagnose missing or ambiguous instances

Definition

A type class is a structure marked for automated instance synthesis. Parameters in square brackets ask Lean to search for an instance.

Type classes support overloaded notation, algebraic hierarchies, serialization, decidable equality, monadic interfaces, and much more. Instance search composes evidence recursively and is sensitive to local context and priorities.

Avoid adding globally surprising instances. The instance graph is part of your API: it should be coherent, terminating, and predictable. When debugging, make expected types explicit and inspect candidate declarations.

Code

class Sized (α : Type) where
  size : α → Nat

instance : Sized (List α) where
  size := List.length

instance : Sized String where
  size := String.length

def twiceSize [Sized α] (x : α) : Nat :=
  2 * Sized.size x

#eval twiceSize [10, 20, 30]

Challenge

Create a Named class with one method and instances for two unrelated structures.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer — Level: intermediate — ~70 min — io, monads, do-notation, except

Use monadic sequencing while keeping pure computation separate from effects.

Objectives

• Read and write do blocks
• Combine Option, Except, and IO
• Keep a pure core around an effectful shell

Definition

A monad supplies pure and bind; do notation is syntax for sequencing computations whose later steps may depend on earlier results.

Lean does not model an effectful function as an ordinary function that secretly mutates the world. An IO α value describes a computation that may perform effects and eventually produce an α.

Professional designs isolate parsing, validation, and transformation as pure functions. The outer IO layer handles files, arguments, clocks, and logging. This improves testability and makes later verification local.

Code

def parsePort (s : String) : Except String Nat := do
  let some n := s.toNat? | throw "not a natural number"
  if n ≤ 65535 then
    pure n
  else
    throw "port out of range"

def main : IO Unit := do
  let input ← IO.getLine
  match parsePort input.trim with
  | .ok n => IO.println s!"accepted: {n}"
  | .error e => IO.eprintln e

Challenge

Refactor a small command-line program into a pure validation function and an IO wrapper.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: common — Level: foundation — ~60 min — curry-howard, proof-terms, logic

Use Curry–Howard as a practical construction guide rather than an abstract slogan.

Objectives

• Interpret implication as a function type
• Construct conjunction and existential evidence
• Recognize proof terms behind tactics

Definition

Under propositions-as-types, a proposition is a type and a proof is a term inhabiting that type.

To prove P → Q, write a function that transforms evidence of P into evidence of Q. To prove P ∧ Q, build a pair. To prove ∃ x, R x, provide a witness and evidence that the witness satisfies the predicate.

Tactics are convenient syntax for constructing these terms. Learning the term-level meaning of each tactic makes proofs easier to debug and reduces dependence on memorized scripts.

Code

theorem idProof (P : Prop) : P → P :=
  fun hP => hP

theorem pairProof (P Q : Prop) : P → Q → P ∧ Q :=
  fun hP hQ => And.intro hP hQ

theorem witness (n : Nat) : ∃ m, m = n :=
  Exists.intro n rfl

Challenge

Give both a term proof and a tactic proof of (P ∧ Q) → (Q ∧ P).

Sources

• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Logic and Proof — Background path for learners who need explicit logic foundations.

Track: common — Level: foundation — ~75 min — logic, quantifiers, cases

Systematically construct and eliminate the logical connectives used in ordinary proofs.

Objectives

• Use intro, exact, constructor, left, right, and cases
• Work with universal and existential quantifiers
• Treat negation as implication to False

Definition

Universal quantification is a dependent function type. Negation ¬P is definitionally P → False.

A conjunction is introduced by constructing both components and eliminated by projection or cases. A disjunction is introduced by selecting a side and eliminated by handling both possibilities. An existential is introduced with a witness and eliminated by unpacking that witness.

Classical logic adds principles such as excluded middle. Lean permits classical reasoning explicitly, but constructive proofs are often computationally informative. Learn to see where classical axioms enter.

Code

theorem distribute (P Q R : Prop) :
    P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R) := by
  intro h
  rcases h with ⟨hP, hQ | hR⟩
  · left
    exact ⟨hP, hQ⟩
  · right
    exact ⟨hP, hR⟩

Challenge

Prove (P → R) → (Q → R) → P ∨ Q → R without automation.

Sources

• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Mathematics in Lean — Primary backbone for the mathematician track.
• Logic and Proof — Background path for learners who need explicit logic foundations.

Track: common — Level: foundation — ~70 min — equality, rewrite, calc, simp

Move between substitution, simplification, and explicit equational reasoning.

Objectives

• Use rfl, rw, simpa, congrArg, and calc
• Distinguish definitional and propositional equality
• Control rewrite direction and location

Definition

Definitional equality is equality by computation and unfolding; rfl closes goals whose two sides reduce to the same expression. Propositional equality is an explicit value of type a = b.

rw [h] substitutes using an equality. simp applies a curated rewrite system and performs reductions. calc exposes the conceptual chain and is often the most maintainable style for nontrivial derivations.

When rfl fails, ask whether the expressions should compute to the same normal form or whether a theorem is required. Do not use stronger automation before understanding this distinction.

Code

theorem map_id (xs : List α) : xs.map (fun x => x) = xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
      simp [ih]

theorem congrExample (h : a = b) : f a = f b := by
  exact congrArg f h

Challenge

Write a calc proof that function composition preserves equality of inputs.

Sources

• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Mathematics in Lean — Primary backbone for the mathematician track.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: common — Level: foundation — ~75 min — tactics, proof-style, refine

Choose tactics based on proof structure and keep scripts stable under refactoring.

Objectives

• Compare exact, apply, refine, have, and show
• Use bullets and case labels
• Prefer explicit structure at semantic boundaries

Definition

Backward reasoning starts from the target and applies rules whose conclusions match it. Forward reasoning derives useful facts from hypotheses. Good Lean proofs combine both.

exact is strongest when you already have the complete term. apply creates goals for missing premises. refine lets you write a partial term with holes. have names a forward consequence. show restates the current target in a useful form.

Large tactic blocks become fragile when they depend on incidental goal order. Use constructor-aligned case labels, local lemmas, and named intermediate facts to make intent visible.

Code

theorem transitive_example (P Q R S : Prop)
    (hPQ : P → Q) (hQR : Q → R) (hRS : R → S) : P → S := by
  intro hP
  apply hRS
  apply hQR
  exact hPQ hP

Challenge

Rewrite the proof using forward reasoning with two named have statements.

Sources

• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Lean 4 VS Code Extension Manual — Professional fluency depends on using the editor feedback loop well.

Track: common — Level: intermediate — ~80 min — simp, rewriting, normalization

Use simp deliberately, configure it locally, and diagnose why it stopped.

Objectives

• Predict common simp reductions
• Use simp only, simp at, and simp_all
• Mark and avoid unsuitable simp lemmas

Definition

simp repeatedly applies simplification lemmas, reductions, congruence rules, and contextual facts until no rule applies.

The simplifier is not an unrestricted theorem prover. Its rewrite orientation aims at canonical forms and termination. A good simp lemma makes expressions smaller or more canonical and does not create loops.

For maintainable proofs, pass the important local lemmas explicitly and use simp only when you need a small stable rule set. Inspect the residual goal: it often reveals the missing normalization step.

Code

theorem append_nil_local (xs : List α) : xs ++ [] = xs := by
  induction xs with
  | nil => simp
  | cons x xs ih => simp [ih]

example (h : x = y) : [x] ++ [] = [y] := by
  simp [h]

Challenge

Find a theorem that becomes one line with simp, then explain every rewrite that simp performs.

Sources

• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.
• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Mathematics in Lean — Primary backbone for the mathematician track.

Track: common — Level: intermediate — ~85 min — induction, cases, generalization

Select an induction variable that matches the recursive definitions in the goal.

Objectives

• Distinguish case analysis from induction
• Generalize variables before induction when needed
• Use induction hypotheses in constructor cases

Definition

Case analysis considers constructors. Induction additionally provides a hypothesis for recursive constructor arguments.

Induct on the data that drives computation. If a function recurses on the first list argument, induction on that argument usually makes definitions unfold cleanly. A poor induction choice leaves an unusable hypothesis.

Sometimes a variable is too specialized when induction begins. Revert or generalize it so the induction hypothesis is quantified strongly enough. Advanced libraries expose tailored induction principles for semantic structures.

Code

theorem append_assoc_local (xs ys zs : List α) :
    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
      simp [ih]

Challenge

Prove that List.length (xs ++ ys) = List.length xs + List.length ys by induction on xs.

Sources

• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Mathematics in Lean — Primary backbone for the mathematician track.

Track: common — Level: intermediate — ~60 min — mathlib, imports, navigation

Find what is already formalized before recreating it.

Objectives

• Read module paths and import boundaries
• Use #check, #print, hover, and go-to-definition
• Recognize naming and namespace patterns

Definition

Mathlib is a large, modular Lean library. Declarations have fully qualified names, while open namespaces and scoped notation control what can be written unqualified.

Begin with the mathematical object, then inspect its namespace and nearby files. API documentation reveals imports, declaration signatures, source links, and related names. In the editor, hover and go-to-definition are often faster than web browsing.

Import Mathlib for experiments; prefer narrower imports in libraries when build time and dependency discipline matter. Avoid guessing theorem names for long periods—search by type shape or concept.

Code

import Mathlib

#check List.map_append
#check Set.Subset.trans
#check Nat.add_comm
#print Set.Subset.trans

open scoped BigOperators

Challenge

Locate one theorem by namespace browsing and one by type-shape search; record the exact query used.

Sources

• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.
• Loogle — Best when you know the formal shape of the theorem you need.
• LeanExplore — Useful when you know the mathematical or programming idea but not its Lean name.
• Lean 4 VS Code Extension Manual — Professional fluency depends on using the editor feedback loop well.

Track: common — Level: intermediate — ~70 min — search, loogle, api

Build a repeatable search workflow instead of relying on memory.

Objectives

• Choose between grep, API docs, Loogle, and semantic search
• Search using partial type signatures
• Validate candidate lemmas in a minimal example

Definition

Theorem discovery is translation between an informal intent, Lean’s chosen definitions, and an exact declaration type.

Use editor completion when you know a namespace prefix. Use Loogle when you know symbols or a type pattern. Use semantic search when you can describe the idea in natural language. Use source search when you suspect a naming family.

A search result is only a candidate. #check it, inspect implicit arguments and type classes, then make a minimal example that applies it. This isolates coercions and namespace issues from the larger proof.

Code

import Mathlib

-- Verify a candidate in isolation.
example {α : Type} (f : α → α) (xs ys : List α) :
    List.map f (xs ++ ys) = List.map f xs ++ List.map f ys := by
  simpa using (List.map_append (f := f) (l₁ := xs) (l₂ := ys))

Challenge

Search for a lemma expressing transitivity of set inclusion without starting from its exact name.

Sources

• Loogle — Best when you know the formal shape of the theorem you need.
• LeanExplore — Useful when you know the mathematical or programming idea but not its Lean name.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.
• Learning Lean 4 — A broad inventory of mature and emerging learning material.

Track: mathematician — Level: intermediate — ~80 min — sets, functions, extensionality

Translate ordinary set-theoretic arguments into predicates and function equality.

Objectives

• Read Set α as α → Prop
• Prove inclusions by introducing elements
• Use extensionality for sets and functions

Definition

In Lean, a set of α is represented as a predicate α → Prop. Membership x ∈ A means A x.

To prove A ⊆ B, introduce an arbitrary element and its membership in A, then prove membership in B. To prove set equality, use extensionality and prove equivalent membership conditions pointwise.

Function equality is also extensional: prove outputs equal for every input. This pattern recurs throughout algebra, topology, measure theory, and category theory in more structured forms.

Code

import Mathlib

example {α : Type} (A B C : Set α)
    (hAB : A ⊆ B) (hBC : B ⊆ C) : A ⊆ C := by
  intro x hx
  exact hBC (hAB hx)

example {α : Type} (A B : Set α) : A ∩ B = B ∩ A := by
  ext x
  simp [and_comm]

Challenge

Prove A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) by extensionality and propositional reasoning.

Sources

• Mathematics in Lean — Primary backbone for the mathematician track.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: mathematician — Level: intermediate — ~85 min — finset, fintype, counting

Navigate the distinction between sets, finite sets with data, and types known to be finite.

Objectives

• Distinguish Set, Finset, and Fintype
• Use membership and cardinality lemmas
• Recognize when decidable equality is required

Definition

Finset α is a finite collection with computational content and no duplicates. Fintype α equips the whole type with a finite enumeration.

Finite combinatorics often moves between predicates, finsets, and subtypes. Coercions make notation pleasant but can obscure which representation a theorem expects. Inspect types when a seemingly obvious lemma does not apply.

Counting proofs combine structural decompositions with cardinality lemmas. Prefer existing API results for unions, images, filters, and products rather than unfolding Finset internals.

Code

import Mathlib

example (s : Finset α) (p : α → Prop) [DecidablePred p] :
    (s.filter p).card ≤ s.card := by
  exact Finset.card_le_card (Finset.filter_subset p s)

example (n : Nat) : (Finset.range n).card = n := by
  simp

Challenge

State and prove a cardinality result for filtering a finset by the always-true predicate.

Sources

• Mathematics in Lean — Primary backbone for the mathematician track.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: common — Level: intermediate — ~90 min — automation, ring, linarith, omega, grind

Choose automation by theory and understand the proof boundary it creates.

Objectives

• Select norm_num, ring, linarith, omega, aesop, or grind appropriately
• Preprocess goals before automation
• Keep automation calls reproducible and readable

Definition

Automation is strongest when the goal belongs to the decision procedure or normalization theory that the tactic implements.

Use norm_num for concrete numeral normalization, ring for polynomial identities, linarith for linear arithmetic over ordered rings and fields, and omega for Presburger arithmetic. aesop performs configurable proof search; grind combines congruence closure, rewriting, and other procedures.

Automation is not a substitute for modeling. Normalize coercions, expose the right hypotheses, and reduce the goal to the tactic’s domain. Record important lemmas explicitly so future readers know why the call succeeds.

Code

import Mathlib

example (x y : ℤ) : (x + y)^2 = x^2 + 2*x*y + y^2 := by
  ring

example (x y : ℚ) (h₁ : x ≤ y) (h₂ : y ≤ x) : x = y := by
  linarith

example (n : Nat) (h : n < 3) : n = 0 ∨ n = 1 ∨ n = 2 := by
  omega

Challenge

Classify five arithmetic goals by the weakest suitable tactic and justify each choice.

Sources

• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.
• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.

Track: common — Level: advanced — ~85 min — debugging, style, maintenance, ci

Treat a formal development as a software system with APIs, tests, reviews, and version constraints.

Objectives

• Minimize failing examples
• Refactor repeated reasoning into lemmas
• Control imports, simp sets, and automation

Definition

Proof engineering is the practice of designing formal code so that it remains comprehensible and stable as definitions and libraries evolve.

When a proof breaks, reduce it to the smallest declaration that still fails. Inspect the exact goal, inferred arguments, coercions, and instance search. This is the proof-assistant equivalent of a minimal reproducible example.

Name domain concepts rather than tactic maneuvers. Localize broad automation, avoid accidental dependencies on global simp lemmas, and separate mathematical statements from technical transport lemmas. Continuous integration should build with the pinned toolchain from a clean checkout.

Code

import Mathlib

-- A stable pattern: small semantic lemmas, then composition.
lemma preserve_nonneg (x : ℤ) (hx : 0 ≤ x) : 0 ≤ x + x := by
  omega

lemma preserve_order (x y : ℤ) (h : x ≤ y) : x + x ≤ y + y := by
  omega

Challenge

Take a one-line automation proof and refactor it into named semantic steps without making it needlessly verbose.

Sources

• Contributing to Mathlib — The practical bridge from learner to ecosystem contributor.
• Lean 4 VS Code Extension Manual — Professional fluency depends on using the editor feedback loop well.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer — Level: advanced — ~90 min — dependent-types, subtype, invariants

Encode selected invariants in types while keeping APIs usable.

Objectives

• Construct and consume subtype values
• Decide what belongs in a type versus a theorem
• Manage proof fields through abstraction

Definition

A subtype {x : α // P x} stores a value x together with a proof of P x. Dependent types allow result types to vary with input values.

Types can prevent invalid states from entering a subsystem, but maximal precision is not always the best interface. Proof-heavy data may increase transport and elaboration costs. Put stable, local invariants in types; leave contextual or frequently changing properties as propositions.

Hide proof construction behind smart constructors and expose ordinary projections. This produces an ergonomic boundary: callers receive certified values without repeating low-level obligations.

Code

def PositiveNat := {n : Nat // 0 < n}

def PositiveNat.ofSucc (n : Nat) : PositiveNat :=
  ⟨n + 1, Nat.zero_lt_succ n⟩

def PositiveNat.value (n : PositiveNat) : Nat := n.1

#eval (PositiveNat.ofSucc 4).value

Challenge

Design a smart constructor returning Option PositiveNat from an arbitrary natural number.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer — Level: advanced — ~95 min — specification, correctness, invariants

Relate a computable implementation to a mathematical specification.

Objectives

• Write preconditions and postconditions
• Separate functional correctness from termination and performance
• Use helper invariants for recursive algorithms

Definition

A functional-correctness theorem states that an implementation’s output satisfies a specification for every input meeting its preconditions.

A common pattern is: define an executable function, define a clean specification, then prove a theorem connecting them. The specification need not be executable; it should optimize for clarity.

Recursive and iterative algorithms often require loop invariants or strengthened induction statements. The strongest useful invariant explains both why the next step is legal and why the final result is correct.

Code

import Mathlib

def max2 (a b : Nat) : Nat := if a ≤ b then b else a

theorem max2_spec (a b : Nat) :
    a ≤ max2 a b ∧ b ≤ max2 a b := by
  unfold max2
  split
  · constructor <;> omega
  · constructor <;> omega

Challenge

Specify a list membership search function and identify the invariant needed for a proof of correctness.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer — Level: advanced — ~100 min — arrays, termination, performance

Use efficient data structures without losing safety or termination.

Objectives

• Explain bounded indexing obligations
• Use measures for nonstructural recursion
• Separate proof erasure from runtime behavior

Definition

Efficient algorithms may recurse on a numeric measure rather than directly on syntax. Lean accepts them when each recursive call is proved to decrease in a well-founded relation.

Array access exposes a proof that an index is in bounds, either explicitly or through checked APIs. Those obligations are part of the safety story, but many proof terms are erased at runtime.

Do not infer performance from source appearance alone. Lean uses optimizations including reference counting and functional-but-in-place updates. Benchmark compiled code, inspect generated behavior when necessary, and keep proof architecture separate from micro-optimization.

Code

def repeatN (n : Nat) (x : α) : List α :=
  match n with
  | 0 => []
  | k + 1 => x :: repeatN k x

-- For nonstructural algorithms, provide a decreasing measure:
-- termination_by remainingWork input

Challenge

Sketch the measure for Euclid’s algorithm or binary search and state what each recursive call must prove.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.
• The Lean 4 Theorem Prover and Programming Language — Concise architectural context for advanced users.

Track: programmer — Level: advanced — ~75 min — lake, packages, testing, ci

Turn individual Lean files into a distributable and reproducible project.

Objectives

• Organize modules and public APIs
• Pin dependencies and retrieve caches
• Add executable tests and theorem-level regression checks

Definition

A Lean package declares modules, libraries, executables, dependencies, and build configuration through Lake.

Use a small import surface and a clear root namespace. Put examples and tests in dedicated modules so the public library does not accidentally depend on them. #guard, examples, and theorem declarations can all serve as regression checks.

CI should install Elan, respect lean-toolchain, fetch dependency caches where appropriate, and run lake build. Documentation should state exact setup commands and the trust assumptions of any external or unsafe components.

Code

-- lakefile.toml sketch
-- name = "verified_tool"
-- version = "0.1.0"
-- defaultTargets = ["VerifiedTool"]
--
-- [[lean_lib]]
-- name = "VerifiedTool"
--
-- [[lean_exe]]
-- name = "verified-tool"
-- root = "Main"

Challenge

Design a package tree for a parser, its specification, correctness proof, executable, and tests.

Sources

• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.
• Lean 4 VS Code Extension Manual — Professional fluency depends on using the editor feedback loop well.
• Contributing to Mathlib — The practical bridge from learner to ecosystem contributor.

Track: mathematician — Level: advanced — ~100 min — algebra, hierarchy, typeclasses

Work fluently with abstract operations whose laws are supplied by instances.

Objectives

• Read hierarchy assumptions such as Monoid, Ring, and Field
• Use generic lemmas at the weakest assumptions
• Control coercions and scalar actions

Definition

Mathlib organizes algebra through structures and type classes: operations and laws are bundled, and stronger structures extend weaker ones.

A theorem stated for a monoid automatically applies to groups and rings because their instances provide the required structure. General statements maximize reuse but can make inference errors harder to read.

When an expression contains several scalar actions, coercions, or overloaded numerals, annotate types and inspect the expected operation. Prefer established hierarchy APIs over unfolding structure fields.

Code

import Mathlib

example {M : Type} [Monoid M] (a b c : M) :
    a * (b * c) = (a * b) * c := by
  simpa [mul_assoc]

example {R : Type} [Ring R] (x y : R) :
    (x + y) * (x - y) = x*x - y*y := by
  ring

Challenge

Restate a concrete integer theorem at the weakest algebraic assumptions that still support its proof.

Sources

• Mathematics in Lean — Primary backbone for the mathematician track.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: mathematician — Level: advanced — ~95 min — number-theory, divisibility, nat, int

Formalize divisibility, primes, gcd, modular arithmetic, and induction over naturals and integers.

Objectives

• Use divisibility witnesses
• Navigate Nat and Int coercions
• Select induction or arithmetic automation appropriately

Definition

a ∣ b means that there exists a multiplier c with b = a * c. Many elementary number-theory proofs are witness construction plus normalization.

Natural-number subtraction is truncated, while integer subtraction is a group operation. Choose the domain deliberately and move across coercions with library lemmas rather than ad hoc rewriting.

For bounded linear arithmetic, omega is often appropriate. For nonlinear divisibility or primality, combine structural lemmas, factor witnesses, and specialized APIs.

Code

import Mathlib

example (a b : Nat) : a ∣ a * b := by
  exact ⟨b, rfl⟩

example (n : Nat) : n ∣ n^2 := by
  exact ⟨n, by simp [pow_two]⟩

Challenge

Prove that if a ∣ b and b ∣ c, then a ∣ c, first by witnesses and then with an existing lemma.

Sources

• Mathematics in Lean — Primary backbone for the mathematician track.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: mathematician — Level: advanced — ~110 min — linear-algebra, linear-map, extensionality

Understand the bundled morphism style and how linear structure propagates through the library.

Objectives

• Read LinearMap and Submodule declarations
• Use extensionality on linear maps
• Separate coordinate-free proofs from matrix calculations

Definition

A linear map bundles a function with proofs that it preserves addition and scalar multiplication. Subspaces are represented by Submodule structures.

Bundling allows notation, coercion to functions, composition, kernels, ranges, and categorical structure to share one API. To prove two linear maps equal, extensionality reduces the goal to pointwise equality.

Matrices are functions of two indices. Basis-dependent calculations are useful, but many theorems are simpler and more reusable when proved at the level of linear maps and submodules.

Code

import Mathlib

example {R M N : Type} [Semiring R]
    [AddCommMonoid M] [Module R M]
    [AddCommMonoid N] [Module R N]
    (f g : M →ₗ[R] N)
    (h : ∀ x, f x = g x) : f = g := by
  ext x
  exact h x

Challenge

Prove equality of two simple linear maps pointwise, then inspect the extensionality lemma that made it possible.

Sources

• Mathematics in Lean — Primary backbone for the mathematician track.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: mathematician — Level: advanced — ~115 min — topology, filters, continuity

Read Mathlib’s filter-based formulation of limits and continuity.

Objectives

• Interpret Tendsto between filters
• Relate neighborhood filters to epsilon-style statements
• Use continuity composition APIs

Definition

A filter packages a notion of “eventually.” Filter.Tendsto f l₁ l₂ states that preimages under f send eventual properties of l₂ to eventual properties of l₁.

Filters unify convergence of sequences, functions, and nets; limits at finite points and infinity; and almost-everywhere statements. The abstraction is initially unfamiliar but removes repeated quantifier patterns.

Learn the bridge lemmas between high-level continuity and explicit metric estimates. Use existing composition and product theorems before expanding Tendsto into set-level definitions.

Code

import Mathlib

example {α β γ : Type} [TopologicalSpace α]
    [TopologicalSpace β] [TopologicalSpace γ]
    {f : α → β} {g : β → γ}
    (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := by
  exact hg.comp hf

Challenge

Translate the informal statement “continuous functions compose” into the exact types of the two hypotheses and conclusion.

Sources

• Mathematics in Lean — Primary backbone for the mathematician track.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: mathematician — Level: expert — ~120 min — analysis, measure, calculus, integral

Approach advanced analysis through the library abstractions rather than from raw definitions.

Objectives

• Identify derivative and integral APIs
• Track measurability and integrability side conditions
• Use almost-everywhere reasoning and norm estimates

Definition

Mathlib’s analysis stack builds on topological, uniform, metric, normed, measurable, and measure-theoretic structures. Each theorem advertises the exact layer it requires.

Advanced proofs often fail because a side condition is missing: measurability, integrability, finite measure, completeness, or domination. Treat these as first-class lemmas and prove them early.

Avoid unfolding definitions of derivative or integral unless developing the theory itself. Search for congruence, linearity, monotonicity, composition, and dominated-convergence APIs that match the mathematical argument.

Code

import Mathlib

-- A small example at the edge of the analysis hierarchy:
example (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) :
    Continuous (fun x => f x + g x) := by
  fun_prop

Challenge

Take a paper proof involving an integral and list every formal side condition that the proof uses implicitly.

Sources

• Mathematics in Lean — Primary backbone for the mathematician track.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: common — Level: advanced — ~95 min — universes, coercions, elaboration

Debug advanced type errors by understanding what the elaborator is inferring.

Objectives

• Read Type u and universe polymorphism
• Distinguish coercions from definitional equality
• Use explicit arguments and type ascriptions strategically

Definition

Type u is a universe of types. Universe polymorphism lets a declaration work uniformly across universe levels without collapsing all types into one self-containing type.

Coercions insert functions that adapt one expected type to another. They make APIs pleasant, but chains of coercions can hide the actual term being elaborated. show, explicit namespace qualification, and type annotations reveal the intended path.

At advanced level, many “tactic failures” are elaboration mismatches. Reduce notation, print declarations, inspect implicit parameters, and create a small explicitly typed example before changing proof strategy.

Code

universe u v

def const {α : Type u} {β : Type v} (a : α) : β → α :=
  fun _ => a

#check @const
set_option pp.universes true in
#check const

Challenge

Explain why a universe hierarchy is needed instead of assigning Type : Type.

Sources

• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer — Level: expert — ~100 min — metaprogramming, syntax, macros

Extend surface syntax while preserving source locations, scopes, and hygiene.

Objectives

• Distinguish Syntax from Expr
• Use syntax quotations and antiquotations
• Write a small macro and inspect its expansion

Definition

Syntax represents parsed concrete syntax. A macro transforms syntax into syntax before term elaboration.

Lean’s quotations let metaprograms construct syntax using ordinary Lean notation, while antiquotations splice syntax fragments into templates. Hygiene prevents accidental variable capture across macro boundaries.

Macros are appropriate for local syntactic rewrites. When expansion depends on types, expected types, local hypotheses, or environment declarations, write an elaborator instead.

Code

import Lean

macro "twice!" t:term : term =>
  `(($t) + ($t))

#eval twice! 21

macro x:ident "↦" body:term : term =>
  `(fun $x => $body)

#eval (x ↦ x + 1) 5

Challenge

Design syntax for a tiny domain-specific expression and state whether macro expansion is sufficient.

Sources

• Metaprogramming in Lean 4 — Core text for extending Lean and writing automation.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer — Level: expert — ~110 min — expr, metam, metavariables

Manipulate elaborated terms and reason about local contexts.

Objectives

• Recognize major Expr constructors
• Understand metavariables and assignments
• Use MetaM services rather than rebuilding kernel logic

Definition

Expr is Lean’s core representation of elaborated terms. MetaM provides a context and mutable state for inference, unification, typeclass synthesis, and metavariable management.

Expressions use de Bruijn-style internal representations, constants, applications, lambdas, forall expressions, literals, projections, and metavariables. Inspect them through pretty-printers rather than relying on raw constructor dumps.

Metavariables are typed holes. Tactics and elaborators create, refine, and assign them while preserving well-typedness. Always respect local contexts and instantiate assigned metavariables before final inspection.

Code

import Lean
open Lean Meta

-- Conceptual skeleton; run inside MetaM:
-- let type ← inferType expr
-- let type ← whnf type
-- let inst ← synthInstance type
-- logInfo m!"{expr} : {type}"

Challenge

Trace how the goal P ∧ Q can be refined into two metavariables for P and Q.

Sources

• Metaprogramming in Lean 4 — Core text for extending Lean and writing automation.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer — Level: expert — ~110 min — elaboration, dsl, commands

Use type-directed elaboration when syntax expansion alone is insufficient.

Objectives

• Differentiate command, term, and tactic elaborators
• Access expected types and environments
• Report source-aware errors

Definition

Elaboration converts syntax into typed expressions, resolving overloading, implicit arguments, coercions, and type classes in context.

A custom term elaborator can inspect its expected type and generate an expression accordingly. A command elaborator can add declarations or run environment-level actions. A tactic elaborator operates on goals.

Good DSLs produce errors in the vocabulary of the domain while still generating ordinary Lean terms. Keep the trusted boundary small: the generated terms remain subject to kernel checking.

Code

import Lean
open Lean Elab Command

elab "#helloLean" : command => do
  logInfo "hello from a command elaborator"

#helloLean

Challenge

Choose macro, term elaborator, command elaborator, or tactic elaborator for four proposed extensions and justify each choice.

Sources

• Metaprogramming in Lean 4 — Core text for extending Lean and writing automation.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer — Level: expert — ~120 min — tactics, automation, tacticm

Write automation that composes with Lean’s goal model and produces ordinary proof terms.

Objectives

• Inspect and replace goals in TacticM
• Build macro tactics before full elaborators
• Design predictable failure and tracing behavior

Definition

A tactic is a metaprogram that transforms metavariable goals, eventually assigning each goal a proof expression.

Begin with tactic macros that compose existing tactics. Move to tactic elaborators when you need to inspect expressions, synthesize instances, or construct proof terms directly.

Automation should fail locally with useful messages, expose tracing options, and avoid hidden global state. Soundness is preserved by the kernel, but poor automation can still be slow, brittle, or misleading.

Code

import Lean

macro "intro_all" : tactic =>
  `(tactic| repeat intro)

example (P Q : Prop) : P → Q → P := by
  intro_all
  assumption

Challenge

Implement a tactic macro that runs constructor and then tries assumption on both goals.

Sources

• Metaprogramming in Lean 4 — Core text for extending Lean and writing automation.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: common — Level: expert — ~105 min — reflection, decision-procedures, trust

Understand how computation can accelerate proofs while retaining a checkable result.

Objectives

• Distinguish proof by reduction, reflection, and external certificates
• Explain the trusted computing base of each route
• Choose native_decide or specialized tactics carefully

Definition

Reflection proves a general correctness theorem for a computation, then uses evaluation of that computation to establish concrete propositions.

Some tactics normalize expressions and construct proof terms. Others call external solvers and import certificates that Lean checks. decide reduces a decidable proposition in the kernel; native variants may execute faster but have different trust considerations that should be documented.

For critical developments, state which axioms, unsafe declarations, external solvers, and native mechanisms are used. Lean can report axioms of a theorem, but project-level trust also includes build and dependency controls.

Code

import Mathlib

example : (37 : Nat) < 100 := by
  decide

example : (12345 : Nat) % 5 = 0 := by
  norm_num

Challenge

Compare three ways to prove a finite Boolean or arithmetic fact and list their trust/performance tradeoffs.

Sources

• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.
• The Lean 4 Theorem Prover and Programming Language — Concise architectural context for advanced users.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: common — Level: expert — ~110 min — foundations, axioms, classical, quotients

Audit what a theorem depends on and understand the foundational features commonly used in practice.

Objectives

• Use #print axioms
• Explain proof irrelevance and quotient support at a high level
• Identify where classical reasoning enters

Definition

Lean’s kernel checks dependent type theory with inductive types, universes, quotient support, and a proposition universe with proof irrelevance. Additional axioms may be introduced explicitly.

Classical reasoning is convenient and widely used in mathematics. It may remove computational content, but it does not make a theorem invalid. The relevant question is which foundational assumptions a project intends to permit.

#print axioms theoremName reveals axioms reachable from a declaration. A complete audit also considers sorry, unsafe code, native execution, external tools, and the exact compiler and dependencies used to build the artifact.

Code

theorem classical_example (P : Prop) : P ∨ ¬P := by
  classical
  exact Classical.em P

#print axioms classical_example

Challenge

Audit a theorem from a project and write a trust statement that is understandable to a non-Lean reviewer.

Sources

• Theorem Proving in Lean 4 — Primary conceptual backbone for theorem proving.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.
• Learning Lean 4 — A broad inventory of mature and emerging learning material.

Track: common — Level: professional — ~90 min — contributing, review, api-design

Practice the social and technical workflow of a large formal library.

Objectives

• Prepare a minimal, well-scoped contribution
• Follow naming, style, documentation, and import conventions
• Respond constructively to review and CI feedback

Definition

A mature contribution is not only a proof that compiles; it is a reusable API addition positioned correctly in the library hierarchy.

Before coding, search for existing declarations and discuss large designs. Add the weakest useful theorem, appropriate namespace, docstring, tests, and imports. Avoid unrelated formatting or refactors in the same change.

Review often improves theorem statements more than proof scripts. Be prepared to generalize assumptions, align names with conventions, add simp or ext attributes carefully, and split foundational lemmas from applications.

Code

-- Typical contribution checklist:
-- 1. search existing API
-- 2. create a focused branch
-- 3. add declaration + documentation + tests
-- 4. run formatter/linter/build
-- 5. explain mathematical and API motivation in the PR

Challenge

Select a small missing lemma in a domain you know and write a contribution proposal before implementing it.

Sources

• Contributing to Mathlib — The practical bridge from learner to ecosystem contributor.
• Learning Lean 4 — A broad inventory of mature and emerging learning material.
• Mathlib API Documentation — The authoritative place to inspect declarations and module structure.

Track: common — Level: professional — ~120 min — capstone, portfolio, professional

Demonstrate professional competence through a complete, reviewable artifact.

Objectives

• Scope a project with explicit success criteria
• Integrate code, proofs, tests, documentation, and CI
• Present trust assumptions and limitations

Definition

A capstone is evidence of integrated skill: modeling, implementation, theorem discovery, proof maintenance, project tooling, and communication.

Programmer capstones may verify a parser, data structure, protocol state machine, optimizer, or algorithm. Mathematician capstones may formalize a coherent theorem cluster with reusable definitions and supporting API.

Keep the project small enough to finish and deep enough to require design decisions. Include a README, architecture note, theorem inventory, build instructions, examples, tests, and a short retrospective on failed approaches.

Code

-- Suggested repository layout:
-- Project/
--   Basic.lean        -- definitions
--   Spec.lean         -- mathematical specification
--   Correctness.lean  -- main theorems
--   Examples.lean     -- executable or formal examples
-- Main.lean
-- lakefile.toml
-- lean-toolchain
-- README.md

Challenge

Write a one-page capstone proposal with scope, definitions, three milestone theorems, tooling, and acceptance criteria.

Sources

• Functional Programming in Lean — Primary backbone for the programmer track.
• Mathematics in Lean — Primary backbone for the mathematician track.
• Contributing to Mathlib — The practical bridge from learner to ecosystem contributor.
• Lean Language Reference — Consult after a tutorial gives intuition and exact behavior matters.

Track: programmer

Build a small expression language, parser, evaluator, and pretty-printer. Prove round-trip or semantic preservation properties.

Milestones

• Typed AST and evaluator
• Parser correctness theorem for an accepted subset
• Pretty-print/parse round trip
• Lake package, tests, CI, trust note