CLRS-Lean is a fourth-edition-primary Lean 4 companion for the mathematical
correctness arguments in Introduction to Algorithms. Canonical chapter
guides live under CLRSLean.FourthEdition; existing unqualified chapter imports
retain their third-edition meanings during the compatibility period. The
repository is both a Lean library and a book-style Verso site: chapter guides
explain the formalization boundary, while section modules contain executable
definitions, theorem interfaces, and proofs.
Fourth-edition snapshot. 35 of 35 chapters have canonical represented content. 1,580 / 1,580 selected source-inventory entries are proved and mapped into the fourth-edition ledger. This selected inventory is not a claim of complete fourth-edition section coverage. 465 additional entries remain available through the machine-readable online-material catalog. They are disjoint from the canonical chapter counts; compatibility imports do not duplicate either ledger.
- Website
- Generated progress dashboard
- Reader-facing proof status
- Contributor workflow
- Documentation index
The public project name is CLRS-Lean. Lean modules use the import-friendly
root CLRSLean.
The project formalizes selected fourth-edition CLRS sections, not every exercise
or every line of pseudocode. Reused theorem developments are counted only in
the fourth-edition chapter selected by
docs/clrs-fourth-edition-map.csv. A chapter
may be complete for its current mathematical model while still leaving pointer
mutation, RAM costs, or imperative refinement for a later layer.
Moved and third-edition-only groups are counted separately in
docs/clrs-online-material.csv; the two ledgers
are disjoint.
All currently selected theorem entries are kernel-checked — main
contains no sorry, admit, or project axiom, and headline theorems depend
only on the three standard Lean/Mathlib axioms (propext, Classical.choice,
Quot.sound). The per-chapter table below is generated from
docs/clrs-proof-progress.csv by
scripts/gen_readme_table.py:
Tracked-proof completion and fourth-edition coverage are separate metrics.
A proved / tracked value such as 47 / 47 means every entry currently selected
for that chapter is proved; it does not mean every textbook obligation has been
selected. Edition-level gaps determine the status and Edition gaps column.
| Ch | Title | Status | Proved / tracked | Edition gaps |
|---|---|---|---|---|
| 1 | The Role of Algorithms in Computing | ⚪ guide | 0 / 0 | — |
| 2 | Getting Started | 🟢 complete | 7 / 7 | — |
| 3 | Characterizing Running Times | 🟢 complete | 56 / 56 | — |
| 4 | Divide-and-Conquer | 🟢 complete | 99 / 99 | — |
| 5 | Probabilistic Analysis and Randomized Algorithms | 🟢 complete | 26 / 26 | — |
| 6 | Heapsort | 🟢 complete | 78 / 78 | — |
| 7 | Quicksort | 🟢 complete | 34 / 34 | — |
| 8 | Sorting in Linear Time | 🟢 complete | 58 / 58 | — |
| 9 | Medians and Order Statistics | 🟢 complete | 72 / 72 | — |
| 10 | Elementary Data Structures | 🟢 complete | 21 / 21 | — |
| 11 | Hash Tables | 🟢 complete | 59 / 59 | — |
| 12 | Binary Search Trees | 🟢 complete | 40 / 40 | — |
| 13 | Red-Black Trees | 🟢 complete | 40 / 40 | — |
| 14 | Dynamic Programming | 🟢 complete | 90 / 90 | — |
| 15 | Greedy Algorithms | 🟢 complete | 27 / 27 | — |
| 16 | Amortized Analysis | 🟢 complete | 69 / 69 | — |
| 17 | Augmenting Data Structures | 🟢 complete | 79 / 79 | — |
| 18 | B-Trees | 🟢 complete | 147 / 147 | — |
| 19 | Data Structures for Disjoint Sets | 🟢 complete | 84 / 84 | — |
| 20 | Elementary Graph Algorithms | 🟢 correctness | 47 / 47 | — |
| 21 | Minimum Spanning Trees | 🟢 complete | 52 / 52 | — |
| 22 | Single-Source Shortest Paths | 🟢 complete | 31 / 31 | — |
| 23 | All-Pairs Shortest Paths | 🟢 complete | 29 / 29 | — |
| 24 | Maximum Flow | 🟢 complete | 35 / 35 | — |
| 25 | Matchings in Bipartite Graphs | 🟢 complete | 18 / 18 | — |
| 26 | Parallel Algorithms | 🟢 complete | 95 / 95 | — |
| 27 | Online Algorithms | 🟢 complete | 10 / 10 | — |
| 28 | Matrix Operations | 🟢 complete | 9 / 9 | — |
| 29 | Linear Programming | 🟢 complete | 10 / 10 | — |
| 30 | Polynomials and the FFT | 🟢 complete | 34 / 34 | — |
| 31 | Number-Theoretic Algorithms | 🟢 complete | 18 / 18 | — |
| 32 | String Matching | 🟢 complete | 61 / 61 | — |
| 33 | Machine-Learning Algorithms | 🟢 complete | 15 / 15 | — |
| 34 | NP-Completeness | 🟠 partial coverage | 20 / 20 | Concrete polynomial-time TM2 implementations of the… |
| 35 | Approximation Algorithms | 🟢 complete | 10 / 10 | — |
Total: 1580 of 1580 selected theorem entries have kernel-checked proofs across 35 represented fourth-edition chapters (no sorry/admit/project axiom on main). This does not by itself claim complete fourth-edition coverage.
Status legend: 🟢 complete / correctness (advertised theorem stack sealed) ·
🟡 sections (represented sections complete, not the whole chapter) ·
🟠 partial coverage (selected proofs exist, but named fourth-edition
section obligations remain) ·
⚪ guide · ⬜ not started.
Notable results across the library:
- Ch4 — recursive Strassen with a
Θ(n^{lg 7})runtime and the represented Master-theorem infrastructure; maximum subarray is retained online. - Ch7 / 9 / 11 — a shared finite-expectation toolkit powering randomized
quicksort's pairwise comparison probability, schedule-driven randomized
SELECTwith expected partition-work cost at most4*c*n, and SUHA + universal-hashing expected search costs. - Online material — the retained Fibonacci-heap logarithmic degree bound and
recursive van Emde Boas structure with
O(log log u)operations. - Ch19 — executable union-find with the inverse-Ackermann
O((m+n) α(n))amortized bound. - Ch20 / 21 — sealed BFS/DFS/topological-sort/SCC theory and MST (Kruskal + Prim) correctness.
- Ch22 — Bellman-Ford correctness, Dijkstra's greedy theorem,
dijkstraInit_invariant, finaldijkstraLoop_correct, and the abstract work bounds; per-edge ordering and mutable/RAM refinements are optional. - Ch26 — executable parallel matrix and merge algorithms with correctness,
work/span bounds, a total greedy scheduler, and
Tₚ ≤ T₁/p + T∞. - Ch28 — LUP decomposition and solving, matrix inversion, Cholesky decomposition with uniqueness, least squares, and the principal cost bounds.
- Ch29 — reusable linear-programming formulations and duality results; detailed SIMPLEX material is retained in the online-material catalog.
See the proof status board for the scheduling view and the proof map for theorem-level detail.
CLRSLean.lean library root and website landing page
CLRSLean/FourthEdition/Chapter_XX.lean
canonical fourth-edition chapter guide
CLRSLean/Chapter_XX.lean compatibility source guide and aggregator
CLRSLean/Chapter_XX/Section_*.lean
current theorem-bearing compatibility sources
CLRSLean/OnlineMaterial.lean retained online/supplementary content
CLRSLean/ProofPatterns/ small reusable cross-chapter proof APIs
CLRSLean/Progress.lean generated public progress dashboard
CLRSLean/Status.lean concise reader-facing status page
CLRSLean/Workflow.lean public contribution workflow
Tests/ stable interface and closure checks
docs/ maintainer ledgers, design notes, and audits
scripts/ metadata, site, and repository checks
literate.toml Verso navigation and page titles
The detailed dependency and ownership rules are in
docs/repository-architecture.md.
| Question | Canonical source |
|---|---|
| What Lean modules exist? | CLRSLean/, checked against literate.toml |
| What does a chapter number mean? | docs/clrs-fourth-edition-map.csv |
| What is the public theorem interface? | Section .lean files and Tests/ |
| What is the chapter-level progress snapshot? | docs/clrs-proof-progress.csv |
| What theorem names and proof boundaries exist? | docs/proof-map.md |
| What should be worked on next? | docs/proof-status-board.md |
| What is blocked or deliberately deferred? | docs/status/blocked-and-deferred.md |
| What appears on the website? | CLRSLean.lean, chapter guides, and literate.toml |
CLRSLean/Progress.lean is generated from the CSV. It should never be edited
as an independent status ledger.
New code should import CLRSLean.FourthEdition.Chapter_NN. Existing
CLRSLean.Chapter_NN imports and public declarations are supported through all
1.x releases and for at least six months after the facade release. Removal
can occur only in 2.0 or later, after both gates have passed. See the
migration guide for shifted chapters, declaration
namespaces, and the exact cleanup policy.
Install Lean through elan, then prepare the repository:
git clone https://github.com/TankTechnology/CLRS-Lean.git
cd CLRS-Lean
lake exe cache get
uv sync --frozenThe Python helper environment is managed by uv; it currently has no runtime
dependencies beyond Python 3.11 or newer.
Build the Lean library:
lake build CLRSLeanRunning many agents or worktrees in parallel? Provision isolated, pre-built
worktrees with scripts/setup-worktree.sh so each skips the Mathlib download —
see docs/build-and-agents.md for the model, the
concurrency limits, and the recovery runbook.
Run the fast repository metadata and configuration checks:
uv run python scripts/check_repository.pyWebsite generation and deployment are separate publishing tasks. Run the Verso build only when the user explicitly requests publishing, release, or website work:
python3 scripts/apply_verso_patch.py
lake build :literate
python3 scripts/prepare_literate_module_map.py \
.lake/build/literate .lake/build/literate-module-map --prune-orphans
python3 scripts/plan_literate_shards.py \
.lake/build/literate-module-map .lake/build/literate-shards \
--shards 4 --digest-input lean-toolchain \
--digest-input lake-manifest.json --digest-input lakefile.lean \
--digest-input literate.toml
lake build verso-literate-html
python3 scripts/render_literate_shards.py \
--executable .lake/packages/verso/.lake/build/bin/verso-literate-html \
--module-map .lake/build/literate-module-map --config literate.toml \
--manifest .lake/build/literate-shards/manifest.json \
--output .lake/build/literate-shard-output --jobs 4
python3 scripts/merge_literate_shards.py \
.lake/build/literate-shards/manifest.json \
.lake/build/literate-html-merged \
.lake/build/literate-shard-output/shard-{0,1,2,3}
python3 scripts/check_literate_html_weight.py .lake/build/literate-html-merged
python3 scripts/check_literate_html_freshness.py .lake/build/literate-html-merged
python3 scripts/prepare_literate_site.py .lake/build/literate-html-merged _siteThe four renderers share a complete site graph but emit disjoint chapter-affine
module sets; --jobs is capped at four. The merger checks a content digest,
complete/unique module inventory, shared-file equality, and hover metadata
before replacing its destination. lake build :literateHtml remains a serial
diagnostic fallback. The tracked patches are idempotent and the raw-output
guard rejects residual tactic widgets and pages above 25 MiB. See the full
site architecture and recovery runbook.
For proof development, use the narrow-to-wide loop documented in
docs/workflows/lean-fast-verification.md
before running a full library build.
A theorem-producing change should update code and status together:
-
Change the relevant section module and its focused interface test.
-
Consult
docs/clrs-fourth-edition-map.csvand update the canonicalCLRSLean/FourthEdition/Chapter_NN.leanguide when the advertised boundary changes. -
Update
docs/clrs-proof-progress.csvanddocs/proof-map.mdwhen coverage changes. -
Regenerate the public dashboard and README progress table:
uv run python scripts/check_progress_csv.py --write-dashboard python3 scripts/gen_readme_table.py
-
Run
uv run python scripts/check_repository.py. -
Build the changed module, its immediate dependents, and finally
lake build CLRSLeanfor a milestone or merge.
Before a milestone merge or a deploy, run a full review with the
clrs-qa-reviewer agent (.claude/agents/clrs-qa-reviewer.md): it checks
format/convention consistency, verifies proofs are genuinely sorry-free via
#print axioms, and validates source navigation configuration. Rendered Verso
navigation is additionally inspected only for an explicitly requested
publishing, release, or website task. Because -Dwarn.sorry=false means a
clean build is not proof of soundness, the axiom check remains mandatory for
proof milestones. For running many proof agents in parallel, see
docs/build-and-agents.md (isolated prebuilt
worktrees, RAM-bound concurrency limits, and the recovery runbook).
Status labels describe the proved model precisely:
main-proof-complete: the advertised main theorem stack is complete.main-proof-complete-for-correctness: correctness is complete; explicit work/RAM refinements remain.selected-section-complete: the represented sections are complete, not the whole textbook chapter.partial: useful proofs exist, but a named central target remains.not-started: no represented section exists onmain.expository: a guide page with no formal theorem target.
The manually dispatched GitHub Pages workflow prepares immutable inputs once, renders four matrix shards in parallel, atomically validates/merges them, then checks, optimizes, and uploads one Pages artifact for one deployment. Neither workflow runs on every commit or pull request. Generated HTML is build output and is not committed to the repository.