NP-completeness of SAT, 3-SAT and their variants (the Cook–Levin theorem) in Lean 4
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-02-000013
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-02-000013/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-02-000013/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'