Computational complexity hardness and completeness results are almost never formalized in proof assistants because standard proofs are anchored to machine models under resource constraints that resist mechanization. Existing developments stop at a handful of completeness theorems.

A Lean library is built around descriptive complexity: decision problems are isomorphism-invariant predicates on finite structures, complexity classes are defined by their logical characterization, membership is shown by definability witnesses, and hardness by first-order reductions from known hard problems. Classes are closed under first-order reductions via per-logic pullback lemmas built on Mathlib's FirstOrder.Language and BoundedFormula. Machine bridges link the logically defined classes to Turing-machine definitions by encoding acceptance as a decision problem over a finite structure.

The library proves 73 completeness results on 68 problems or problem families over 14 classes, including all 21 Karp problems as NP-complete. It establishes class relations inside the logic (NL = coNL, the Abiteboul-Vianu theorem) and unconditional lower bounds (FO(≤) ⊊ FO(≤,TC) and failure of order-free FO(IFP) to capture PTIME). The SAT completeness theorem's dependency closure is far smaller than machine-model developments.