1. CLRS-Lean
Imports
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 import CLRSLean.Chapter_20 import CLRSLean.Chapter_23 import CLRSLean.Progress import CLRSLean.Status import CLRSLean.Workflow

CLRS-Lean

CLRS-Lean is a Lean 4 companion to CLRS-style algorithm proofs. The project is organized as a readable online book: each chapter has a short guide page, and each selected textbook section has a literate Lean page containing the formal model, the public theorem interface, and the proof.

Project Aim

The goal is not to mechanically translate pseudocode line by line. The first target is the mathematical proof content of the textbook: loop invariants, exchange arguments, cut properties, recurrences, and optimal-substructure claims. Low-level implementation proofs, such as union-find or heap correctness, are added only when they are needed for the main theorem.

This keeps the site useful for three kinds of readers:

  • algorithm readers who want the proof idea before reading Lean code;

  • Lean readers who want stable theorem names and proof patterns;

  • contributors who need an honest map of what is proved, partial, or deferred.

Reading Route

Start with the chapter pages in the sidebar.

  • Chapter 1 - Algorithms: the project reading contract and the way CLRS-Lean turns textbook claims into Lean definitions plus theorems.

  • Chapter 2 - Getting Started: sorting correctness, a lightweight runtime bound, and a merge-sort recurrence.

  • Chapter 3 - Growth of Functions: CLRS-style wrappers around Mathlib asymptotics plus selected standard growth facts.

  • Chapter 4 - Divide-and-Conquer: maximum-subarray specification correctness, recurrence proof infrastructure for the substitution and recursion-tree methods, Strassen's 2 by 2 block algebra correctness, plus the proved exact-power Master method core, floor/ceiling exact-power extraction, and all-input transfer bridge with adjacent-power sandwich generation, discrete Master-scale wrappers, natural-exponent polynomial wrappers for Master cases 1 and 2, the real-log bridge from a^(⌊log_b n⌋) to n^(log_b a), and named case-1/case-2 wrappers in textbook n^(log_b a) and n^(log_b a) log n scales.

  • Chapter 5 - Probabilistic Analysis: the finite rank-symmetry proof for the hiring problem and its logarithmic expected-hires bound.

  • Chapter 6 - Heapsort: recursive MAX-HEAPIFY repair, bottom-up BUILD-MAX-HEAP, the in-place heapsort loop with a proved sorted-suffix invariant and sortedness theorem, an indexed array heap proof spine, and priority-queue operation specifications.

  • Chapter 7 - Quicksort: stable functional partition classification, scan-state partition-loop correctness, a returned pivot-index partition wrapper with an explicit adjacent-swap trace, functional quicksort sortedness/permutation preservation, a deterministic quadratic comparison-count bound, and the expected-comparison recurrence with harmonic bounds for the current randomized-quicksort model.

  • Chapter 8 - Sorting in Linear Time: stable counting-sort bucket correctness, abstract radix-sort correctness and complete digit-signature stability from stable digit passes, a concrete base-b digit wrapper for natural-key radix sort, a key-order correctness wrapper with the one-digit arithmetic case discharged, deterministic bucket-sort correctness, and the finite-uniform collision/second-moment core for bucket-sort expected time.

  • Chapter 9 - Medians and Order Statistics: selection-by-rank correctness for the specification selector, pivot-style quickselect, and pivot-parametric deterministic SELECT via a count-based order-statistic certificate, plus an executable median-of-medians pivot/select wrapper, the local five-element median certificate, executable five-element grouping, median-of-medians partition-size bounds, and the abstract linear recurrence wrapper.

  • Chapter 10 - Elementary Data Structures: functional stack, queue, and linked-list operation proofs.

  • Chapter 11 - Hash Tables: direct-address table correctness, deterministic chained-hash-table insert/delete/search facts, and a finite-uniform bucket interface proving expected chain length equals the load factor.

  • Chapter 12 - Binary Search Trees: search, minimum/maximum, insertion, complete functional successor/predecessor specifications, Boolean search wrappers after insertion/deletion, and functional deletion correctness for an inductive BST model.

  • Chapter 13 - Red-Black Trees: local rotation, recoloring, red-red repair, four insertion-fixup case certificates, and red-black shape invariant lemmas.

  • Chapter 14 - Augmenting Data Structures: order-statistic tree size augmentation, size/rank-preserving local rotations, and rank-selection correctness for the current functional model.

  • Chapter 15 - Dynamic Programming: rod-cutting Bellman recurrence facts, matrix-chain parenthesization optimality plus split-table reconstruction, and LCS certificate optimality plus table-recurrence reconstruction certificates and recurrence wrappers.

  • Chapter 16 - Greedy Algorithms: activity-selection exchange infrastructure and the complete Huffman optimality proof, currently the flagship greedy case study.

  • Chapter 17 - Amortized Analysis: finite-prefix aggregate, accounting, and potential-method telescoping theorems, plus stack/counter/table examples with an executable multi-step counter trace bound and size-level dynamic-table potential, actual-cost and capacity-choice case specs, capacity-direction, actual-cost lower/upper bounds, post-state field equations, stored-count direction, positive insertion/deletion count/capacity wrappers, post-state capacity, post-transition potential, concrete amortized-cost unfolding, resize-branch capacity wrappers, exact zero/positive deletion-cost wrappers, premise-light deletion-cost branch wrappers, and transition wrappers.

  • Chapter 18 - B-Trees: first-pass mathematical B-tree membership, search, direct base search success/failure wrappers, height-expression base/positivity/recurrence/monotonicity, split-child direct validity and membership/search preservation, direct failed-membership preservation, insertion/deletion direct validity, equality-key query wrappers, successful/unsuccessful search-after-update theorem surface, Prop-level deletion success wrappers, membership-driven search-after-update wrappers, and direct inserted/deleted-key, old-key query preservation, and failed membership corollaries.

  • Chapter 19 - Fibonacci Heaps: abstract finite-set heap model with make-heap, operation-level correctness, direct operation-result validity for normalized counters, direct insert/union/extract-min/decrease-key/delete membership facts plus operation-key, old-key preservation, failed membership corollaries, and direct failed-membership preservation wrappers, returned minimum-after-update positive/empty specs plus direct minimum/extract-min empty-result and nonempty-result wrappers, remaining/delete minimum nonempty-result wrappers, insert/union/extract-min-remaining/decrease-key/delete minimum direct membership/lower-bound wrappers, heap potential zero/nonnegativity and telescoping facts, a Fibonacci lower-bound recurrence with positivity, monotonicity, and even/half-index power-of-two growth facts, conditional degree-to-binary-log wrappers, and a conservative degree-bound wrapper.

  • Chapter 20 - van Emde Boas Trees: high/low universe decomposition with bounded recomposition facts and a finite-set specification layer for membership, extrema, successor, predecessor, successful-query universe bounds, empty-result extrema/successor/predecessor queries, insert, and delete, including membership-, extrema-, and neighbor-query-after-update positive/no-neighbor specs, direct no-neighbor query wrappers, extrema empty-after-update specs, direct extrema empty-result wrappers, direct base extrema/neighbor nonempty-result wrappers, direct updated-neighbor nonempty-result wrappers, direct deletion-extrema nonempty-result wrappers, direct extrema membership/lower- and upper-bound wrappers, direct extrema-after-update membership/order wrappers, direct base/insert/delete neighbor membership/order wrappers, premise-light no-neighbor wrappers over old represented sets, member-query preservation and failure corollaries, direct failed member-query preservation wrappers, update-query universe-bound corollaries, and operation-depth recurrence/monotonicity specs.

  • Chapter 23 - Minimum Spanning Trees: the MST cut property, the mathematical Kruskal skeleton, and finite-graph MST wrappers.

  • Progress Dashboard: a compact, generated chapter-by-chapter view of current coverage, backed by docs/clrs-proof-progress.csv.

  • Proof Status: a planning board plus a compact ledger of proved, partial, blocked, and deferred work.

  • Workflow: the contribution loop for adding or strengthening a CLRS section.

