1. CLRS-Lean
Imports
import CLRSLean.ProofPatterns import CLRSLean.Probability import CLRSLean.FourthEdition import CLRSLean.OnlineMaterial import CLRSLean.Chapter_01 import CLRSLean.Chapter_02 import CLRSLean.Chapter_03 import CLRSLean.Chapter_04 import CLRSLean.Chapter_05 import CLRSLean.Chapter_06 import CLRSLean.Chapter_07 import CLRSLean.Chapter_08 import CLRSLean.Chapter_09 import CLRSLean.Chapter_10 import CLRSLean.Chapter_11 import CLRSLean.Chapter_12 import CLRSLean.Chapter_13 import CLRSLean.Chapter_14 import CLRSLean.Chapter_15 import CLRSLean.Chapter_16 import CLRSLean.Chapter_17 import CLRSLean.Chapter_18 import CLRSLean.Chapter_19 -- Keep registered Chapter 19 compatibility pages in Verso's module set while -- the chapter aggregator itself exposes only canonical textbook sections. import CLRSLean.Chapter_19.Section_19_1_Fibonacci_Heap_Model.S1_ExecutableFibHeap import CLRSLean.Chapter_19.Section_19_1_Fibonacci_Heap_Model.S2_CascadingCuts import CLRSLean.Chapter_19.Section_19_1_Fibonacci_Heap_Model.S3_AmortizedCosts import CLRSLean.Chapter_20 import CLRSLean.Chapter_21 import CLRSLean.Chapter_22 import CLRSLean.Chapter_23 import CLRSLean.Chapter_24 import CLRSLean.Chapter_25 import CLRSLean.Chapter_26 import CLRSLean.Chapter_27 import CLRSLean.Chapter_28 import CLRSLean.Chapter_29 import CLRSLean.Chapter_30 import CLRSLean.Chapter_31 import CLRSLean.Chapter_32 import CLRSLean.Chapter_33 import CLRSLean.Chapter_34 import CLRSLean.Extensions import CLRSLean.Progress import CLRSLean.Status import CLRSLean.Workflow

CLRS-Lean

CLRS-Lean is a fourth-edition-primary Lean 4 companion for CLRS-style algorithm proofs. It is organized as an online book: canonical guides under CLRSLean.FourthEdition explain each formalization boundary, and current theorem-bearing source modules contain the definitions, executable models, interfaces, and proofs.

Project Aim

The first target is the mathematical content of CLRS: loop invariants, sortedness and permutation arguments, exchange proofs, cut properties, recurrences, optimal substructure, and graph-algorithm correctness. Pointer mutation, RAM costs, and line-by-line pseudocode refinement are separate layers unless a chapter's main theorem depends on them.

This distinction lets a chapter be complete for its advertised model without claiming that every implementation detail or exercise has been formalized.

Start Here

There are four useful reading routes:

  1. Algorithms: choose a fourth-edition chapter guide, read its scope, then follow its current source link to a represented section.

  2. Progress: open Progress Dashboard for the generated chapter matrix.

  3. Planning: open Proof Status for completed, partial, and missing proof groups.

  4. Contributing: open Workflow, then use the relevant chapter guide and focused interface test.

The Reusable CLRS proof patterns page collects the small cross-chapter APIs for boundary shifts, exchange certificates, fibers, and interval geometry.

Fourth-Edition Primary View

The canonical public chapter sequence is CLRS fourth edition, Chapters 1--35. docs/clrs-fourth-edition-map.csv owns the section-level bridge from that sequence to current theorem-bearing sources. All 35 chapter guides now point to represented source; the generated dashboard and proof-status page preserve the exact remaining partial boundary for Chapter 34. Third-edition-only Fibonacci heaps, van Emde Boas trees, computational geometry, and moved section material live under CLRSLean.OnlineMaterial. Progress counts are selected theorem inventories rather than counts of every fourth-edition textbook obligation.

Existing CLRSLean.Chapter_NN imports and declarations keep their current meanings through all 1.x releases and for at least six months after the facade release. They may be removed only in 2.0 or later, after both gates pass. See docs/migrations/clrs4.md for shifted chapter imports, current declaration namespaces, and the cleanup policy.

Status Meaning

  • main-proof-complete: the advertised theorem stack is complete for its current model.

  • main-proof-complete-for-correctness: correctness is complete, while explicit work or RAM refinement remains.

  • selected-section-complete: represented sections are complete; the entire textbook chapter is not claimed.

  • partial: useful proofs exist, but a central theorem or refinement target remains.

  • not-started: no represented section exists on the current main branch.

  • expository: the chapter is a guide with no theorem target.

The machine-readable source for chapter rows is docs/clrs-proof-progress.csv, interpreted through docs/clrs-fourth-edition-map.csv. The public Progress Dashboard is generated from the progress CSV. The longer maintainer theorem ledger is docs/proof-map.md.

Library Shape

  • CLRSLean.lean: library root and landing page.

  • CLRSLean/FourthEdition/Chapter_XX.lean: canonical chapter guide.

  • CLRSLean/OnlineMaterial.lean: online/supplementary compatibility catalog.

  • CLRSLean/ProofPatterns.lean: reusable pattern aggregator.

  • CLRSLean/Chapter_XX.lean: current compatibility source aggregator.

  • CLRSLean/Chapter_XX/Section_XX_Y_Name.lean: current formal source.

  • CLRSLean/Progress.lean: generated progress dashboard.

  • CLRSLean/Status.lean: reader-facing status interpretation.

  • CLRSLean/Workflow.lean: contributor workflow.

  • Tests/Chapter_XX_Interface.lean: public interface checks.

Chapter guides aggregate section modules. Section modules own formal facts. Interface tests protect the public surface. Progress prose never replaces a kernel-checked theorem.

Verification

For local repository checks:

  • uv run python scripts/check_repository.py

  • lake build CLRSLean

For a reader-facing or navigation change, also build the Verso site:

Run lake build :literateHtml.

Generated HTML is deployed by GitHub Actions and is not committed as source.