Levelized Lean

The Problem

Lean 4 is a powerful theorem prover, but as projects grow, two problems emerge:

• For humans and LLMs: To understand what a module provides, you have to read the proof. Proofs can be hundreds of lines long and tell you why something is true — but all you wanted to know was what is true.
• For build systems: Changing a proof in a low-level file triggers recompilation up the entire import chain, even though the proof is erased from compiled .olean files.

Both problems have the same root cause: Lean doesn't separate interface from implementation. Every file is both a header and a source file.

C++ solved this in the 1990s.

The Idea

This is the levelized design from John Lakos' Large-Scale C++ Software Design, adapted for Lean 4. The insight: in C++, you read .h files to understand a module's API and only open .c files when you need to change the implementation. We apply the same discipline to theorem proving.

Here's what a header file looks like in our system:

-- Quicksort.lean (the header)
import LeanPractice.Code.Quicksort
import LeanPractice.Proofs.Quicksort

Wrap qs_mem_proof := @quicksort_mem

ProvenTheorem quicksort_sorted : ∀ (l : List Nat), Sorted (quicksort l)
ProvenTheorem qs_mem : ∀ (l : List Nat) (x : Nat), x ∈ quicksort l ↔ x ∈ l

Two lines. That's the entire public API of quicksort: it produces sorted output, and it preserves membership. The proof is 70+ lines in a separate file that consumers never need to open.

File Structure

Three parallel directories hold implementation details. Headers are the only .lean files at the top level (besides Basic.lean). An LLM running ls *.lean gets exactly the headers.

Code/Module.lean — the implementation

Contains the function definition, helper lemmas needed by the proof, and a _spec definition stating what the module promises. This is the .c file.

Proofs/Module.lean — the proof

The actual proof, named <theorem>_proof. Only imports the Code file — no circular dependencies. Can be arbitrarily long and complex without affecting consumers.

Tests/Module.lean — compiler-verified tests

Hard-coded test cases as example statements using native_decide. If the file compiles, every test passed:

-- Tests/BubbleSort.lean
-- If this file compiles, every test passed.

example : Sorted (bubbleSort []) := by native_decide
example : Sorted (bubbleSort [5, 4, 3, 2, 1]) := by native_decide
example : Sorted (bubbleSort [3, 1, 4, 1, 5, 9, 2, 6]) := by native_decide
example : Sorted (bubbleSort [1000, 1, 500, 2, 999]) := by native_decide

Module.lean — the header

The header is the readable source of truth. A reader (human or LLM) should understand everything a module provides by reading the header alone.

Compare a fully-proven module with one that's still in progress:

ProvenTheorem quicksort_sorted
  : ∀ (l : List Nat), Sorted (quicksort l)

ProvenTheorem qs_mem
  : ∀ (l : List Nat) (x : Nat),
    x ∈ quicksort l ↔ x ∈ l

Signature bubbleSort
  : List Nat → List Nat

TestedConjecture bubbleSort_sorted
  : ∀ (l : List Nat), Sorted (bubbleSort l)

ProvenTheorem bs_pass_mem
  : ∀ (l : List Nat) (x : Nat),
    x ∈ bubblePass l ↔ x ∈ l

At a glance you can see: quicksort is fully proven, bubble sort's sortedness is only tested (not proven), but its pass-level membership is proven. The evidence level is in the macro name itself.

The Header Macros

All macros are defined in Basic.lean. They're short — the entire macro system is about 40 lines of code.

Signature macros (type + totality)

Signature is redundant when a ProvenTheorem already covers the full input space (totality is implied). Include it when the header has only tested/unproven conjectures, or when the theorem covers a restricted input space.

Evidence macros (behavioral claims)

Wrapping external theorems

Proof files and external libraries don't always follow the _proof naming convention. Wrap creates aliases:

-- The external theorem is called `quicksort_mem`, not `qs_mem_proof`
Wrap qs_mem_proof := @quicksort_mem

-- Now this works:
ProvenTheorem qs_mem : ∀ (l : List Nat) (x : Nat), x ∈ quicksort l ↔ x ∈ l

Wrap expands to noncomputable def. If the types don't match, Lean catches it at compile time.

The Evidence Hierarchy

From weakest to strongest guarantee:

Signature / PartialSignature   type + totality, zero behavior claims
         │
UnprovenConjecture             asserted behavior, zero evidence (sorry)
         │
TestedConjecture               checked on hard-coded examples (native_decide)
         │
