Progress Dashboard
CLRS-Lean represents all 35 fourth-edition chapters and proves
all 1,689 of its 1,689 selected reader-facing theorem entries.
These are scope-qualified inventory counts, not a claim that every paragraph,
exercise, implementation model, or textbook problem has been formalized.
The machine-readable source of truth is docs/clrs-proof-progress.csv.
Fourth-Edition Snapshot
This is the canonical CLRS fourth-edition chapter ledger. Reused third-edition theorem sources remain compatibility evidence, not an alternative chapter-numbering scheme. Legacy imports remain supported through all 1.x releases and for at least six months; removal is possible only in 2.0 or later.
-
Fourth-edition chapters tracked: 35.
-
Chapters represented in Lean: 35.
-
Tracked reader-facing theorem entries: 1,689.
-
Proved tracked theorem entries: 1,689.
-
Online/supplementary theorem entries: 470.
-
Remaining edition-coverage units: 0.
Tracked theorem entries form a selected proof inventory of reviewed groups mapped
to represented fourth-edition sections. A complete proved/tracked count does not
by itself mean that every fourth-edition section obligation is covered. Moved
subsections and wholly excluded legacy chapters are counted only
in the machine-readable online-material ledger. This produces disjoint canonical and online-material ledgers;
compatibility imports do not duplicate either count.
An edition-coverage unit is one unresolved section in a represented chapter,
or one whole-chapter unit when no section of that chapter is represented.
The status partial means partial fourth-edition coverage, even when
every theorem already selected for that chapter is proved.
Status Counts
-
main-proof-complete: 34 chapters. -
expository: 1 chapter.
Chapter Matrix
| Ch | Chapter | Status | Sections | Tracked | Gap units |
|---|---|---|---|---|---|
| 1 | 1. The Role of Algorithms in Computing | expository | Chapter_01 | 0 | 0 |
| 2 | 2. Getting Started | main-proof-complete | 2.1;2.2;2.3 | 20 | 0 |
| 3 | 3. Characterizing Running Times | main-proof-complete | 3.1;3.2;3.3 | 71 | 0 |
| 4 | 4. Divide-and-Conquer | main-proof-complete | 4.1;4.2;4.3;4.4;4.5;4.6;4.7 | 104 | 0 |
| 5 | 5. Probabilistic Analysis and Randomized Algorithms | main-proof-complete | 5.1;5.2;5.3;5.4 | 26 | 0 |
| 6 | 6. Heapsort | main-proof-complete | 6.1;6.2;6.3;6.4;6.5 | 85 | 0 |
| 7 | 7. Quicksort | main-proof-complete | 7.1;7.2;7.3;7.4 | 34 | 0 |
| 8 | 8. Sorting in Linear Time | main-proof-complete | 8.1;8.2;8.3;8.4 | 58 | 0 |
| 9 | 9. Medians and Order Statistics | main-proof-complete | 9.1;9.2;9.3 | 72 | 0 |
| 10 | 10. Elementary Data Structures | main-proof-complete | 10.1;10.2;10.3 | 21 | 0 |
| 11 | 11. Hash Tables | main-proof-complete | 11.1;11.2;11.3;11.4;11.5 | 62 | 0 |
| 12 | 12. Binary Search Trees | main-proof-complete | 12.1;12.2;12.3 | 44 | 0 |
| 13 | 13. Red-Black Trees | main-proof-complete | 13.1;13.2;13.3;13.4 | 40 | 0 |
| 14 | 14. Dynamic Programming | main-proof-complete | 14.1;14.2;14.3;14.4;14.5 | 90 | 0 |
| 15 | 15. Greedy Algorithms | main-proof-complete | 15.1;15.2;15.3;15.4 | 40 | 0 |
| 16 | 16. Amortized Analysis | main-proof-complete | 16.1;16.2;16.3;16.4 | 69 | 0 |
| 17 | 17. Augmenting Data Structures | main-proof-complete | 17.1;17.2;17.3 | 79 | 0 |
| 18 | 18. B-Trees | main-proof-complete | 18.1;18.2;18.3 | 147 | 0 |
| 19 | 19. Data Structures for Disjoint Sets | main-proof-complete | 19.1;19.2;19.3;19.4 | 84 | 0 |
| 20 | 20. Elementary Graph Algorithms | main-proof-complete | 20.1;20.2;20.3;20.4;20.5 | 50 | 0 |
| 21 | 21. Minimum Spanning Trees | main-proof-complete | 21.1;21.2 | 52 | 0 |
| 22 | 22. Single-Source Shortest Paths | main-proof-complete | 22.1;22.2;22.3;22.4;22.5 | 31 | 0 |
| 23 | 23. All-Pairs Shortest Paths | main-proof-complete | 23.1;23.2;23.3 | 29 | 0 |
| 24 | 24. Maximum Flow | main-proof-complete | 24.1;24.2;24.3;24.4;24.5 | 35 | 0 |
| 25 | 25. Matchings in Bipartite Graphs | main-proof-complete | 25.1;25.2;25.3 | 18 | 0 |
| 26 | 26. Parallel Algorithms | main-proof-complete | 26.1;26.2;26.3 | 95 | 0 |
| 27 | 27. Online Algorithms | main-proof-complete | 27.1;27.2;27.3 | 10 | 0 |
| 28 | 28. Matrix Operations | main-proof-complete | 28.1;28.2;28.3 | 13 | 0 |
| 29 | 29. Linear Programming | main-proof-complete | 29.1;29.2;29.3 | 10 | 0 |
| 30 | 30. Polynomials and the FFT | main-proof-complete | 30.1;30.2;30.3 | 34 | 0 |
| 31 | 31. Number-Theoretic Algorithms | main-proof-complete | 31.1;31.2;31.3;31.4;31.5;31.6;31.7;31.8 | 18 | 0 |
| 32 | 32. String Matching | main-proof-complete | 32.1;32.2;32.3;32.4;32.5 | 61 | 0 |
| 33 | 33. Machine-Learning Algorithms | main-proof-complete | 33.1; 33.2; 33.3 | 15 | 0 |
| 34 | 34. NP-Completeness | main-proof-complete | 34.1;34.2;34.3;34.4;34.5 | 59 | 0 |
| 35 | 35. Approximation Algorithms | main-proof-complete | 35.1;35.2;35.3;35.4;35.5 | 13 | 0 |
Agent Update Rule
Every theorem-producing agent should treat this table as part of the proof
artifact, not as a separate report. If a contribution adds, removes,
renames, strengthens, or finishes a reader-facing theorem group, update
docs/clrs-proof-progress.csv in the same commit. If the change
alters the public snapshot or chapter rows, regenerate this page before
building the site.
Minimum maintenance loop:
-
Consult
docs/clrs-fourth-edition-map.csv, then update the relevant Lean files anddocs/clrs-proof-progress.csv. -
Regenerate this page with
uv run python scripts/check_progress_csv.py --write-dashboard. -
Run
lake build CLRSLean; for explicit website publishing, use the four-shard runbook indocs/site-architecture.md. The seriallake build :literateHtmltarget is a diagnostic fallback.