Hardness Reductions in Lean

A Lean 4 / mathlib library of NP-hardness reductions, organized as a Garey–Johnson-style catalog of hard problems: machine-checked proofs of the classical reduction constructions — SAT → 3SAT, SAT → CLIQUE, VERTEX COVER → SUBSET SUM, … — together with a certificate layer that pins down, syntactically, that the reduction maps are polynomial-time.

There is no Turing machine in this library, and no formalization of P or NP. That is the design, not a shortcut, and it is what keeps the library light enough to grow the way the informal catalog literature does.

The idea

A textbook NP-hardness proof has two parts of very different character. The heart is combinatorial: a gadget construction, and an argument that yes-instances map to yes-instances and back. The other part is resource accounting — "the construction is clearly polynomial" — which the literature settles by inspection, because for honest constructions it is visibly true, and writing it out against a machine model would add nothing to the mathematics.

A formalization that starts from a machine model must pay for the routine part first, and pay dearly: structured instances become strings, gadget constructions become machine programs, and resource bookkeeping runs through every proof. This library decouples the two parts instead, so that each can be done in the style appropriate to it.

The mathematical layer. A problem is a predicate on structured instances, and a reduction is a map together with a correctness proof:

def Problem (α : Type u) := α → Prop

structure Reduction (P : Problem α) (Q : Problem β) where  -- notation: P ⟶ᵣ Q
  map : α → β
  correct : ∀ x, P x ↔ Q (map x)

Instances are bundled structures over mathlib types (SimpleGraph, CNF formulas, lists of numbers), so the correctness arguments — the actual mathematics — are carried out with mathlib's ordinary APIs, at the level of abstraction the informal proofs use. No resource bounds appear anywhere in this layer.

The certificate layer. Separately, Cert/Language.lean defines a small deep-embedded combinator language Code σ τ over a closed universe of first-order types (numbers, booleans, pairs, lists), with an explicit cost model that charges numbers by bit length. The language is designed so that a single theorem, proven once for all programs, gives the resource bound:

theorem Code.cost_size_le_polyBound (c : Code σ τ) :
    ∃ C d, ∀ x, c.cost x + τ.size (c.eval x) ≤ C * (σ.size x + 1) ^ d

A reduction is certified by exhibiting its instance map as a Code program and proving that program correct on concrete instances (Cert/Bridge.lean). The polynomial bound then comes for free: there are no per-reduction cost proofs anywhere in the library, just as there are none in the literature. Certified reductions compose, and the certificate of a composite is the composite program. The recurring proof obligation of an adequacy file — realizing a gadget's tagged vertex or element names as positions of the emitted list — is served by a block-numbering layer (Cert/Numbering.lean): a layout is composed from digit and block combinators, and its bound, injectivity, and bijection onto the positions are read off rather than re-proved.

The representation layer. The two layers meet at concrete instances: each abstract problem has a concrete counterpart, defined by pulling the predicate back along a total decoder (Concrete.CLIQUE x = CLIQUE (decodeGraph x)), and certificates speak about the concrete problems. That the concrete problem faithfully represents the abstract one is itself a theorem, once per problem: encoding any bundled instance and decoding the result reproduces it up to isomorphism, giving a reduction pair CLIQUE ⟶ᵣ Concrete.CLIQUE and back (Graph/Representation.lean). Composing through such a pair turns a certified reduction between concrete problems into the reduction between the abstract ones, so a degenerate decoder cannot hide: what the certified pipeline proves about the abstract problems is a theorem, not a reading of the decoder. Every problem in the catalog carries its representation pair, one Representation.lean per domain, and the pairs of different domains compose — VERTEX COVER → SET COVER is recovered abstract-to-abstract with nothing but certificates in between.