ProvenTheorem                  proven for ALL inputs (Lean's type checker)

Each level is visible in the header at a glance. You never have to compile or open another file to know the evidence level of any claim.

A promotion script (promote.sh) automatically rewrites headers when you add a proof file — changing TestedConjecture to ProvenTheorem, updating imports, and adjusting everything consistently.

Dependency Structure

Lean enforces acyclic imports — circular dependencies are a compile error. The directory layout reflects purpose, and levels emerge naturally from the import graph:

        Main.lean
           │
    ┌──────┴──────┐
    │   Headers    │   Quicksort.lean, MergeSort.lean, ...
    └──────┬──────┘
    ┌──────┴──────┐
    │  Code/ +    │   Code/Quicksort.lean
    │  Proofs/ +  │   Proofs/Quicksort.lean
    │  Tests/     │   Tests/BubbleSort.lean
    └──────┬──────┘
    ┌──────┴──────┐
    │  Basic.lean │   Shared definitions, macros
    └─────────────┘

Changing a header triggers recompilation of everything above it. Changing a proof triggers nothing — the .olean for the header doesn't change because proofs are erased at compile time.

Facades: Wrapping External Libraries

External libraries (Mathlib, Batteries, CSLib) name theorems however they like. The Wrap macro enables facade headers that re-export their API in our uniform format, without modifying their code.

Here's a real example — a facade over an external BST library:

-- Facades/BST.lean
-- The external library has 90 lines with deep namespaces.
-- This facade re-exports the public API.

import LeanPractice.External.BST

-- Function signatures
Signature External.Data.BST.Tree.insert : Tree Nat → Nat → Tree Nat
Signature External.Data.BST.Tree.mem    : Tree Nat → Nat → Bool
Signature External.Data.BST.Tree.toList  : Tree Nat → List Nat

-- Wrap their names to our convention
Wrap bst_insert_preserves_proof := @External.Data.BST.insert_preserves_bst
Wrap bst_toList_sorted_proof    := @External.Data.BST.toList_sorted

-- The public API: everything a consumer needs
ProvenTheorem bst_insert_preserves :
  ∀ (t : Tree Nat) (x : Nat), IsBST t → IsBST (t.insert x)

ProvenTheorem bst_toList_sorted :
  ∀ (t : Tree Nat), IsBST t → List.Pairwise (· < ·) t.toList

An LLM reads 10 lines instead of 90. The external library's code is untouched. If the library changes a theorem's type, the facade fails to compile — the lie is caught.

This stacks: facades import external code, headers import facades, consumers import headers. Each layer sees only the layer above. You can write facades for any Lean library and get uniform, LLM-friendly access to the entire ecosystem.

Fast Headers: Breaking the Recompilation Cascade

The problem

In standard Lean, changing a proof in a low-level file triggers recompilation up the import chain. Even though proofs are erased in .olean files, the build system tracks input hashes — if a dependency's .olean changes at all, everything above it rebuilds.

The solution: axiom headers

FastHeader declares theorems as axiom — no proof dependency, no sorry warning, no import of proof files:

-- Fast/Quicksort.lean
import LeanPractice.Code.Quicksort
-- NOTE: No import of Proofs/Quicksort!
-- Changing the proof rebuilds NOTHING above this file.

namespace Fast
FastHeader quicksort_sorted : ∀ (l : List Nat), Sorted (quicksort l)
FastHeader quicksort_mem : ∀ (l : List Nat) (x : Nat), x ∈ quicksort l ↔ x ∈ l
end Fast

Soundness

The gap (axiom with no proof import) is closed by separate verification files that are only built by CI, not during development:

-- Verify/Quicksort.lean (CI-only)
import LeanPractice.Proofs.Quicksort

example : ∀ (l : List Nat), Sorted (quicksort l) := quicksort_sorted_proof
example : ∀ (l : List Nat) (x : Nat), x ∈ quicksort l ↔ x ∈ l := quicksort_mem

If the axiom's type doesn't match the proof's type, the verification file fails to compile. CI catches it; development stays fast.

What rebuilds when?

The C++ analogy

Lakos designed this for C++ compilation speed in the 1990s. The same structure solves Lean proof-checking speed for the same reason: separate the interface from the implementation, cascade only on interface changes.

Why This Matters for LLMs

Context windows are limited. To use a module, an LLM only needs its header — a few lines per function/theorem. The proofs (which can be hundreds of lines) stay out of context entirely.

ProvenTheorem quicksort_sorted : ∀ (l : List Nat), Sorted (quicksort l)
ProvenTheorem qs_mem : ∀ (l : List Nat) (x : Nat), x ∈ quicksort l ↔ x ∈ l

Headers are the API. Not just the "main" theorem — every theorem a consumer might need. If an LLM gets stuck because a lemma isn't in any header, that lemma belongs in a header.

Source Code

The complete working implementation is available on GitHub: