{"id":"palomar/PALOMAR-2026-10-02-000013","url":"https://github.com/RBarish-UTokyo/NPCompleteness-Lean4/tree/3e603e795b44fedcf7d6dd65b7d1e30547ead925","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-02-000013-v1.json","repo":"https://github.com/RBarish-UTokyo/NPCompleteness-Lean4","tags":["cs.CC","cs.LO","msc:68Q17","msc:68Q15","msc:03D15","msc:68Q04","msc:68V20","complexity-theory","satisfiability","lean-formalization"],"score":0,"title":"NP-completeness of SAT, 3-SAT and their variants (the Cook–Levin theorem) in Lean 4","trust":"high","domain":"cs.CC","source":"palomar","authors":["Robert D. Barish"],"reviews":0,"subject":"cs.CC","summary":"A Lean 4 proof of the Cook–Levin theorem and of the NP-completeness of several variants of satisfiability, for an explicit machine model, using only Lean's core library. The compared theorems state that the following languages are NP-complete: SAT, the set of binary codes of satisfiable CNF formulas (Complexity.sat_np_complete); 3-SAT, with at most three literals per clause (threeSAT_np_complete); exactly-3-SAT, with exactly three literals per clause on three distinct variables (exactThreeSAT_np_complete); (≤1,≤2)-SAT, with two or three literals per clause and every variable occurring at…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-02","reactions":{},"formalized":true,"formalizes":[{"title":"The complexity of theorem-proving procedures","identifier":"doi:10.1145/800157.805047","relationship":"formalizes"},{"title":"Reducibility among combinatorial problems","identifier":"doi:10.1007/978-1-4684-2001-2_9","relationship":"formalizes"},{"title":"A simplified NP-complete satisfiability problem","identifier":"doi:10.1016/0166-218X(84)90081-7","relationship":"adapts"},{"title":"Planar formulae and their uses","identifier":"doi:10.1137/0211025","relationship":"adapts"},{"title":"Computational Complexity: A Modern Approach","identifier":"ISBN 978-0-521-42426-4","relationship":"formalizes"}]}