{"id":"palomar/PALOMAR-2026-10-30-000013","url":"https://github.com/IanMcNelly/lean4-tsp-complexity-christofides/tree/73c122b96051de95d29b6977cdc2a10b56e2af2b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000013-v1.json","repo":"https://github.com/IanMcNelly/lean4-tsp-complexity-christofides","tags":["cs.DS","cs.CC","math.CO","cs.LO","msc:68W25","msc:68Q17","msc:90C27","msc:05C45","msc:03B35"],"score":0,"title":"Machine-Checked Christofides 3/2-Approximation and Polyhedral Complexity Barriers for the Traveling Salesperson Problem in Lean 4","trust":"high","domain":"cs.DS","source":"palomar","authors":["Ian McNelly"],"reviews":0,"subject":"cs.DS","summary":"This formalization develops a machine-checked theory of the Traveling Salesperson Problem (TSP) on finite undirected graphs over Fin n in Lean 4 across two principal modules. First, in Christofides.lean (compared against ChallengeChristofides.lean), we formalize the complete Christofides-Serdyukov 3/2-approximation algorithm for Metric TSP: the Minimum Spanning Tree (MST) lower bound (cost(T) = 2/3 on all nontrivial cuts; Yannakakis DFJ slack matrix nonnegativity and conditional Fiorini-Rothvoss PSD extension complexity scaling; and polynomial-time reductions from Hamiltonian Cycle and…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem","identifier":"https://apps.dtic.mil/sti/citations/ADA025602","relationship":"formalizes"},{"title":"O nekotorykh ekstremal'nykh obkhodakh v grafakh (On some extremal walks in graphs)","identifier":"","relationship":"formalizes"},{"title":"Solution of a Large-Scale Traveling-Salesman Problem","identifier":"https://doi.org/10.1287/opre.2.4.393","relationship":"formalizes"},{"title":"The Traveling-Salesman Problem and Minimum Spanning Trees","identifier":"https://doi.org/10.1287/opre.18.6.1138","relationship":"formalizes"},{"title":"Expressing Combinatorial Optimization Problems by Linear Programs","identifier":"https://doi.org/10.1016/0022-0000(91)90024-Y","relationship":"adapts"}]}