{"id":"palomar/PALOMAR-2026-11-04-000016","url":"https://github.com/jtraverso/plantholt-overfull-criterion/tree/f8900944da7743b1facd771139c9ebdbfd8aaa28","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-04-000016-v2.json","repo":"https://github.com/jtraverso/plantholt-overfull-criterion","tags":["math.CO","msc:05C15","msc:05C70"],"score":0,"title":"Plantholt's overfull criterion for graphs of high minimum degree, with 1-factorization theorems for dense regular graphs (6/7 and 11/12)","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Theorem 1.2 of M. Plantholt, Overfull conjecture for graphs with high minimum degree (J. Graph Theory 47, 2004), and of a 1-factorization theorem for dense regular graphs in the style of Chetwynd and Hilton (1989). theorem_1_2: if c ≥ 3/4 is such that every regular graph of even order n and degree at least c n is 1-factorizable, and G has even order n with (3δ − Δ)/2 ≥ c n, then G is Class 1 (χ′ = Δ) if and only if G has no Δ-overfull subgraph. lineGraph_colorable_of_isRegular: a d-regular graph of even order 2n with 11 n ≤ 6 d is d-edge-colourable, i.e.…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-05","reactions":{},"formalized":true,"formalizes":[{"title":"Overfull conjecture for graphs with high minimum degree","identifier":"doi:10.1002/jgt.20013","relationship":"formalizes"},{"title":"Regular graphs of high degree are 1-factorizable","identifier":"doi:10.1112/plms/s3-50.2.193","relationship":"formalizes"},{"title":"1-factorizing regular graphs of high degree—an improved bound","identifier":"doi:10.1016/0012-365X(89)90082-4","relationship":"adapts"}]}