Formalized complexity classes and completeness in lean proof assistant
Descriptive Complexity in Lean: Completeness by First-Order Reductions
Logic in Computer ScienceComputational Complexity
Summary
Understanding how difficult computer problems are and how they relate is important but often tricky to prove. The authors created a library in Lean, a tool for checking math proofs, to express these complexity results using logic rather than machines. They proved many classic results about problem difficulty, showing how problems relate using logical descriptions and simple reductions. This helps make sure that complexity results are correct and understandable inside a formal system.
What this means in practice
- •For formal methods engineers: Use the Lean library to formally verify complexity results and reductions in software correctness proofs for critical systems.
- •For automated theorem prover developers: Integrate these formalized complexity concepts to enhance reasoning capabilities about decision problems and complexity class inclusions.
Authors
Pierre Senellart, Anton Gnatenko
Abstract
We show that descriptive complexity can serve as a foundation for formalizing computational complexity results in a proof assistant, by constructing a Lean library centered around the following concepts: decision problems are isomorphism-invariant predicates on finite structures; complexity classes are defined by their logical characterization; membership is shown by definability witnesses; hardness is shown by first-order reductions from a known hard problem. We also establish bridges to traditional machine models such as (non)deterministic Turing machines. The library proves 73 completeness results, on 68 problems or problem families, over 14 different classes; relations between the classes established inside the logic and not by machine simulation, among them NL = coNL and the Abiteboul-Vianu theorem; and unconditional lower bounds, among them $\mathrm{FO}(\leq) \subsetneq \mathrm{FO}(\leq, \mathrm{TC})$ and the failure of order-free FO(IFP) to capture PTIME.