Verified polynomial-time reductions in Lean 4: formalizing the complexity of decision-relevant information
Tristan Simas
TL;DR
This work formalizes a decision-theoretic problem of sufficiency: identifying a coordinate subset whose known values determine the optimal action in a finite-state setting. It introduces a Lean 4 framework for polynomial-time reductions, proving a complete complexity landscape under explicit and succinct encodings: SUFFICIENCY-CHECK and MINIMUM-SUFFICIENT-SET are $\text{coNP}$-complete, while ANCHOR-SUFFICIENCY is $\Sigma_{2}^{\textsf{P}}$-complete; an explicit/succinct encoding dichotomy yields a polynomial-time explicit-state regime and $2^{\Omega(n)}$ ETH-based hardness in the succinct regime. The paper further identifies tractable subcases (bounded actions, separable utilities, tree-structured utilities) and connects the hardness results to engineering practice, explaining why over-modeling can be a rational response under computational constraints. Beyond theory, the authors provide a reusable reduction library, formal proofs, and mechanized strengthened reductions, offering practical guidance for software architecture and configuration design under worst-case complexity considerations.
Abstract
We present a Lean 4 framework for polynomial-time reductions and complexity-theory proofs, and use it to formalize the complexity of identifying decision-relevant information. Problem: given a decision problem, which coordinates suffice to compute an optimal action? (SUFFICIENCY-CHECK; explicit encodings). Verified complexity results (Lean): coNP-complete; $(1-\varepsilon)\ln n$ inapproximable (from SET-COVER); $2^{Ω(n)}$ lower bounds under ETH for succinct encodings; W[2]-hard for a natural parameterization; and a dichotomy between explicit and succinct models. Formalization contributions: bundled Karp reductions with polynomial-time witnesses; composition lemmas/tactics; and templates for NP/coNP and $Σ_2^P$ membership and hardness. Scale: about 5,600 lines of Lean across 36 files, with 230+ theorems and explicit polynomial bounds.