Current Coverage

  • Chapter 1: expository. No theorem target; this page explains the project conventions.

  • 2.1 Insertion sort: proved. Public results: CLRS.Chapter02.insertionSort_sorted, CLRS.Chapter02.insertionSort_perm.

  • 2.2 Analyzing algorithms: proved. Public result: CLRS.Chapter02.insertionSortWorstComparisons_quadratic.

  • 2.3 Designing algorithms: proved. Public results: CLRS.Chapter02.mergeSort_sortedLE, CLRS.Chapter02.mergeSort_perm, CLRS.Chapter02.mergeSortRecurrenceOnPowersOfTwo_closedForm.

  • 3.1 Asymptotic notation: proved. Public results: CLRS.Chapter03.isBigO_iff, CLRS.Chapter03.isLittleO_iff, CLRS.Chapter03.isBigTheta_trans.

  • 3.2 Standard functions: partial. Current results: CLRS.Chapter03.isLittleO_pow_pow, CLRS.Chapter03.isLittleO_pow_const_exp, CLRS.Chapter03.isLittleO_log_rpow, CLRS.Chapter03.isLittleO_log_pow_rpow, CLRS.Chapter03.isBigO_log_pow_rpow, CLRS.Chapter03.isLittleO_exp_exp_of_lt, CLRS.Chapter03.isEquivalent_harmonic_log, CLRS.Chapter03.isBigTheta_harmonic_log, CLRS.Chapter03.isBigTheta_nat_floor_coerce, CLRS.Chapter03.isBigTheta_nat_ceil_coerce, CLRS.Chapter03.isBigTheta_nat_floor_half_coerce, CLRS.Chapter03.isBigTheta_nat_ceil_half_coerce, CLRS.Chapter03.factorial_upper_bound, CLRS.Chapter03.factorial_lower_bound_offset, CLRS.Chapter03.factorial_lower_bound_half_pow, CLRS.Chapter03.isLittleO_exp_vs_factorial, CLRS.Chapter03.isLittleO_factorial_pow_self.

  • 4.1 Maximum subarray: proved for the exhaustive-search specification, crossing helper, and left/right/crossing combine interface. Public results: CLRS.Chapter04.mem_nonemptySubarrays_iff, CLRS.Chapter04.bestCandidate_correct, CLRS.Chapter04.mem_crossingSubarrays_iff, CLRS.Chapter04.maxCrossingSubarray_correct, CLRS.Chapter04.maxCrossingSubarray_isNonemptySubarray_append, CLRS.Chapter04.subarray_append_left_or_right_or_crossing, CLRS.Chapter04.subarray_append_optimal_of_cases, CLRS.Chapter04.maxSubarray_exists_of_ne_nil, CLRS.Chapter04.maxSubarray_correct.

  • 4.2 Strassen's algorithm: proved for 2 by 2 block algebra. Public result: CLRS.Chapter04.strassen2x2_correct.

  • 4.3 Substitution method: proved for one-step recurrence bounds. Public results: CLRS.Chapter04.substitution_upper_bound, CLRS.Chapter04.substitution_lower_bound, CLRS.Chapter04.linear_substitution_upper_bound, CLRS.Chapter04.geometric_substitution_upper_bound.

  • 4.4 Recursion-tree method: proved for additive level-cost expansions. Public results: CLRS.Chapter04.recursion_tree_additive_unroll, CLRS.Chapter04.recursion_tree_additive_upper_envelope, CLRS.Chapter04.recursion_tree_constant_level_cost.

  • 4.5 Master method: proved for exact-power recurrences. Public results: CLRS.Chapter04.master_case1_geometric, CLRS.Chapter04.master_case2_constant_forcing, CLRS.Chapter04.master_case3_tail_dominated.

  • 4.6 Proof of the master theorem: partial. Current results: CLRS.Chapter04.FloorDivideRecurrence, CLRS.Chapter04.CeilDivideRecurrence, CLRS.Chapter04.exactPowerRecurrence_of_floorDivideRecurrence, CLRS.Chapter04.exactPowerRecurrence_of_ceilDivideRecurrence, CLRS.Chapter04.powerInterval_of_pos, CLRS.Chapter04.eventuallyPowerUpperSandwich_of_powerStep, CLRS.Chapter04.eventuallyPowerLowerSandwich_of_powerStep, CLRS.Chapter04.allInput_bigO_of_power_upper_sandwich, CLRS.Chapter04.allInput_bigOmega_of_power_lower_sandwich, CLRS.Chapter04.allInput_bigTheta_of_power_sandwich, and CLRS.Chapter04.allInput_bigTheta_of_powerStep, CLRS.Chapter04.criticalPowerScale, and CLRS.Chapter04.allInput_bigTheta_of_criticalPowerScale, CLRS.Chapter04.criticalPowerLogScale, CLRS.Chapter04.allInput_bigTheta_of_criticalPowerLogScale, CLRS.Chapter04.tailDominatedScale, CLRS.Chapter04.allInput_bigTheta_of_tailDominatedScale, CLRS.Chapter04.polynomialScale, CLRS.Chapter04.polynomialLogScale, CLRS.Chapter04.criticalPowerScale_isBigTheta_polynomialScale, CLRS.Chapter04.criticalPowerLogScale_isBigTheta_polynomialLogScale, CLRS.Chapter04.realLogExponent, CLRS.Chapter04.realLogScale, CLRS.Chapter04.criticalPowerScale_isBigTheta_realLogScale, CLRS.Chapter04.realLogLogScale, CLRS.Chapter04.criticalPowerLogScale_isBigTheta_realLogLogScale, CLRS.Chapter04.exactPower_allInput_masterCase1_criticalPowerScale, CLRS.Chapter04.floorDivide_allInput_masterCase1_criticalPowerScale, and CLRS.Chapter04.ceilDivide_allInput_masterCase1_criticalPowerScale; CLRS.Chapter04.exactPower_allInput_masterCase1_realLogScale, CLRS.Chapter04.floorDivide_allInput_masterCase1_realLogScale, and CLRS.Chapter04.ceilDivide_allInput_masterCase1_realLogScale; CLRS.Chapter04.exactPower_allInput_masterCase1_polynomialScale, CLRS.Chapter04.floorDivide_allInput_masterCase1_polynomialScale, and CLRS.Chapter04.ceilDivide_allInput_masterCase1_polynomialScale; CLRS.Chapter04.exactPower_allInput_masterCase2_criticalPowerLogScale, CLRS.Chapter04.floorDivide_allInput_masterCase2_criticalPowerLogScale, and CLRS.Chapter04.ceilDivide_allInput_masterCase2_criticalPowerLogScale; CLRS.Chapter04.exactPower_allInput_masterCase2_realLogLogScale, CLRS.Chapter04.floorDivide_allInput_masterCase2_realLogLogScale, and CLRS.Chapter04.ceilDivide_allInput_masterCase2_realLogLogScale; CLRS.Chapter04.exactPower_allInput_masterCase2_polynomialLogScale, CLRS.Chapter04.floorDivide_allInput_masterCase2_polynomialLogScale, and CLRS.Chapter04.ceilDivide_allInput_masterCase2_polynomialLogScale; CLRS.Chapter04.exactPower_allInput_masterCase3_tailDominatedScale, CLRS.Chapter04.floorDivide_allInput_masterCase3_tailDominatedScale, and CLRS.Chapter04.ceilDivide_allInput_masterCase3_tailDominatedScale. Remaining target: the case-3 comparison scale for the forcing-dominated Master statement.

  • 5.1 Hiring problem: proved for the finite rank-symmetry model. Public results: CLRS.Chapter05.hireProbability_eq, CLRS.Chapter05.expectedHiresByIndicators_eq_harmonic, CLRS.Chapter05.expectedHires_isBigTheta_log.

  • 6.1 Heaps: proved for the indexed heap predicate and root maximum. Public results: CLRS.Chapter06.parent_lt_self, CLRS.Chapter06.eq_left_or_right_parent, CLRS.Chapter06.ArrayMaxHeap.getElem_le_root, CLRS.Chapter06.orderedDesc_arrayMaxHeap.

  • 6.2 Maintaining the heap property: proved for fuelled MAX-HEAPIFY recursive repair. Public results: CLRS.Chapter06.swapAt_perm, CLRS.Chapter06.maxHeapifyFuel_perm, CLRS.Chapter06.valAt_i_le_maxChildIndex, CLRS.Chapter06.arrayMaxHeap_of_except_of_maxChildIndex_self, CLRS.Chapter06.maxHeapifyFuel_swap_branch_repair, CLRS.Chapter06.maxHeapifyFuel_repair_subtree, CLRS.Chapter06.maxHeapifyFuel_root_isMaxHeap.

  • 6.3 Building a heap: proved for bottom-up repeated heapify. Public results: CLRS.Chapter06.buildMaxHeapLoop_isMaxHeap, CLRS.Chapter06.buildMaxHeapLoop_perm, CLRS.Chapter06.arrayBuildMaxHeap_isMaxHeap, CLRS.Chapter06.arrayBuildMaxHeap_correct.

  • 6.4 The heapsort algorithm: proved for the in-place CLRS loop refinement. Public results: CLRS.Chapter06.arrayHeapSortInPlaceLoop_perm, CLRS.Chapter06.arrayHeapSortInPlaceLoop_length, CLRS.Chapter06.arrayHeapSortInPlace_perm, CLRS.Chapter06.arrayHeapSortInPlace_length, CLRS.Chapter06.arrayHeapSortStep_suffix_head_eq_root, CLRS.Chapter06.arrayHeapSortStep_suffix_head_bounds_prefix, CLRS.Chapter06.HeapSortLoopInvariant.step, CLRS.Chapter06.arrayHeapSortStep_state_correct, CLRS.Chapter06.arrayHeapSortInPlaceLoop_terminal_invariant, CLRS.Chapter06.arrayHeapSortInPlaceLoop_orderedAsc, CLRS.Chapter06.arrayHeapSortInPlaceLoop_state_correct, CLRS.Chapter06.arrayHeapSortInPlaceLoop_exact_state_correct, CLRS.Chapter06.arrayHeapSortInPlace_terminal_invariant, CLRS.Chapter06.arrayHeapSortInPlace_orderedAsc, CLRS.Chapter06.arrayHeapSortInPlace_state_correct, CLRS.Chapter06.arrayHeapSortInPlace_exact_state_correct, CLRS.Chapter06.arrayHeapSortInPlace_correct, CLRS.Chapter06.arrayHeapSort_terminal_invariant, CLRS.Chapter06.arrayHeapSort_state_correct, CLRS.Chapter06.arrayHeapSort_exact_state_correct, CLRS.Chapter06.arrayHeapSort_orderedAsc, CLRS.Chapter06.arrayHeapSort_perm, CLRS.Chapter06.arrayHeapSort_correct.

  • 6.5 Priority queues: proved for the functional heap interface plus array-level HEAP-MAXIMUM, full fuelled HEAP-INCREASE-KEY, and HEAP-EXTRACT-MAX / HEAP-DELETE. Public results: CLRS.Chapter06.heapInsert_orderedDesc, CLRS.Chapter06.heapInsert_perm, CLRS.Chapter06.heapIncreaseKey_orderedDesc, CLRS.Chapter06.heapDelete_orderedDesc, CLRS.Chapter06.arrayHeapMaximum?_max, CLRS.Chapter06.ArrayMaxHeap.set_increased_except_up, CLRS.Chapter06.ArrayMaxHeapExceptUp.bubble_step, CLRS.Chapter06.ArrayMaxHeapExceptUp.bubbleUpFuel_global, CLRS.Chapter06.arrayHeapIncreaseKey?_state_correct, CLRS.Chapter06.arrayHeapIncreaseKeyNoBubble?_state_correct, CLRS.Chapter06.arrayHeapExtractMax?_state_correct, CLRS.Chapter06.arrayHeapDelete?_state_correct.

  • 7.1 Description of quicksort: proved for the functional-list model, scan-state partition loop, and returned pivot-index wrapper with an explicit adjacent-swap trace. Public results: CLRS.Chapter07.partitionAround_left_eq_filter, CLRS.Chapter07.partitionAround_right_eq_filter, CLRS.Chapter07.mem_partitionAround_left_iff, CLRS.Chapter07.mem_partitionAround_right_iff, CLRS.Chapter07.partitionAround_correct, CLRS.Chapter07.partitionAround_perm, CLRS.Chapter07.partitionAround_left_allLeUpper, CLRS.Chapter07.partitionAround_right_allGt, CLRS.Chapter07.AdjacentSwapTrace.to_perm, CLRS.Chapter07.AdjacentSwapTrace.of_perm, CLRS.Chapter07.partitionLoop_invariant, CLRS.Chapter07.partitionLoop_correct, CLRS.Chapter07.clrsPartition_correct, CLRS.Chapter07.clrsPartitionArray_pivot, CLRS.Chapter07.clrsPartitionArray_left_bound, CLRS.Chapter07.clrsPartitionArray_right_bound, CLRS.Chapter07.clrsPartitionArray_perm, CLRS.Chapter07.clrsPartitionArray_swapTrace, CLRS.Chapter07.clrsPartitionArray_correct, CLRS.Chapter07.clrsPartitionArray_correct_with_trace, CLRS.Chapter07.quickSort_perm, CLRS.Chapter07.quickSort_ordered, CLRS.Chapter07.quickSort_correct.

  • 7.2 Performance of quicksort: proved for the current deterministic comparison-count model. Public results: CLRS.Chapter07.partitionAround_length_add, CLRS.Chapter07.quickSortComparisonsFuel_quadratic, and CLRS.Chapter07.quickSortComparisons_quadratic.

  • 7.3 Randomized quicksort: proved for the expected-comparison recurrence, closed-form telescope, and harmonic upper bound in the current recurrence model. Public results: CLRS.Chapter07.expectedComparisons_recurrence, CLRS.Chapter07.expectedComparisons_telescope, CLRS.Chapter07.expectedComparisons_harmonic_bound, CLRS.Chapter07.expectedComparisons_quadratic, and CLRS.Chapter07.expectedComparisons_monotone.

  • 7.4 Quicksort analysis refinements: future-work. Planned targets: index-level mutable-array PARTITION, an explicit probability space for pivot choices, sharper n log n tail bounds, and lower-bound packaging.

  • 8.2 Counting sort: proved for the stable bucket specification. Public results: CLRS.Chapter08.countingSortBy_ordered, CLRS.Chapter08.countingSortBy_bucket_eq, CLRS.Chapter08.countingSortBy_mem_iff, CLRS.Chapter08.countingSortBy_perm, and CLRS.Chapter08.countingSortBy_correct.

  • 8.3 Radix sort: proved for the abstract stable digit-pass model with complete digit-signature stability plus a concrete base-b natural-key wrapper, including key-order packaging and the bounded fixed-width arithmetic bridge. Public results: CLRS.Chapter08.radixPass_orderedRel, CLRS.Chapter08.radixSortBy_ordered, CLRS.Chapter08.radixSortBy_stable, CLRS.Chapter08.radixSortBy_mem_iff, CLRS.Chapter08.radixSortBy_perm, CLRS.Chapter08.radixSortBy_correct_stable, CLRS.Chapter08.baseDigitsLow_allDigitsLe, CLRS.Chapter08.radixSortNatBy_correct_stable, CLRS.Chapter08.radixSortNatBy_correct_keyOrdered_of_digitOrder, CLRS.Chapter08.radixDigitOrderRespectsKey_of_bounded, and CLRS.Chapter08.radixSortNatBy_correct_keyOrdered_of_bounded.

  • 8.4 Bucket sort: proved for deterministic bucket-index correctness. Public results: CLRS.Chapter08.bucketSortBy_ordered, CLRS.Chapter08.bucketSortBy_perm, CLRS.Chapter08.bucketSortBy_correct, and CLRS.Chapter08.bucketSortByRank_correct; finite-uniform expected-cost results: CLRS.Chapter08.uniformAverageFin_indicator_singleton, CLRS.Chapter08.uniformAverageFin2_collision, CLRS.Chapter08.expectedBucketQuadraticCost_self_eq, and CLRS.Chapter08.expectedBucketQuadraticCost_self_linear_bound.

  • 9.2 Selection by rank: proved for the specification selector and pivot-style quickselect. Public results: CLRS.Chapter09.selectByRank?_mem, CLRS.Chapter09.selectByRank?_rankCorrect, CLRS.Chapter09.selectByRank?_correct, CLRS.Chapter09.quickSelect?_mem, CLRS.Chapter09.quickSelect?_rankCorrect, CLRS.Chapter09.quickSelect?_correct.

  • 9.3 Deterministic selection: proved for a pivot-parametric SELECT interface, the five-element median certificate, executable five-element grouping, grouped split-count bounds, deterministic median-pivot instance, median-of-medians pivot/select wrapper, and the abstract linear recurrence wrapper. Public results: CLRS.Chapter09.selectWithPivot?_correct, CLRS.Chapter09.medianOfFive?_certificate, CLRS.Chapter09.medianOfFive?_isSome_of_length_eq_five, CLRS.Chapter09.fullGroupsOfFive_medianGroupCertificates, CLRS.Chapter09.fullGroupsOfFive_medianPivot_split_counts, CLRS.Chapter09.fullGroupsOfFive_medianPivot_fullInput_split_counts, CLRS.Chapter09.fullGroupsOfFive_medianPivot_partition_size_bound, CLRS.Chapter09.selectRecurrence_linear_step, CLRS.Chapter09.selectRecurrence_linear_induction, CLRS.Chapter09.medianOfMedians_linear_bound, CLRS.Chapter09.medianGroupCertificates_selectPivot_split_counts, CLRS.Chapter09.medianOfFiveGroups?_mem_flatten, CLRS.Chapter09.fullGroupsOfFive_medianOfFiveGroups?_isSome, CLRS.Chapter09.medianOfMediansPivot?_mem, CLRS.Chapter09.medianOfMediansPivot?_partition_size_bound, CLRS.Chapter09.medianOfMediansSelect?_correct.

  • 9.3-9.4 Linear-time selection refinements: future-work. Planned target: connect the executable medianOfMediansSelect? cost semantics to the proved abstract linear recurrence theorem.

  • 10.1 Stacks and queues: proved for the functional-list model. Public results: CLRS.Chapter10.pop_push, CLRS.Chapter10.dequeue_enqueue_nonempty.

  • 10.2 Linked lists: proved for the functional-list model. Public results: CLRS.Chapter10.listSearch_sound, CLRS.Chapter10.mem_listDeleteAll_iff.

  • 11.1 Direct-address tables: proved for the functional table model. Public results: CLRS.Chapter11.search_insert_same, CLRS.Chapter11.search_delete_same.

  • 11.2 Chained hash tables: partial. Current results: CLRS.Chapter11.hashSearch_hashInsert_self, CLRS.Chapter11.hashSearch_hashInsert_iff, CLRS.Chapter11.hashSearch_hashDelete_self, CLRS.Chapter11.hashSearch_hashDelete_iff, CLRS.Chapter11.uniformAverageFin_indicator_singleton, CLRS.Chapter11.expectedSearchChainLength_eq_loadFactor, CLRS.Chapter11.expectedUnsuccessfulSearchCost_eq_one_plus_loadFactor, CLRS.Chapter11.totalBucketLength_finiteHashInsert, and CLRS.Chapter11.expectedSearchChainLength_finiteHashInsert.

  • 12.1 Binary search trees: partial. Current results: CLRS.Chapter12.BSTree.search_eq_true_iff, CLRS.Chapter12.BSTree.minimum?_le_of_ordered, CLRS.Chapter12.BSTree.le_maximum?_of_ordered, CLRS.Chapter12.BSTree.successor?_least_greater, CLRS.Chapter12.BSTree.successor?_eq_some_iff, CLRS.Chapter12.BSTree.successor?_eq_none_iff, CLRS.Chapter12.BSTree.successor?_isSome_iff_exists_greater, CLRS.Chapter12.BSTree.predecessor?_greatest_less, CLRS.Chapter12.BSTree.predecessor?_eq_some_iff, CLRS.Chapter12.BSTree.predecessor?_eq_none_iff, CLRS.Chapter12.BSTree.predecessor?_isSome_iff_exists_less, CLRS.Chapter12.BSTree.inTree_insert_iff, CLRS.Chapter12.BSTree.search_insert_eq_true_iff, CLRS.Chapter12.BSTree.insert_ordered, CLRS.Chapter12.BSTree.inTree_delete_iff, CLRS.Chapter12.BSTree.not_inTree_delete_self, CLRS.Chapter12.BSTree.delete_eq_self_of_not_inTree, CLRS.Chapter12.BSTree.search_delete_self_eq_false, CLRS.Chapter12.BSTree.search_delete_eq_true_iff, CLRS.Chapter12.BSTree.delete_ordered.

  • 13.1 Red-black trees: partial. Current results: CLRS.Chapter13.RBTree.inTree_rotateLeft_iff, CLRS.Chapter13.RBTree.inTree_repaintRoot_iff, CLRS.Chapter13.RBTree.noRedRed_repaint_black, CLRS.Chapter13.RBTree.balancedBlackHeight_rotateLeft_red_red, CLRS.Chapter13.RBTree.balancedBlackHeight_rotateRight_red_red, CLRS.Chapter13.RBTree.redBlackShape_repaint_rotateLeft_red_red, CLRS.Chapter13.RBTree.redBlackShape_repaint_rotateRight_red_red, CLRS.Chapter13.RBTree.redBlackShape_repaint_black, CLRS.Chapter13.RBTree.inTree_insertFixup_leftLeft_iff, CLRS.Chapter13.RBTree.inTree_insertFixup_leftRight_iff, CLRS.Chapter13.RBTree.inTree_insertFixup_rightLeft_iff, CLRS.Chapter13.RBTree.inTree_insertFixup_rightRight_iff, CLRS.Chapter13.RBTree.redBlackShape_insertFixup_leftLeft, CLRS.Chapter13.RBTree.redBlackShape_insertFixup_leftRight, CLRS.Chapter13.RBTree.redBlackShape_insertFixup_rightLeft, and CLRS.Chapter13.RBTree.redBlackShape_insertFixup_rightRight.

  • 14.1 Order-statistic trees: partial. Current results: CLRS.Chapter14.OSTree.storedSize_eq_realSize_of_wellSized, CLRS.Chapter14.OSTree.recomputeSizes_wellSized, CLRS.Chapter14.OSTree.keys_recomputeSizes, CLRS.Chapter14.OSTree.keys_rotateLeft, CLRS.Chapter14.OSTree.keys_rotateRight, CLRS.Chapter14.OSTree.realSize_rotateLeft, CLRS.Chapter14.OSTree.realSize_rotateRight, CLRS.Chapter14.OSTree.storedSize_rotateLeft_of_wellSized, CLRS.Chapter14.OSTree.storedSize_rotateRight_of_wellSized, CLRS.Chapter14.OSTree.rankSelect?_rotateLeft, CLRS.Chapter14.OSTree.rankSelect?_rotateRight, CLRS.Chapter14.OSTree.rotateLeft_wellSized, CLRS.Chapter14.OSTree.rotateRight_wellSized, CLRS.Chapter14.OSTree.osSelect?_eq_rankSelect?_of_wellSized, CLRS.Chapter14.OSTree.osSelect?_rotateLeft_eq_rankSelect?_of_wellSized, CLRS.Chapter14.OSTree.osSelect?_rotateRight_eq_rankSelect?_of_wellSized, and CLRS.Chapter14.OSTree.osSelect?_recomputeSizes_eq_rankSelect?.

  • 15.1 Rod cutting: partial. Current results: CLRS.Chapter15.firstCutValue_le_of_rodCutRecurrence, CLRS.Chapter15.rodRevenue_le_of_firstCutValue_bounds, CLRS.Chapter15.price_le_revenue_of_rodCutRecurrence, CLRS.Chapter15.planValue_le_revenue_of_rodCutRecurrence, CLRS.Chapter15.planValue_le_optimalPlanValue_of_same_length.

  • 15.2 Matrix-chain multiplication: partial. Current results: CLRS.Chapter15.ChainPlan.start_le_end, CLRS.Chapter15.MatrixChainLowerBound, CLRS.Chapter15.MatrixChainSplitOptimal, CLRS.Chapter15.matrixChain_opt_le_planCost, CLRS.Chapter15.matrixChain_reconstructed_cost_eq, CLRS.Chapter15.matrixChain_reconstructed_optimal, and CLRS.Chapter15.matrixChain_reconstructed_cost_le_planCost.

  • 15.4 Longest common subsequence: partial. Current results: CLRS.Chapter15.IsCommonSubsequence, CLRS.Chapter15.LCSCertificate.commonSubsequence_length_le, CLRS.Chapter15.LCSCertificate.length_eq_of_certificates, and CLRS.Chapter15.isCommonSubsequence_comm, CLRS.Chapter15.LCSTableRecurrence.cons_cons, CLRS.Chapter15.LCSTableRecurrence.cons_cons_of_eq, CLRS.Chapter15.LCSTableRecurrence.cons_cons_of_ne, CLRS.Chapter15.LCSTableCertificate.nil_left, CLRS.Chapter15.LCSTableCertificate.nil_right, CLRS.Chapter15.LCSTableCertificate.cons_cons, CLRS.Chapter15.LCSTableCertificate.cons_cons_of_eq, CLRS.Chapter15.LCSTableCertificate.cons_cons_of_ne, CLRS.Chapter15.LCSTableCertificate.commonSubsequence_length_le, CLRS.Chapter15.lcsTable_reconstruction_optimal, and CLRS.Chapter15.lcsCertificate_of_table_reconstruction_length.

  • 16.1 Activity selection: proved for finite sorted lists. Current results: CLRS.ActivitySelection.earliest_finish_minFinish, CLRS.ActivitySelection.finishSorted_head_minFinish, CLRS.ActivitySelection.finishSorted_greedyChoiceCertificate, CLRS.ActivitySelection.activitySelection, CLRS.ActivitySelection.activitySelection_cons_eq, CLRS.ActivitySelection.greedySelect_cons_eq, CLRS.ActivitySelection.greedySelect_sublist, CLRS.ActivitySelection.greedySelect_feasible, CLRS.ActivitySelection.greedy_choice_optimal_from_certificate, CLRS.ActivitySelection.greedySelect_after_maxCardinality, CLRS.ActivitySelection.greedySelect_cons_maxCardinality, CLRS.ActivitySelection.greedySelect_maxCardinality, CLRS.ActivitySelection.activitySelection_cons_maxCardinality, CLRS.ActivitySelection.activitySelection_maxCardinality, CLRS.ActivitySelection.greedySelect_optimal_length, CLRS.ActivitySelection.greedySelect_cons_recursive_correct, CLRS.ActivitySelection.activitySelection_cons_recursive_correct, CLRS.ActivitySelection.activitySelection_cons_correct, CLRS.ActivitySelection.activitySelection_correct.

  • 16.3 Huffman codes: proved. Public results: CLRS.HuffmanV2.optimum_huffman_freqs, CLRS.HuffmanV2.huffmanOfFreqs_correct, and CLRS.HuffmanV2.huffmanOfFreqs_cost_le.

  • 17.1-17.3 Amortized-analysis framework: proved for finite-prefix aggregate, accounting, and potential-method telescoping facts. Public results: CLRS.Chapter17.aggregate_bound_of_prefix_bound, CLRS.Chapter17.accounting_totalCost_eq_totalCharge_sub_delta, CLRS.Chapter17.accounting_totalCost_le_totalCharge, CLRS.Chapter17.potential_totalCost_eq_totalAmortized_sub_delta, and CLRS.Chapter17.potential_totalCost_le_totalAmortized.

  • 17.2 Stack and counter examples: partial. Public results: CLRS.Chapter17.multiPop_totalCost_le, CLRS.Chapter17.binaryCounter_increment_potential_le_two, CLRS.Chapter17.binaryCounter_trace_potential_le, CLRS.Chapter17.binaryCounter_trace_totalFlips_le, and CLRS.Chapter17.binaryCounter_totalFlips_le.

  • 17.4 Dynamic tables: partial. Public results: CLRS.Chapter17.dynamicPotential_nonneg, CLRS.Chapter17.dynamicTableInsert_potential_nonneg, CLRS.Chapter17.dynamicTableDelete_potential_nonneg, CLRS.Chapter17.dynamicTableInsertCost_pos, CLRS.Chapter17.dynamicTableInsertCost_le_num_succ, CLRS.Chapter17.dynamicTableInsertCost_of_fits, CLRS.Chapter17.dynamicTableInsertCost_of_expand, CLRS.Chapter17.dynamicTableInsertSize_of_fits, CLRS.Chapter17.dynamicTableInsertSize_of_expand, CLRS.Chapter17.dynamicTableInsertSize_fits, CLRS.Chapter17.dynamicTableInsertSize_ge_size, CLRS.Chapter17.dynamicTableInsertSize_ge_double_of_expand, CLRS.Chapter17.dynamicTableInsert_valid, CLRS.Chapter17.dynamicTableInsert_num, CLRS.Chapter17.dynamicTableInsert_size, CLRS.Chapter17.dynamicTableInsert_size_of_fits, CLRS.Chapter17.dynamicTableInsert_size_of_expand, CLRS.Chapter17.dynamicTableInsert_num_pos, CLRS.Chapter17.dynamicTableInsert_num_gt, CLRS.Chapter17.dynamicTableInsert_num_ge, CLRS.Chapter17.dynamicTableInsert_capacity_fits, CLRS.Chapter17.dynamicTableInsert_capacity_pos, CLRS.Chapter17.dynamicTableInsert_capacity_ge_size, CLRS.Chapter17.dynamicTableInsert_capacity_ge_double_of_expand, CLRS.Chapter17.dynamicTableInsert_amortizedCost_eq, CLRS.Chapter17.dynamicTableInsert_amortizedBound, CLRS.Chapter17.dynamicTableDeleteCost_pos_of_nonempty, CLRS.Chapter17.dynamicTableDeleteCost_pos_iff_nonempty, CLRS.Chapter17.dynamicTableDeleteCost_zero_iff_empty, CLRS.Chapter17.dynamicTableDeleteCost_le_num, CLRS.Chapter17.dynamicTableDeleteCost_empty, CLRS.Chapter17.dynamicTableDeleteCost_of_contract, CLRS.Chapter17.dynamicTableDeleteCost_of_no_contract, CLRS.Chapter17.dynamicTableDeleteCost_eq_num_of_contract, CLRS.Chapter17.dynamicTableDeleteCost_eq_one_of_no_contract, CLRS.Chapter17.dynamicTableDeleteSize_of_contract, CLRS.Chapter17.dynamicTableDeleteSize_of_no_contract, CLRS.Chapter17.dynamicTableDeleteSize_fits, CLRS.Chapter17.dynamicTableDeleteSize_le_size, CLRS.Chapter17.dynamicTableDeleteSize_le_half_of_contract, CLRS.Chapter17.dynamicTableDelete_valid, CLRS.Chapter17.dynamicTableDelete_num, CLRS.Chapter17.dynamicTableDelete_size, CLRS.Chapter17.dynamicTableDelete_size_of_contract, CLRS.Chapter17.dynamicTableDelete_size_of_no_contract, CLRS.Chapter17.dynamicTableDelete_num_le, CLRS.Chapter17.dynamicTableDelete_num_empty, CLRS.Chapter17.dynamicTableDelete_num_pos_of_one_lt, CLRS.Chapter17.dynamicTableDelete_num_lt_of_nonempty, CLRS.Chapter17.dynamicTableDelete_capacity_fits, CLRS.Chapter17.dynamicTableDelete_capacity_pos_of_one_lt, CLRS.Chapter17.dynamicTableDelete_capacity_le_size, CLRS.Chapter17.dynamicTableDelete_capacity_le_half_of_contract, CLRS.Chapter17.dynamicTableDelete_amortizedCost_eq, CLRS.Chapter17.dynamicTableDelete_amortizedBound, and CLRS.Chapter17.dynamicTable_amortizedBound.

  • 18.1-18.3 B-trees: partial. Public results: CLRS.Chapter18.BTree.search_correct, CLRS.Chapter18.BTree.search_true_iff, CLRS.Chapter18.BTree.search_true_of_mem, CLRS.Chapter18.BTree.mem_of_search_true, CLRS.Chapter18.BTree.search_false_iff, CLRS.Chapter18.BTree.search_false_of_not_mem, CLRS.Chapter18.BTree.not_mem_of_search_false, CLRS.Chapter18.BTree.minKeys_zero, CLRS.Chapter18.BTree.minKeys_pos, CLRS.Chapter18.BTree.one_le_minKeys, CLRS.Chapter18.BTree.minKeys_lower_bound, CLRS.Chapter18.BTree.minKeys_succ, CLRS.Chapter18.BTree.minKeys_le_succ, CLRS.Chapter18.BTree.minKeys_monotone_height, CLRS.Chapter18.BTree.splitChild_preserves_model, CLRS.Chapter18.BTree.splitChild_valid, CLRS.Chapter18.BTree.splitChild_mem_old, CLRS.Chapter18.BTree.splitChild_not_mem_iff, CLRS.Chapter18.BTree.splitChild_not_mem_old, CLRS.Chapter18.BTree.splitChild_search_iff, CLRS.Chapter18.BTree.splitChild_search_old, CLRS.Chapter18.BTree.splitChild_search_of_mem, CLRS.Chapter18.BTree.splitChild_search_false_iff, CLRS.Chapter18.BTree.splitChild_search_false_old, CLRS.Chapter18.BTree.splitChild_search_false_of_not_mem, CLRS.Chapter18.BTree.insert_preserves_model, CLRS.Chapter18.BTree.insert_valid, CLRS.Chapter18.BTree.insert_mem_iff, CLRS.Chapter18.BTree.insert_search_iff, CLRS.Chapter18.BTree.insert_search_of_eq, CLRS.Chapter18.BTree.insert_search_of_mem, CLRS.Chapter18.BTree.insert_not_mem_iff, CLRS.Chapter18.BTree.insert_not_mem_of_ne, CLRS.Chapter18.BTree.insert_search_false_iff, CLRS.Chapter18.BTree.insert_search_false_of_ne, CLRS.Chapter18.BTree.insert_search_false_of_not_mem_ne, CLRS.Chapter18.BTree.delete_preserves_model, CLRS.Chapter18.BTree.delete_valid, CLRS.Chapter18.BTree.delete_mem_iff, CLRS.Chapter18.BTree.delete_mem_iff_ne, CLRS.Chapter18.BTree.delete_search_iff, CLRS.Chapter18.BTree.delete_search_iff_ne, CLRS.Chapter18.BTree.delete_search_false_of_eq, CLRS.Chapter18.BTree.delete_mem_of_ne, CLRS.Chapter18.BTree.delete_mem_of_ne_prop, CLRS.Chapter18.BTree.delete_search_of_ne, CLRS.Chapter18.BTree.delete_search_of_ne_prop, CLRS.Chapter18.BTree.delete_search_of_mem_ne, CLRS.Chapter18.BTree.delete_search_of_mem_ne_prop, CLRS.Chapter18.BTree.delete_not_mem_iff, CLRS.Chapter18.BTree.delete_not_mem_old, CLRS.Chapter18.BTree.delete_not_mem_of_eq, CLRS.Chapter18.BTree.delete_search_false_iff, CLRS.Chapter18.BTree.delete_search_false_old, and CLRS.Chapter18.BTree.delete_search_false_of_not_mem.

  • 19.1 Fibonacci heaps: partial. Public results: CLRS.Chapter19.FibHeap.makeHeap_correct, CLRS.Chapter19.FibHeap.makeHeap_valid, CLRS.Chapter19.FibHeap.makeHeap_minimum_none, CLRS.Chapter19.FibHeap.potential_makeHeap, CLRS.Chapter19.FibHeap.potential_nonneg, CLRS.Chapter19.FibHeap.minimum_correct, CLRS.Chapter19.FibHeap.minimum_mem, CLRS.Chapter19.FibHeap.minimum_le, CLRS.Chapter19.FibHeap.minimum_none_iff, CLRS.Chapter19.FibHeap.minimum_none_of_empty, CLRS.Chapter19.FibHeap.minimum_ne_none_of_nonempty, CLRS.Chapter19.FibHeap.insert_correct, CLRS.Chapter19.FibHeap.insert_valid, CLRS.Chapter19.FibHeap.insert_mem_iff, CLRS.Chapter19.FibHeap.insert_not_mem_iff, CLRS.Chapter19.FibHeap.insert_not_mem_of_ne, CLRS.Chapter19.FibHeap.insert_minimum_correct, CLRS.Chapter19.FibHeap.insert_minimum_mem, CLRS.Chapter19.FibHeap.insert_minimum_le_inserted, CLRS.Chapter19.FibHeap.insert_minimum_le_old, CLRS.Chapter19.FibHeap.insert_minimum_none_iff, CLRS.Chapter19.FibHeap.insert_minimum_ne_none, CLRS.Chapter19.FibHeap.union_correct, CLRS.Chapter19.FibHeap.union_valid, CLRS.Chapter19.FibHeap.union_not_mem_iff, CLRS.Chapter19.FibHeap.union_not_mem_of_not_mem, CLRS.Chapter19.FibHeap.union_minimum_correct, CLRS.Chapter19.FibHeap.union_minimum_mem, CLRS.Chapter19.FibHeap.union_minimum_le_left, CLRS.Chapter19.FibHeap.union_minimum_le_right, CLRS.Chapter19.FibHeap.union_minimum_none_iff, CLRS.Chapter19.FibHeap.union_minimum_none_of_empty, CLRS.Chapter19.FibHeap.union_minimum_ne_none_of_left, CLRS.Chapter19.FibHeap.union_minimum_ne_none_of_right, CLRS.Chapter19.FibHeap.extractMin_correct, CLRS.Chapter19.FibHeap.extractMin_valid, CLRS.Chapter19.FibHeap.extractMin_not_mem_iff, CLRS.Chapter19.FibHeap.extractMin_not_mem_old, CLRS.Chapter19.FibHeap.extractMin_none_iff, CLRS.Chapter19.FibHeap.extractMin_none_of_empty, CLRS.Chapter19.FibHeap.extractMin_ne_none_of_nonempty, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_correct, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_ne, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_mem, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_le_old, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_none_iff, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_none_of_all_eq, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_ne_none_of_remaining, CLRS.Chapter19.FibHeap.decreaseKey_correct, CLRS.Chapter19.FibHeap.decreaseKey_valid, CLRS.Chapter19.FibHeap.decreaseKey_oldKey_mem_iff, CLRS.Chapter19.FibHeap.decreaseKey_oldKey_not_mem_of_ne, CLRS.Chapter19.FibHeap.decreaseKey_not_mem_iff, CLRS.Chapter19.FibHeap.decreaseKey_not_mem_of_ne, CLRS.Chapter19.FibHeap.decreaseKey_minimum_correct, CLRS.Chapter19.FibHeap.decreaseKey_minimum_mem, CLRS.Chapter19.FibHeap.decreaseKey_minimum_le_new, CLRS.Chapter19.FibHeap.decreaseKey_minimum_le_old, CLRS.Chapter19.FibHeap.decreaseKey_minimum_none_iff, CLRS.Chapter19.FibHeap.decreaseKey_minimum_ne_none, CLRS.Chapter19.FibHeap.delete_correct, CLRS.Chapter19.FibHeap.delete_valid, CLRS.Chapter19.FibHeap.delete_minimum_correct, CLRS.Chapter19.FibHeap.delete_minimum_ne, CLRS.Chapter19.FibHeap.delete_minimum_mem, CLRS.Chapter19.FibHeap.delete_minimum_le_old, CLRS.Chapter19.FibHeap.delete_minimum_none_iff, CLRS.Chapter19.FibHeap.delete_minimum_none_of_all_eq, CLRS.Chapter19.FibHeap.delete_minimum_ne_none_of_remaining, CLRS.Chapter19.FibHeap.delete_mem_iff, CLRS.Chapter19.FibHeap.delete_not_mem_iff, CLRS.Chapter19.FibHeap.delete_not_mem_old, CLRS.Chapter19.FibHeap.delete_not_mem_of_eq, CLRS.Chapter19.FibHeap.heapPotential_telescope, CLRS.Chapter19.FibHeap.fibLowerBound_step, CLRS.Chapter19.FibHeap.fibLowerBound_pos, CLRS.Chapter19.FibHeap.fibLowerBound_le_succ, CLRS.Chapter19.FibHeap.fibLowerBound_monotone, CLRS.Chapter19.FibHeap.fibLowerBound_add_two_ge_double, CLRS.Chapter19.FibHeap.fibLowerBound_even_lower_bound, CLRS.Chapter19.FibHeap.fibLowerBound_half_lower_bound, CLRS.Chapter19.FibHeap.degreeIndex_half_le_log_card, CLRS.Chapter19.FibHeap.degreeIndex_le_twice_log_card_add_one, and CLRS.Chapter19.FibHeap.degree_bound_log.

  • 20.1-20.2 van Emde Boas trees: partial. Public results: CLRS.Chapter20.VEB.index_high_low, CLRS.Chapter20.VEB.high_index, CLRS.Chapter20.VEB.low_index, CLRS.Chapter20.VEB.index_lt, CLRS.Chapter20.VEB.high_lt, CLRS.Chapter20.VEB.low_lt, CLRS.Chapter20.VEB.member_correct, CLRS.Chapter20.VEB.member_lt_univ, CLRS.Chapter20.VEB.minimum_correct, CLRS.Chapter20.VEB.minimum_mem, CLRS.Chapter20.VEB.minimum_le, CLRS.Chapter20.VEB.minimum_lt_univ, CLRS.Chapter20.VEB.minimum_none_iff, CLRS.Chapter20.VEB.minimum_none_of_empty, CLRS.Chapter20.VEB.minimum_ne_none_of_nonempty, CLRS.Chapter20.VEB.maximum_correct, CLRS.Chapter20.VEB.maximum_mem, CLRS.Chapter20.VEB.le_maximum, CLRS.Chapter20.VEB.maximum_lt_univ, CLRS.Chapter20.VEB.maximum_none_iff, CLRS.Chapter20.VEB.maximum_none_of_empty, CLRS.Chapter20.VEB.maximum_ne_none_of_nonempty, CLRS.Chapter20.VEB.successor_correct, CLRS.Chapter20.VEB.successor_mem, CLRS.Chapter20.VEB.successor_gt, CLRS.Chapter20.VEB.successor_le, CLRS.Chapter20.VEB.successor_lt_univ, CLRS.Chapter20.VEB.successor_none_iff, CLRS.Chapter20.VEB.successor_none_of_no_gt, CLRS.Chapter20.VEB.successor_ne_none_of_exists_gt, CLRS.Chapter20.VEB.predecessor_correct, CLRS.Chapter20.VEB.predecessor_mem, CLRS.Chapter20.VEB.predecessor_lt, CLRS.Chapter20.VEB.le_predecessor, CLRS.Chapter20.VEB.predecessor_lt_univ, CLRS.Chapter20.VEB.predecessor_none_iff, CLRS.Chapter20.VEB.predecessor_none_of_no_lt, CLRS.Chapter20.VEB.predecessor_ne_none_of_exists_lt, CLRS.Chapter20.VEB.insert_correct, CLRS.Chapter20.VEB.insert_member_iff, CLRS.Chapter20.VEB.insert_member_lt_univ, CLRS.Chapter20.VEB.insert_member_self, CLRS.Chapter20.VEB.insert_member_old, CLRS.Chapter20.VEB.insert_member_false_iff, CLRS.Chapter20.VEB.insert_member_false_of_ne, CLRS.Chapter20.VEB.insert_minimum_correct, CLRS.Chapter20.VEB.insert_minimum_mem, CLRS.Chapter20.VEB.insert_minimum_mem_old_of_ne, CLRS.Chapter20.VEB.insert_minimum_le_inserted, CLRS.Chapter20.VEB.insert_minimum_le_old, CLRS.Chapter20.VEB.insert_minimum_lt_univ, CLRS.Chapter20.VEB.insert_minimum_none_iff, CLRS.Chapter20.VEB.insert_minimum_ne_none, CLRS.Chapter20.VEB.insert_maximum_correct, CLRS.Chapter20.VEB.insert_maximum_mem, CLRS.Chapter20.VEB.insert_maximum_mem_old_of_ne, CLRS.Chapter20.VEB.insert_maximum_inserted_le, CLRS.Chapter20.VEB.insert_maximum_old_le, CLRS.Chapter20.VEB.insert_maximum_lt_univ, CLRS.Chapter20.VEB.insert_maximum_none_iff, CLRS.Chapter20.VEB.insert_maximum_ne_none, CLRS.Chapter20.VEB.insert_successor_correct, CLRS.Chapter20.VEB.insert_successor_mem, CLRS.Chapter20.VEB.insert_successor_mem_old_of_ne, CLRS.Chapter20.VEB.insert_successor_gt, CLRS.Chapter20.VEB.insert_successor_le, CLRS.Chapter20.VEB.insert_successor_lt_univ, CLRS.Chapter20.VEB.insert_successor_none_iff, CLRS.Chapter20.VEB.insert_successor_none_of_no_gt, CLRS.Chapter20.VEB.insert_successor_none_of_insert_le_old_no_gt, CLRS.Chapter20.VEB.insert_successor_ne_none_of_insert_gt, CLRS.Chapter20.VEB.insert_successor_ne_none_of_old_gt, CLRS.Chapter20.VEB.insert_predecessor_correct, CLRS.Chapter20.VEB.insert_predecessor_mem, CLRS.Chapter20.VEB.insert_predecessor_mem_old_of_ne, CLRS.Chapter20.VEB.insert_predecessor_lt, CLRS.Chapter20.VEB.insert_le_predecessor, CLRS.Chapter20.VEB.insert_predecessor_lt_univ, CLRS.Chapter20.VEB.insert_predecessor_none_iff, CLRS.Chapter20.VEB.insert_predecessor_none_of_no_lt, CLRS.Chapter20.VEB.insert_predecessor_none_of_query_le_insert_old_no_lt, CLRS.Chapter20.VEB.insert_predecessor_ne_none_of_insert_lt, CLRS.Chapter20.VEB.insert_predecessor_ne_none_of_old_lt, CLRS.Chapter20.VEB.delete_correct, CLRS.Chapter20.VEB.delete_member_iff, CLRS.Chapter20.VEB.delete_member_lt_univ, CLRS.Chapter20.VEB.delete_member_deleted_false, CLRS.Chapter20.VEB.delete_member_of_ne, CLRS.Chapter20.VEB.delete_member_false_iff, CLRS.Chapter20.VEB.delete_member_false_old, CLRS.Chapter20.VEB.delete_member_false_of_eq, CLRS.Chapter20.VEB.delete_minimum_correct, CLRS.Chapter20.VEB.delete_minimum_ne, CLRS.Chapter20.VEB.delete_minimum_mem, CLRS.Chapter20.VEB.delete_minimum_le_old, CLRS.Chapter20.VEB.delete_minimum_lt_univ, CLRS.Chapter20.VEB.delete_minimum_none_iff, CLRS.Chapter20.VEB.delete_minimum_none_of_all_eq, CLRS.Chapter20.VEB.delete_minimum_ne_none_of_remaining, CLRS.Chapter20.VEB.delete_maximum_correct, CLRS.Chapter20.VEB.delete_maximum_ne, CLRS.Chapter20.VEB.delete_maximum_mem, CLRS.Chapter20.VEB.delete_maximum_old_le, CLRS.Chapter20.VEB.delete_maximum_lt_univ, CLRS.Chapter20.VEB.delete_maximum_none_iff, CLRS.Chapter20.VEB.delete_maximum_none_of_all_eq, CLRS.Chapter20.VEB.delete_maximum_ne_none_of_remaining, CLRS.Chapter20.VEB.delete_successor_correct, CLRS.Chapter20.VEB.delete_successor_mem, CLRS.Chapter20.VEB.delete_successor_gt, CLRS.Chapter20.VEB.delete_successor_le, CLRS.Chapter20.VEB.delete_successor_lt_univ, CLRS.Chapter20.VEB.delete_successor_none_iff, CLRS.Chapter20.VEB.delete_successor_none_of_no_gt, CLRS.Chapter20.VEB.delete_successor_none_of_old_no_gt, CLRS.Chapter20.VEB.delete_successor_ne_none_of_remaining_gt, CLRS.Chapter20.VEB.delete_predecessor_correct, CLRS.Chapter20.VEB.delete_predecessor_mem, CLRS.Chapter20.VEB.delete_predecessor_lt, CLRS.Chapter20.VEB.delete_le_predecessor, CLRS.Chapter20.VEB.delete_predecessor_lt_univ, CLRS.Chapter20.VEB.delete_predecessor_none_iff, CLRS.Chapter20.VEB.delete_predecessor_none_of_no_lt, CLRS.Chapter20.VEB.delete_predecessor_none_of_old_no_lt, CLRS.Chapter20.VEB.delete_predecessor_ne_none_of_remaining_lt, CLRS.Chapter20.VEB.operationDepth_zero, CLRS.Chapter20.VEB.operationDepth_succ, CLRS.Chapter20.VEB.operationDepth_linear, CLRS.Chapter20.VEB.operationDepth_monotone, and CLRS.Chapter20.VEB.operationDepth_strict_mono.

  • 23.1 Growing a minimum spanning tree: partial. Current results: CLRS.MST.Graph.connected_crosses_cut, CLRS.MST.FiniteGraph.minimumSpanningTree_of_mstExtending_empty, CLRS.MST.FiniteGraph.mstExtending_empty_of_minimumSpanningTree, CLRS.MST.FiniteGraph.minimumSpanningTree_iff_mstExtending_empty, CLRS.MST.FiniteGraph.exists_crossing_tree_edge_of_cut, CLRS.MST.FiniteGraph.exists_crossing_tree_edge_preserving_prefix, and CLRS.MST.safe_edge_of_lightest_crossing.

  • 23.2 Kruskal and Prim: partial. Current results: CLRS.MST.processed_prefix_excludes_of_exact_component_kruskal, CLRS.MST.cut_certificate_of_exact_component_kruskal_prefix, CLRS.MST.Graph.InsertedEdgeConnection, CLRS.MST.Graph.exchangePath_connected_insert, CLRS.MST.Graph.exchangePath_of_insert_connected, CLRS.MST.Graph.exchangePath_iff_insertedEdgeConnection, CLRS.MST.FiniteGraph.exchangePath_of_insert_connects_erased_edge, CLRS.MST.FiniteGraph.exchangePath_iff_insertedEdgeConnection_of_spanningTree, CLRS.MST.kruskal_optimal, and CLRS.MST.FiniteGraph.kruskal_minimum_spanning_tree_of_cycle_test.

Status Policy

The site uses explicit status labels instead of hiding incomplete work.

  • proved: the named theorem is proved in Lean without relying on sorry.

  • expository: the page is a reader guide rather than a theorem-bearing section.

  • partial: important theorem infrastructure exists, but the full textbook section is not yet complete.

  • blocked-design: progress needs a representation decision, such as paths, walks, heaps, arrays, or cost semantics.

  • deferred-implementation: a low-level implementation proof is useful but not required for the current mathematical theorem.

  • future-work: valuable extensions, exercises, or chapter-end problems.

Build and Deployment

The deployed site is generated from the Lean source by Verso:

  • lake build compiles the Lean library.

  • lake build :literateHtml generates the website.

GitHub Actions runs the same pipeline and publishes the generated _site directory to GitHub Pages.

Repository: TankTechnology/CLRS-Lean