MaxSNP-completeness and APX-completeness of MAX-3-SAT and 3-OCCURRENCE MAX-3-SAT (the PCP theorem and hardness of approximation) in Lean 4
A Lean 4 proof of the PCP theorem and of its consequences for approximation, for an explicit single-tape Turing machine model. The compared theorems are: the PCP theorem in gap form, that for a fixed fraction num/den > 0 every NP language reduces in polynomial time to 3-SAT so that members give satisfiable formulas and non-members give formulas of which every assignment leaves at least that fraction of the clauses unsatisfied (Complexity.pcp_gap); the PCP theorem in verifier form, NP = PCP(O(log n), O(1)) (Complexity.pcp_theorem); that the problems of the syntactic class MaxSNP0 are in NPO…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-09-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-09-000010/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-09-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'