The Cook-Levin Theorem: SAT is NP-Complete
ProvedCookLevin.cook_levin_theoremcomplexity-theorycook-levinnp-completeness
The Cook-Levin theorem states that the Boolean satisfiability problem (SAT) is NP-complete, given polynomial-time verifier decider and reduction computation machines.
Preamble
import Definitions.Def_CookLevin_Verifier import Definitions.Def_CookLevin_Reduction
Formal statement
namespace CookLevin
theorem cook_levin_theorem (h1 : PolyTimeDecidable satVerifier) (h2 : ReductionIsPolyTime) :
NPComplete SAT := by sorry
end CookLevinSource
Read-back
What the Lean code literally says, in plain math · gemini-3.6-flash
This theorem asserts that the language SAT is NP-complete (i.e. NPComplete SAT), conditional on two hypotheses: h1 : PolyTimeDecidable satVerifier, asserting that the verifier function satVerifier is decided by a multi-tape Turing machine in polynomial time; and h2 : ReductionIsPolyTime, asserting that the tableau reduction function cookLevinReduction is computable by a multi-tape Turing machine in polynomial time.
Human review
Confirmed by the mission captain (proposal self-audit).