The deferred bridge. What this library does not contain is a theorem connecting the cost model to a machine model of polynomial time — mathlib does not yet have one to connect to. The interface is deliberately a single point: when a machine model of FP lands in mathlib, one theorem ("the Code interpreter runs in polynomial time") turns every certificate in this catalog into a machine-model Karp reduction, with no per-reduction work. Until then, the precise claim of a certificate is: the map is expressed in a language in which only polynomial-cost, polynomial-size transformations can be written, for a cost model designed to be honest (see the size discipline below).

The catalog

Reductions are filed under their target problem — each is a proof that the target is hard, and every reduction in the catalog is certified in the Code layer. The picture keeps one arrow per construction; fifteen further edges exist in the library as one-line derivations — composites, and the weakening 3SAT → SAT (an instance of CertifiedReduction.ofRestrict, whose width test is a program) — and are omitted to keep it readable.

flowchart LR
  subgraph Logic
    SAT
    SAT3["3SAT"]
    OCC3["3SAT, clauses of length 2–3,<br>≤3 occurrences per variable"]
    NAE3["NOT-ALL-EQUAL 3SAT"]
    M2SAT["MAX 2SAT"]
  end
  subgraph Graphs
    CLIQUE
    IS["INDEPENDENT SET"]
    VC["VERTEX COVER"]
    VCD3["VERTEX COVER,<br>maximum degree ≤ 3"]
    DS["DOMINATING SET"]
    COL["K-COLORABILITY"]
    COL3["3-COLORABILITY"]
    CC["CLIQUE COVER"]
    SMC["SIMPLE MAX CUT"]
    HC["HAMILTONIAN CIRCUIT"]
    HP["HAMILTONIAN PATH"]
  end
  subgraph Networks
    TSP["TRAVELING SALESMAN"]
  end
  subgraph Sets
    SC["SET COVER"]
    HS["HITTING SET"]
    SP["SET PACKING"]
    M3D["3-DIMENSIONAL MATCHING"]
    X3C["EXACT COVER BY 3-SETS"]
  end
  subgraph Numbers
    SS["SUBSET SUM"]
    PART["PARTITION"]
    KNAP["KNAPSACK"]
  end
  SAT --> SAT3
  SAT --> OCC3
  SAT --> M3D
  M3D --> X3C
  SAT --> CLIQUE
  CLIQUE --> IS
  IS --> CLIQUE
  IS --> VC
  VC --> IS
  VC --> DS
  VC --> SC
  VC --> HS
  IS --> SP
  VC --> SS
  VC --> HC
  HC --> HP
  HC --> TSP
  SS --> PART
  SS --> KNAP
  SAT3 --> NAE3
  SAT3 --> M2SAT
  M2SAT --> SMC
  SAT3 --> VCD3
  SAT --> COL3
  COL3 --> COL
  COL --> CC

Loading

