{"id":"palomar/PALOMAR-2026-10-22-000006","url":"https://github.com/RBarish-UTokyo/MaxWeightIS-XP-EulerGenusOddFaces-Lean4/tree/00f581e7401feedce30699ae94763d4afbfb2f6f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000006-v1.json","repo":"https://github.com/RBarish-UTokyo/MaxWeightIS-XP-EulerGenusOddFaces-Lean4","tags":["cs.DS","math.CO","msc:05C69","msc:05C10","msc:68Q25","msc:68R10","msc:68V20","graph-algorithms","independent-sets","formal-verification"],"score":0,"title":"An XP Algorithm for Maximum-Weight Independent Set in Embedded Graphs, in Lean 4","trust":"high","domain":"cs.DS","source":"palomar","authors":["Robert D. Barish"],"reviews":0,"subject":"cs.DS","summary":"A Lean 4 and Mathlib formalization of Theorem 1 of \"Maximum-weight independent set in embedded graphs parameterized by Euler genus and number of odd faces\" (forthcoming), with a provably correct implementation of the algorithm as one fixed program for an explicit sixteen-register pointer machine. Lean proves that for every graph drawn in a closed surface of Euler genus gamma whose complement has k regions of odd total boundary length, and all rational vertex weights, the program outputs a maximum-weight independent set within f(gamma + k) * N^(D(gamma, k) + C) * (L + 1)^b bit operations,…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Maximum-weight independent set in embedded graphs parameterized by Euler genus and number of odd faces","identifier":"","relationship":"formalizes"}]}