Skip to content
  1. CLRS-Lean
  2. Proof Status
Browse chapters

Proof Status

This page gives a concise reader-facing interpretation of CLRS-Lean's canonical fourth-edition proof state. The generated Progress Dashboard owns chapter counts and status rows; docs/clrs-fourth-edition-map.csv owns the bridge to current theorem-bearing sources; section modules and interface tests own formal truth; and docs/scope.md records the project-wide claim boundary.

Whole-Book Snapshot

The canonical ledger contains 35 chapter rows. All 35 chapters are represented in Lean: 34 chapters are main-proof-complete for their advertised models, and Chapter 1 is expository. No chapter remains partial or not-started, and the generated dashboard reports all 1,689 selected reader-facing theorem entries proved with zero edition-coverage gap units.

This is a selected, reviewed theorem inventory. It does not claim every exercise, chapter-end Problem, pointer/RAM model, or floating-point implementation. The generated dashboard owns the live totals; this page explains how to read them.

The September 8 source audit and its chapter-by-chapter repair record are kept separately in docs/audits/2026-09-08-chapter-review/ and docs/plans/2026-09-08-chapter-repairs/. The original audit describes its base commit; the repair record links later execution refinements, regressions, and clarified cost models. It does not establish an independent page-by-page verification against the textbook.

Edition And Compatibility Contract

Chapter numbers on this page mean CLRS fourth edition. New work should import CLRSLean.FourthEdition.Chapter_NN. Existing unqualified CLRSLean.Chapter_NN imports and their public declarations keep their third-edition meanings 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. Declaration namespaces migrate chapter by chapter; docs/migrations/clrs4.md records the current mapping.

Status Labels

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

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

  • selected-section-complete: represented sections are complete without a claim about the unrepresented remainder of the chapter.

  • partial: meaningful theorem infrastructure exists, but the edition map names a central textbook theorem, section, or refinement gap.

  • not-started: no section is represented in the canonical chapter.

  • expository: a guide page with no theorem target.

The proved/tracked fraction is a selected proof-inventory metric. Even a complete fraction can accompany partial when the fourth-edition map names an obligation that has not yet been selected into that inventory.

Chapter 34 Flagship

Chapter 34 is now main-proof-complete at its advertised boundary. Section 34.5 closes the selected textbook chain through VERTEX-COVER, HAM-CYCLE, decision-TSP, and SUBSET-SUM. Each public decision problem has its honest serialized language and certificate interface, fixed polynomial-time reduction and verifier machines, exact semantic bridge, and NP-completeness wrapper.

  • Sections 34.1--34.3 provide the complexity framework, P ⊆ NP, and polynomial-reduction infrastructure.

  • Section 34.4 closes the semantic Cook--Levin tableau circuit, polynomial size bounds, exact function-level reduction, and fixed polynomial-time TM2; cookLevin_theorem and generalCircuitSAT_npComplete are the public closure points.

  • The concrete chain continues through SAT, 3-CNF-SAT, and honest general graph-plus-k CLIQUE, including fixed verifiers and reduction machines.

  • Section 34.5 closes VERTEX-COVER, HAM-CYCLE, decision-TSP, and SUBSET-SUM with exact semantic bridges, bounded certificates, fixed machines, and the public VERTEXCOVER_npComplete, HAMCYCLE_npComplete, TSP_npComplete, and SUBSETSUM_npComplete theorems.

SAT and 3-CNF-SAT have exact raw certificate checkers and reduction-backed fixed verifier machines. Direct machine lowerings of the smaller assignment checkers, and direct concrete machines for the empty and universal languages, remain optional refinements; they do not reopen the chapter boundary. The Chapter 34 guide and section pages own the construction-level details.

The canonical ledger currently classifies every theorem-bearing chapter as main-proof-complete for its advertised model; Chapter 1 is expository. That label applies only to the represented fourth-edition sections, never automatically to exercises, chapter-end Problems, pointer/RAM models, or floating-point implementations.

Chapter 2 now includes the complete symbolic insertion-sort line-cost table: all seven cᵢ contributions, their trace-derived execution counts, and exact best/worst substitutions. It also includes a local executable MERGE whose bundled contract proves sortedness, exact permutation preservation, a linear head-comparison bound, and exactly one output write per input element. Operational mutable-array and word-RAM semantics remain lower-level refinements rather than implied by these symbolic cost theorems.

Chapter 6 now exposes checked active-prefix MAX-HEAP-INSERT: it rejects only an oversized heap prefix, preserves any inactive backing-list tail, grows the heap and backing list by one, and adds exactly the requested key. Its costed wrapper erases to the same operation and proves an explicit logarithmic bound on visited upward-bubbling frames. Persistent-list and RAM instruction costs are not included in that metric.

Chapter 15 closes all eleven findings from its semantic-fidelity audit. The activity-selection development now has the textbook input predicate, iterative algorithm, and exact scan count; the generic greedy framework separates its two structural properties and is instantiated back to activity selection; Huffman has equation (15.4), separate Lemma 15.2/15.3 interfaces, and honest list/heap cost layers; offline caching includes literal-empty-start optimality through CLRS.Caching.fifo_optimal_from_empty.

Online And Supplementary Material

The separate CLRSLean.OnlineMaterial catalog retains 470 tracked theorem groups: 426 from the three wholly excluded third-edition Chapters 19, 20, and 33, plus 44 from moved section-level developments such as maximum subarray, matroids and task scheduling, detailed SIMPLEX, iterative FFT, and integer factorization. Those 44 groups are disjoint from the 1,689 canonical tracked theorem entries. docs/clrs-online-material.csv owns the topic-level counts and source modules; compatibility imports do not duplicate either ledger.

Reader Contract

A proved or complete label always refers to a named Lean theorem for an explicit model. A partial label names the remaining mathematical or representation layer. Compatibility facades preserve theorem availability; they do not by themselves prove every obligation in the new edition. Dated audits are historical evidence rather than live status sources.