-
Notifications
You must be signed in to change notification settings - Fork 2
OpenAug 5, 2026
No due date
•Last updated Complete the core textbook algorithms, invariants, correctness theorems, and principal complexity results for CLRS Chapters 27-35. Exercises and chapter-end Problems are explicitly deferred to a later phase.
22% complete
List view
0 of 21 selected 0 issues of 21 selected
Ch32.4: Knuth-Morris-Pratt algorithm (prefix function + linear-time correctness)
chapter-32String MatchingString MatchingproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#71 In TankTechnology/CLRS-Lean;Ch33.2-33.3: Segment intersection detection + convex hull (Graham scan)
chapter-33Computational GeometryComputational GeometryproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#75 In TankTechnology/CLRS-Lean;Ch32.2: Rabin-Karp algorithm (rolling hash + correctness)
chapter-32String MatchingString MatchingproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#69 In TankTechnology/CLRS-Lean;Ch31.8-31.9: Primality testing (Miller-Rabin) + integer factorization (Pollard's rho)
chapter-31Number-Theoretic AlgorithmsNumber-Theoretic AlgorithmsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#67 In TankTechnology/CLRS-Lean;Roadmap: Ch28.1 LUP decomposition and linear-system solving
chapter-28Matrix OperationsMatrix OperationsproofFormalization / theorem-proving taskFormalization / theorem-proving taskroadmapRoadmap and tracking issuesRoadmap and tracking issuesStatus: Open.#77 In TankTechnology/CLRS-Lean;Ch31.6-31.7: Modular exponentiation + RSA public-key cryptosystem
chapter-31Number-Theoretic AlgorithmsNumber-Theoretic AlgorithmsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#66 In TankTechnology/CLRS-Lean;Ch31.3-31.5: Modular arithmetic, modular linear equations, Chinese remainder theorem
chapter-31Number-Theoretic AlgorithmsNumber-Theoretic AlgorithmsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#65 In TankTechnology/CLRS-Lean;Ch28: LDL^T decomposition — existence proof (ldltDecomp_exists, Theorem 28.4)
chapter-28Matrix OperationsMatrix OperationsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#125 In TankTechnology/CLRS-Lean;Ch35.1-35.3: Approximation algorithms — vertex cover, TSP, set cover
chapter-35Approximation AlgorithmsApproximation AlgorithmsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#81 In TankTechnology/CLRS-Lean;Ch33.1: Line-segment properties (cross product, orientation, intersection tests)
chapter-33Computational GeometryComputational GeometryproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#74 In TankTechnology/CLRS-Lean;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.#78 In TankTechnology/CLRS-Lean;Ch30.1-30.2: Polynomial representation, DFT, and FFT (complex roots of unity)
chapter-30Polynomials and the FFTPolynomials and the FFTproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#72 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.#126 In TankTechnology/CLRS-Lean;Ch32.3: String matching with finite automata (transition function + correctness)
chapter-32String MatchingString MatchingproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#70 In TankTechnology/CLRS-Lean;Ch35.4-35.5: Randomized rounding (MAX-3-CNF) + subset-sum FPTAS
chapter-35Approximation AlgorithmsApproximation AlgorithmsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#82 In TankTechnology/CLRS-Lean;Ch30.3: Efficient FFT implementations (iterative + parallel circuit)
chapter-30Polynomials and the FFTPolynomials and the FFTproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#73 In TankTechnology/CLRS-Lean;Ch31.1-31.2: Elementary number theory + Euclid's algorithm (GCD, extended Euclid)
chapter-31Number-Theoretic AlgorithmsNumber-Theoretic AlgorithmsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#64 In TankTechnology/CLRS-Lean;Ch33.4: Finding the closest pair of points (divide-and-conquer, O(n log n))
chapter-33Computational GeometryComputational GeometryproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#76 In TankTechnology/CLRS-Lean;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.#79 In TankTechnology/CLRS-Lean;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.#80 In TankTechnology/CLRS-Lean;Ch28: LUP-SOLVE correctness proof (lupSolve_correct, Theorem 28.2)
chapter-28Matrix OperationsMatrix OperationsproofFormalization / theorem-proving taskFormalization / theorem-proving taskStatus: Open.#124 In TankTechnology/CLRS-Lean;