-
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
Ch15.3: Elements of dynamic programming (conceptual section)
proofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#136 In TankTechnology/CLRS-Lean;Ch24.5: Shortest-path properties (subpath property, optimal substructure)
proofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#135 In TankTechnology/CLRS-Lean;Ch14.3: toRB refinement erasure for the generic AugmentedRBTree deletion pipeline
chapter-14Augmenting Data StructuresAugmenting Data StructuresproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#133 In TankTechnology/CLRS-Lean;Ch26.4-26.5: Push-Relabel / Relabel-to-Front maximum-flow algorithm
extreme-difficultyRequires concentrated proof-design workRequires concentrated proof-design workproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#132 In TankTechnology/CLRS-Lean;Ch28: Least-squares optimality proof (leastSquares_optimal, Theorem 28.5)
chapter-28Matrix OperationsMatrix OperationsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.Ch28: LDL^T decomposition — existence proof (ldltDecomp_exists, Theorem 28.4)
chapter-28Matrix OperationsMatrix OperationsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.Ch28: LUP-SOLVE correctness proof (lupSolve_correct, Theorem 28.2)
chapter-28Matrix OperationsMatrix OperationsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.Ch35.4-35.5: Randomized rounding (MAX-3-CNF) + subset-sum FPTAS
chapter-35Approximation AlgorithmsApproximation AlgorithmsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.Ch35.1-35.3: Approximation algorithms — vertex cover, TSP, set cover
chapter-35Approximation AlgorithmsApproximation AlgorithmsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.Ch34.4-34.5: NP-completeness proofs (CIRCUIT-SAT → 3-CNF-SAT → CLIQUE → VERTEX-COVER chain)
chapter-34NP-CompletenessNP-Completenessextreme-difficultyRequires concentrated proof-design workRequires concentrated proof-design workproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.Ch34.1-34.3: NP-Completeness foundations (polynomial time, verification, reducibility)
chapter-34NP-CompletenessNP-Completenessextreme-difficultyRequires concentrated proof-design workRequires concentrated proof-design workproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.Roadmap: Ch28.2-28.3 inversion, SPD decomposition, and least squares
chapter-28Matrix OperationsMatrix OperationsproofFormalization / theorem-proving taskFormalization / theorem-proving taskroadmapRoadmap and tracking issuesRoadmap and tracking issuesStatus: Open.