-
Notifications
You must be signed in to change notification settings - Fork 2
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Ch28: Least-squares optimality proof (leastSquares_optimal, Theorem 28.5)
ch28Chapter ch28 workChapter ch28 workenhancementNew feature or requestNew feature or requestStatus: Open.#126 In TankTechnology/CLRS-Lean;Ch28: LDL^T decomposition — existence proof (ldltDecomp_exists, Theorem 28.4)
ch28Chapter ch28 workChapter ch28 workenhancementNew feature or requestNew feature or requestStatus: Open.#125 In TankTechnology/CLRS-Lean;Ch28: LUP-SOLVE correctness proof (lupSolve_correct, Theorem 28.2)
ch28Chapter ch28 workChapter ch28 workenhancementNew feature or requestNew feature or requestStatus: Open.#124 In TankTechnology/CLRS-Lean;Ch28: LUP decomposition — existence proof (lupDecomp_exists, Theorem 28.1)
ch28Chapter ch28 workChapter ch28 workenhancementNew feature or requestNew feature or requestStatus: Open.#123 In TankTechnology/CLRS-Lean;Ch27: Executable P-MERGE and P-MERGE-SORT implementations
ch27Chapter ch27 workChapter ch27 workenhancementNew feature or requestNew feature or requestStatus: Open.#122 In TankTechnology/CLRS-Lean;Ch27: All-input Θ-bounds for P-MERGE, P-MERGE-SORT costs
ch27Chapter ch27 workChapter ch27 workenhancementNew feature or requestNew feature or requestStatus: Open.#121 In TankTechnology/CLRS-Lean;Ch27: Greedy-scheduler bound (Theorems 27.1/27.2) — Tp ≤ T₁/p + T∞
ch27Chapter ch27 workChapter ch27 workenhancementNew feature or requestNew feature or requestStatus: Open.#120 In TankTechnology/CLRS-Lean;Ch1-26 completeness roadmap: remaining 9 core gaps across 4 chapters
proofFormalization / theorem-proving taskFormalization / theorem-proving taskroadmapRoadmap and tracking issuesRoadmap and tracking issuesStatus: Open.#110 In TankTechnology/CLRS-Lean;Ch18 B-Trees: node-level deletion repair with full invariant preservation
chapter-18B-TreesB-TreesproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#109 In TankTechnology/CLRS-Lean;Ch18 B-Trees: separator, occupancy, and same-depth invariant stack
chapter-18B-TreesB-TreesproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#108 In TankTechnology/CLRS-Lean;Ch26.2: Edmonds-Karp BFS augmenting loop + O(VE²) complexity theorem
proofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#106 In TankTechnology/CLRS-Lean;Ch26.6: Max-Flow Min-Cut converse — residual-network cut lemma + full equivalence
proofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#105 In TankTechnology/CLRS-Lean;