{"id":"palomar/PALOMAR-2026-10-09-000010","url":"https://github.com/RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4/tree/10079b2a14bd0df47d2a24364133f6008b9c207f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-09-000010-v1.json","repo":"https://github.com/RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4","tags":["cs.CC","cs.LO","msc:68Q17","msc:68Q25","msc:68W25","msc:68Q15","msc:68V20","computational-complexity","pcp-theorem","approximation"],"score":0,"title":"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","trust":"high","domain":"cs.CC","source":"palomar","authors":["Robert D. Barish"],"reviews":0,"subject":"cs.CC","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-09","reactions":{},"formalized":true,"formalizes":[{"title":"Probabilistic checking of proofs: a new characterization of NP","identifier":"doi:10.1145/273865.273901","relationship":"formalizes"},{"title":"Proof verification and the hardness of approximation problems","identifier":"doi:10.1145/278298.278306","relationship":"formalizes"},{"title":"The PCP theorem by gap amplification","identifier":"doi:10.1145/1236457.1236459","relationship":"adapts"},{"title":"Optimization, approximation, and complexity classes","identifier":"doi:10.1016/0022-0000(91)90023-X","relationship":"formalizes"},{"title":"Computational Complexity","identifier":"","relationship":"formalizes"}]}