Cook–Levin theorem: SAT is NP-complete
ProvedCookLevin.sat_npCompletecook-levinnp-completenesssatturing-machine
Boolean satisfiability is NP-complete in the project’s multi-tape Turing machine model. The verifier and tableau-reduction computability obligations are discharged by verified machines; the conclusion has no additional hypotheses.
Preamble
import Definitions.Def_CookLevin_Verifier import Definitions.Def_CookLevin_Reduction open CookLevin
Formal statement
theorem CookLevin.sat_npComplete : NPComplete SAT := by sorry
Source
Unconditional conclusion of CookLevin.cook_levin_theorem (https://prove2.me/theorems/b5d75d8e-6bbb-49a3-bd6d-e25ba880e328), applying CookLevin.satVerifier_polyTimeDecidable and CookLevin.reductionIsPolyTime. Original formalization: https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Theorem.lean .