Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `(3,4)-satisfiability is NP-hard`

conditional — 1 open assumptionproofs/Lax345332Proofs/Reduction.lean · lax-345332

What this proof establishes

thm×Lax345332.ThreeFourSat

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Satisfiability is NP-hard by the Cook–Levin theorem, the reduction is correct and runs in polynomial time, and polynomial-time many-one reductions compose.