Introduction

The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.

Main Goal

Prove CookLevin.cook_levin_theorem:

$$NPComplete SAT$$

under the decider and reduction hypotheses.

We formalize the equivalence between Turing machines and the WordRAM model of computation. Turing machines are the standard model for studying computability, but algorithms are rarely described in terms of tape operations. WordRAM is much closer to assembly, with memory accesses, arithmetic instructions, branches, and loops. The goal is to connect this familiar way of expressing algorithms to the foundations of computability. This will also bring us closer to one day formalizing Fine Grained Complexity.

The formal target is halting equivalence through simulations in both directions, with the stated memory bounds and a family of word widths, each fixed during a run.

References:

• Stephen A. Cook and Robert A. Reckhow. Time Bounded Random Access Machines. Journal of Computer and System Sciences 7(4), 354–375, 1973.
• Torben Hagerup. Sorting and Searching on the Word RAM. STACS 1998, 366–398.

We establish the polynomial simulation needed for WordRAM-based NP proofs. It reuses the same machines and Cook–Levin definitions, with uniform programs, logarithmic word widths, and standard bit input/output.

The targets cover function outputs and verifier verdicts, including loading and serialization costs.

This adapts Cook–Reckhow’s Theorem 2(a), pp. 361–363, to Hagerup’s bounded-word operations, including multiplication; no particular simulation exponent is prescribed.

References:

• Stephen A. Cook and Robert A. Reckhow. Time Bounded Random Access Machines. Journal of Computer and System Sciences 7(4), 354–375, 1973.
• Torben Hagerup. Sorting and Searching on the Word RAM. STACS 1998, 366–398.

Prove that $k$-SAT is NP-complete for every fixed $k\ge3$, with at most $k$ literal occurrences per clause.

Construct the reductions and certificate verifier using the existing WordRAM definitions. We reuse proved polynomial backend and Cook–Levin SAT completeness.

References:

• Richard M. Karp. Reducibility Among Combinatorial Problems. Complexity of Computer Computations, 85–103, 1972. Main Theorem, problem 11; reduction, p. 98.
• Stephen A. Cook and Robert A. Reckhow. Time Bounded Random Access Machines. Journal of Computer and System Sciences 7(4), 354–375, 1973.
• Torben Hagerup. Sorting and Searching on the Word RAM. STACS 1998, 366–398.

Prove that subset sum is NP-complete by reducing the existing 3-SAT language, to it. Given a list of positive integers and a nonnegative target, decide whether some selection of entries sums exactly to the target. Integers are encoded in binary.

References:

• Richard M. Karp. Reducibility Among Combinatorial Problems. Complexity of Computer Computations, 85–103, 1972. Binary encoding convention, p. 89; Main Theorem, problem 18, pp. 94–95; original Exact Cover reduction, p. 100.