{"id":"palomar/PALOMAR-2026-10-23-000015","url":"https://github.com/RBarish-UTokyo/MaxWeightIS-FPT-EulerGenusOddFaces-Lean4/tree/9d427d31eec04c5762495c296c846a5992bdb724","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000015-v1.json","repo":"https://github.com/RBarish-UTokyo/MaxWeightIS-FPT-EulerGenusOddFaces-Lean4","tags":["cs.DS","math.CO","msc:05C69","msc:05C10","msc:68Q25","msc:68R10","msc:68V20","algorithms","graph-embeddings","formal-verification"],"score":0,"title":"An FPT 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 a fixed-parameter theorem 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 integer vertex weights, the program outputs a maximum-weight independent set within 2^(c (p size(p) + 1)) (N size(M))^c bit operations,…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"Maximum-weight independent set in embedded graphs parameterized by Euler genus and number of odd faces","identifier":"","relationship":"formalizes"},{"title":"4-Block Integer Programming is in FPT","identifier":"arxiv:2609.26746v1","relationship":"adapts"}]}