{"id":"palomar/PALOMAR-2026-10-26-000001","url":"https://github.com/jtraverso/regular-subgraphs/tree/daea9b30d10bfae6c75ba7be5904080119bbbdba","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-26-000001-v1.json","repo":"https://github.com/jtraverso/regular-subgraphs","tags":["math.CO","msc:05C70","msc:05C07","msc:11T06"],"score":0,"title":"Regular subgraphs of almost regular graphs (Alon–Friedland–Kalai)","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the Alon–Friedland–Kalai theorem for primes: for a prime p, every finite simple graph with maximum degree at most 2p − 1 and average degree greater than 2p − 2 contains a p-regular subgraph (a nonempty subgraph with all degrees 0 or p); as a corollary, every 4-regular graph plus an edge contains a 3-regular subgraph. The prime-power case of the paper is not stated. The proof uses Mathlib's Chevalley–Warning theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-26","reactions":{},"formalized":true,"formalizes":[{"title":"Regular subgraphs of almost regular graphs","identifier":"doi:10.1016/0095-8956(84)90047-9","relationship":"formalizes"}]}