After the modules: project ideas

Ideas for your own repositories, from easiest to hardest. Each one combines programming and proving, which is what makes Lean interesting.

1. Verified sorting algorithms ⭐ (recommended first)

  • Implement insertion sort and merge sort on List Nat.
  • Prove that the result is sorted.
  • Prove that the result is a permutation of the input.
  • You learn: induction, auxiliary lemmas, inductive predicates (Sorted).
  • Estimated time: 1 week.

2. Expression calculator with a verified optimizer

  • Define an Expr type (numbers, variables, addition and multiplication) and an eval function.
  • Write an optimizer (x + 0 → x, x * 1 → x, constant folding).
  • Prove that eval (optimize e) = eval e.
  • You learn: recursive inductive types and proofs by structural induction. It is the "hello world" of compiler verification.
  • Estimated time: 1 week.

3. Mini compiler to a stack machine

  • Extend project 2: compile Expr to instructions (push, add, mul) for a stack machine.
  • Prove that running the compiled code gives the same result as eval.
  • You learn: generalizing the induction hypothesis, the most important skill in verification.
  • Estimated time: 1–2 weeks.

4. A command-line program in Lean

  • A real tool you can run with lake exe: a word counter, a CSV-to-JSON converter or a to-do manager backed by a text file.
  • You learn: IO, monads, file handling and Lean as a general-purpose language (Functional Programming in Lean, chapters 2–7).
  • Estimated time: 1 week.

5. Verified data structures

  • A binary search tree with insert, find and delete.
  • Prove that the ordering invariant is preserved and that find finds what was inserted.
  • Extra: do it with AVL or red-black trees.
  • Estimated time: 2 weeks.

6. Mathematics with Mathlib

  • Create a new project with lake new my-math math, which includes Mathlib, Lean's large mathematics library.
  • Formalize classic results: the infinitude of primes, the irrationality of √2 or properties of sequences.
  • You learn: to search a huge library and to use powerful tactics (ring, linarith, norm_num, exact?).
  • Resource: Mathematics in Lean.
  • Estimated time: ongoing.

7. Advent of Code in Lean

  • Solve the Advent of Code puzzles in Lean and, where possible, prove a property of your solution.
  • A good way to practice daily with varied problems.

Suggested layout for each repository

my-project/
├── README.md          ← what it is, what is proved and how to build it
├── lakefile.toml
├── lean-toolchain     ← pins the Lean version
├── MyProject.lean
└── MyProject/
    ├── Basic.lean     ← definitions
    └── Theorems.lean  ← proofs

Tip: add a GitHub Action to each repository that runs lake build on every push, so you always know everything still compiles. The official action is leanprover/lean-action.