Workflow

CLRS-Lean uses a repeatable fourth-edition section workflow. The goal is to make future chapters easy to audit, easy to deploy, and pleasant to read while the current theorem sources migrate chapter by chapter.

Section Lifecycle

1. Textbook map.

2. Algorithm model.

3. Mathematical proof plan.

4. Lean theorem interface.

5. Lean proof.

6. Verification.

7. Progress and documentation update.

8. Repository and site verification.

1. Textbook Map

Start with docs/clrs-fourth-edition-map.csv and the corresponding CLRSLean.FourthEdition.Chapter_NN guide. Record the canonical section number, current source module, algorithm, main theorem-like claims, proof method, and any exercises or chapter-end problems. Never infer a fourth-edition section number from a legacy filename. Exercises are normally marked future-work until the main theorem interface is stable.

2. Algorithm Model

Choose the Lean model that exposes the proof cleanly. Prefer a mathematical model first: lists for sorting, finite sets for edge collections, abstract oracles for cycle tests, and recurrence functions for first-pass runtime arguments.

Implementation-level refinements such as arrays, heaps, priority queues, and union-find can refine the mathematical model later.

3. Mathematical Proof Plan

Write the proof as small claims before proving them in Lean. Typical patterns include:

• sortedness plus permutation preservation;

• loop invariant over a state relation;

• exchange argument;

• cut property;

• recurrence solution;

• optimal-substructure lower bound.

4. Lean Interface

Expose theorem names that a reader would search for. A section should have a small public surface even if the local proof needs many helper lemmas.

Example:

During the facade period, the canonical import is fourth-edition-prefixed but declarations can remain in their legacy namespace. The edition map owns that bridge until the chapter's source/namespace migration lands.

5. Lean Proof

Keep early proofs local and readable. Extract shared abstractions only after at least two sections need the same interface. This keeps the site from developing premature infrastructure that readers must understand before they can read a single algorithm.

6. Verification

Use narrow checks while editing, then a project-level build before publishing:

• lake env lean CLRSLean/Chapter_02/Section_02_1_Insertion_Sort.lean

• lake env lean Tests/Chapter_02_Interface.lean

• lake build

• lake build :literateHtml

When local literateHtml generation is too slow, the Lean build and static configuration checks still provide useful evidence, and the GitHub Pages build becomes the final deployment gate.

7. Progress And Documentation Update

Every user-facing section change should update the book structure:

• the relevant CLRSLean/FourthEdition/Chapter_XX.lean canonical guide;

• the current theorem-bearing source guide named by the edition map;

• literate.toml if a new module should appear in the navigation;

• docs/proof-map.md for the longer maintainer ledger;

• docs/clrs-proof-progress.csv when chapter coverage changes;

• docs/proof-status-board.md only when planning priorities change.

8. Progress CSV Update

The proof-progress CSV is the machine-readable fourth-edition chapter ledger for agents and the public dashboard. Any agent that changes reader-facing theorem coverage should consult docs/clrs-fourth-edition-map.csv and update docs/clrs-proof-progress.csv in the same commit.

Rule of thumb:

• new public theorem group: increment tracked_key_theorems and proved_tracked_theorems;

• closed gap: reduce edition_gap_units, update repo_status, and move the item from remaining_edition_gaps to proved_key_theorem_groups;

• new chapter or section page: update represented_sections, evidence_source, literate.toml, and the chapter guide page;

• deferred or blocked theorem group: record it in remaining_edition_gaps instead of silently dropping it.

Regenerate the dashboard after changing the CSV:

• uv run python scripts/check_progress_csv.py --write-dashboard

Compatibility Policy

Existing unqualified CLRSLean.Chapter_NN imports and public declarations remain supported through all 1.x releases and for at least six months after the facade release. Removal is possible only in 2.0 or later, after both gates pass. New work should use the fourth-edition guide import; see docs/migrations/clrs4.md for source and namespace mappings.

9. Repository And Site Verification

Before committing proof-status changes, run:

• uv run python scripts/check_repository.py

• lake build CLRSLean

Run lake build :literateHtml and generated-site checks only for an explicit publishing, release, or website task.