• SAT (Logic/Sat.lean) — the root of the catalog: satisfiability of CNF formulas over an explicit variable list. No reduction lands here; every hardness claim below traces back to it.
• 3SAT (Logic/Sat3.lean) — hard from SAT (clause splitting: each long clause becomes a chain of width-3 clauses linked by fresh chain variables; short clauses, including the empty clause, are kept as they are).
• 3SAT with clauses of length 2 or 3 and at most 3 occurrences per variable (Logic/Sat3/BoundedOcc.lean) — hard from SAT and from 3SAT (one fresh variable per occurrence, linked by an implication cycle). Length-2 clauses are essential: by Tovey's theorem, the exactly-length-3 variant is always satisfiable.
• NOT-ALL-EQUAL 3SAT (Logic/Nae3Sat.lean) — hard from 3SAT (one fresh variable per clause plus one global variable standing in for the constant false). Its restriction is clause width exactly three, where 3SAT's is at most three: each entry states the sharpest restriction its own construction delivers.
• MAX 2SAT (Logic/MaxSat.lean) — hard from 3SAT (ten clauses of width at most two per source clause, over one fresh variable; threshold seven per clause). A counting predicate — the question is how many clauses an assignment satisfies — which is what makes width two hard: asking whether all clauses of a 2CNF hold is 2SAT.
• CLIQUE (Graph/Clique.lean) — hard from SAT (the occurrence graph: a vertex per literal occurrence, adjacency between non-conflicting occurrences in distinct clauses, threshold the number of clauses), from INDEPENDENT SET (complementation), and from VERTEX COVER.
• INDEPENDENT SET (Graph/IndepSet.lean) — hard from CLIQUE (complementation), from VERTEX COVER (a set is independent iff its complement is a cover), and from SAT.
• VERTEX COVER (Graph/VertexCover.lean) — hard from INDEPENDENT SET (the same complementation, read the other way) and from SAT.
• VERTEX COVER on graphs of maximum degree at most three (Graph/VertexCover/BoundedDegree.lean) — hard from 3SAT (a cyclic T/F circuit per variable, a triangle per clause, one connection edge per literal). Stated as ≤ 3 rather than = 3: the construction is not cubic, and degree ≤ 2 is polynomial, so this is the sharpest of the ≤-bounds.
• DOMINATING SET (Graph/DominatingSet.lean) — hard from VERTEX COVER (the edge-vertex gadget: one fresh vertex per edge, joined to both endpoints, so every edge becomes a triangle; the threshold k + #isolated absorbs the textbook's "WLOG no isolated vertices").
• GRAPH K-COLORABILITY and GRAPH 3-COLORABILITY (Graph/Colorability.lean, Graph/Colorability3/FromSat.lean) — the two problems ask different questions of one Garey–Johnson instance — a graph and a number, read as the palette size — so they share an instance type, with 3-COLORABILITY the k = 3 restriction, promoted to its own entry as 3SAT is. 3-COLORABILITY is hard from unrestricted SAT (the palette gadget: a T/F/B triangle names the colours, a polarity pair per variable is the assignment, a chain of OR components per clause checks it; seeding each chain at a vertex forced to F's colour handles clauses of every width uniformly). K-COLORABILITY is hard from 3-COLORABILITY by weakening (a program tests the palette size, as the 3SAT → SAT weakening tests clause width).
• CLIQUE COVER (Graph/CliqueCover.lean) — hard from K-COLORABILITY (complementation: a clique of Gᶜ is an independent set of G, so splitting Gᶜ into k cliques is colouring G with k colours); Garey–Johnson's PARTITION INTO CLIQUES [GT15]. The predicate is defined as a partition into cliques rather than as Gᶜ.Colorable k — the second definition would make the reduction true by definition and prove nothing.
• SIMPLE MAX CUT (Graph/MaxCut.lean) — hard from MAX 2SAT (Garey–Johnson–Stockmeyer's Theorem 1.2: a splitting pass first makes every clause a distinct two-literal pair over one fresh variable per clause; then the GJS framework — two rails joined completely bipartitely, a ladder of 3q + 1 disjoint 3-edge paths per variable, a pair edge plus two rail attachments per clause — makes an aligned bipartition cut exactly |A₁| + 2·(satisfied pairs), while misalignment costs more than the clause edges can repay). Unit weights only; the weighted MAX CUT [ND16] waits for a weights convention, and this entry will become its restriction.
• HAMILTONIAN CIRCUIT (Graph/HamiltonianCircuit.lean) — hard from VERTEX COVER (Garey–Johnson's Theorem 3.4: a twelve-node cover-testing component per edge, the components at a vertex strung into a chain, and k selector nodes joined to both ends of every chain, so that a circuit may enter exactly k chains). The predicate is deliberately not mathlib's SimpleGraph.IsHamiltonian, whose one-vertex convention would leak into every gadget proof.
• HAMILTONIAN PATH (Graph/HamiltonianPath.lean) — hard from HAMILTONIAN CIRCUIT (Garey–Johnson [GT39]: duplicate a distinguished vertex and hang a pendant off each copy; a pendant has one neighbour, so it must be an end of any Hamiltonian path, and the path between the pendants glues back into a circuit). The gluing is sound only with three or more vertices, so the reduction branches, the degenerate side answering with the empty graph.
• TRAVELING SALESMAN (Networks/TravelingSalesman.lean) — hard from HAMILTONIAN CIRCUIT (Garey–Johnson [ND22], and Karp's: distance 1 along an edge, 2 across a non-edge, budget the number of cities, so a tour comes in on budget exactly when every step is an edge). The entry states the symmetric problem GJ states — distances are ℕ with symmetry carried as a field — and its real content is a change of representation: TSP quantifies over orderings of the cities where HAMILTONIAN CIRCUIT quantifies over walks, bridged once by exists_isHamiltonianCycle_iff_exists_equiv (Hamiltonicity.lean).
• SET COVER (Sets/SetCover.lean) — hard from VERTEX COVER (cover the edges by vertex stars: a vertex's set is its incident edges, and k stars cover the ground set iff the k vertices cover the graph).
• HITTING SET (Sets/HittingSet.lean) — hard from VERTEX COVER (a vertex cover is a hitting set of the edge system). SET COVER's dual, over the same instance type: the two problem statements are each other's with the roles of positions and elements exchanged.
• SET PACKING (Sets/SetPacking.lean) — hard from INDEPENDENT SET and from CLIQUE (the same vertex-star system that SET COVER uses, read the other way round: two distinct vertices are non-adjacent exactly when their stars are disjoint). Composed with complementation, CLIQUE → SET PACKING is Karp's original reduction, whose ground elements are the non-edges.
• 3-DIMENSIONAL MATCHING (Sets/Matching3D.lean) — hard from SAT and from 3SAT (Garey–Johnson's three-part construction: truth-setting cycles per variable whose two perfect matchings are "all true" and "all false", satisfaction-testing triples per clause, and a garbage-collection component absorbing the released elements).
• EXACT COVER BY 3-SETS (Sets/ExactCover3.lean) — hard from 3-DIMENSIONAL MATCHING, and hence from SAT and 3SAT (merge the three coordinate sets into a disjoint union; the sets are automatically 3-element because the three coordinates land in three different summands).
• SUBSET SUM (Numbers/SubsetSum.lean) — hard from VERTEX COVER (Karp's base-4 digit construction: one digit position per edge plus a high vertex-counting digit; an edge has only two endpoints, so no digit exceeds 3 and no carries occur).
• PARTITION (Numbers/Partition.lean) — hard from SUBSET SUM (adjoin two padding elements, sum + 1 − t and t + 1: an even split must separate them, and the side of the first one, minus the padding, sums to the target).
• KNAPSACK (Numbers/Knapsack.lean) — hard from SUBSET SUM (sizes and values both the given numbers, so the capacity bounds from above exactly what the goal bounds from below).

Twenty-five problems and forty-one reductions, every one certified end to end. Keeping the correctness catalog and the certified catalog equal is the standing milestone — the library's thesis is that certification is cheap enough to be universal — so a new entry lands with its certificate or acquires one before the next entry starts. Certified reductions compose (the certificate of a composite is the composite program), and every entry carries its representation theorems (<Domain>/Representation.lean, all five domains): each abstract problem reduces to its concrete encoding and back, so the certified pipeline's conclusions transfer to the abstract problems by composition.

What exactly is proven

For every reduction in the catalog:

• a machine-checked equivalence P x ↔ Q (map x) for every instance x — including degenerate ones (empty formulas, empty clauses, isolated vertices, thresholds exceeding the vertex count). There are no well-formedness side conditions and no "WLOG".

For every certified reduction — today, all of them — additionally:

• the instance map is a program of the Code language, correct with respect to total decoding of concrete instances, and therefore of polynomially bounded cost and output size by the generic theorem.

Not proven, by design:

• anything about Turing machines, P, NP, or NP-completeness — there is no formal statement "SAT is NP-complete" here, and no claim of membership in NP for any problem;
• the connection between the Code cost model and a machine model (the deferred bridge above);
• the adequacy of the cost model, which is a design judgment enforced by discipline rather than by a theorem. The discipline is spelled out below, so it can be audited. (The adequacy of the encodings is deliberately not on this list: for every problem in the catalog it is the theorem pair of its domain's Representation.lean.)

Size discipline

The certificates are only as honest as the size model, so the library follows strict rules, chosen to make the eventual bridge theorem true rather than convenient:

• Explicit element lists. Graph instances carry an explicit vertex list (isolated vertices are represented); SUBSET SUM instances carry a list of numbers (duplicates are distinct items). Instance size is never measured by a succinct proxy.
• Numbers cost their bit length, and no Code combinator can iterate a number of times given by a number's value — only list lengths drive iteration. Exponentiation is the sharp case: natPowLen takes its exponent from a list, never from a number, so a program wanting b ^ j must exhibit a list of length j. Base-4 place values are therefore exponentially large numbers of only linearly many bits.
• Fresh names are tagged tuples. Gadget constructions never generate fresh objects from a counter; a fresh vertex or variable is a tagged tuple of input objects (an occurrence is "clause × position within it"), so instance maps stay structural. A concrete instance has only ℕ labels, so a certificate has to realize those tags as numbers; it does so with an injective pairing (Code.natPair), and the reduction proof asks nothing of the realization but injectivity (CNF.satisfiable_relabel).
• Junk-tolerant decoding. Concrete instances decode totally: a graph's vertices are the positions of its vertex list, its edges are the in-range index pairs, everything else is ignored. Every value means something, so no well-formedness predicates infect the statements.

The discipline has visible mathematical consequences. For instance, the DOMINATING SET reduction has threshold k + (number of isolated vertices) where the textbook says "WLOG assume no isolated vertices": the WLOG is a preprocessing pass that a formal reduction has to either implement or, as here, absorb into the construction.

Restrictions: "hard even if"

Garey and Johnson's "remains NP-complete even if …" is first-class and promise-free: P.restrict R conjoins the side condition into the predicate (fun x ↦ R x ∧ P x), so a reduction into a restriction is exactly a hardness-even-if proof, and no promise infects the instance types. Reduction.codRestrict builds such a reduction from one whose gadgets satisfy R by construction; weakening in the other direction (Reduction.ofRestrict) requires the restriction to be decidable — the classical requirement that promises be checkable falls out of the formalization by itself. The bounded-occurrence 3SAT entry is the model instance of the pattern.

Building

Requires the Lean toolchain pinned in lean-toolchain (elan installs it automatically) and mathlib's build cache:

lake exe cache get
lake build

CI builds every push. API documentation is generated with doc-gen4 and published at https://dominikpeters.github.io/HardnessReductionsLean/.

Three documents carry the working conventions: CLAUDE.md for the architecture and file layout, STYLE.md for how to state a reduction, build a gadget, write a certificate annex, and get past the tactic failures that recur here, and ROADMAP.md for what is next.

Roadmap

The library is a growing prototype; ROADMAP.md keeps the prioritized queue. The standing themes:

• Aggregation in Code. The language deliberately has no general fold — an unrestricted fold would break the once-and-for-all polynomial theorem, since accumulators can grow exponentially. Instead, bounded aggregates are added one at a time, each paying for its own case of the polynomial theorem (listSum and the length-indexed exponentiation natPowLen are the two admitted so far). An operation is eligible exactly when its output size is bounded by the input's bit content, and it must carry its own case of the blanket theorem.
• More catalog entries and restrictions. Garey–Johnson's "six basic problems" (3SAT, 3DM, VERTEX COVER, PARTITION, HAMILTONIAN CIRCUIT, CLIQUE) are all present; the queue now favours entries that stress something new — a new instance shape, domain folder, combinator, or proof pattern — with STEINER TREE and the weighted problems of the Networks/ domain next.
• The machine-model bridge, once mathlib has a formalization of polynomial-time computation to bridge to.