{"id":"palomar/PALOMAR-2026-10-15-000011","url":"https://github.com/jtraverso/asymptotic-triangle-packing/tree/8c687e967e27800dc417203691c46044ec39c248","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000011-v1.json","repo":"https://github.com/jtraverso/asymptotic-triangle-packing","tags":["math.CO","msc:05C70","msc:05C35","msc:05C65","hypergraph-matchings","triangle-packing","formal-verification"],"score":0,"title":"Near-regular hypergraph matchings and the asymptotic triangle-packing gap","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of three results. (1) A finite nibble theorem: r-uniform hypergraphs whose degrees are at most (1+μ)d everywhere and at least (1−μ)d outside an exceptional set of at most η|V| vertices, with codegrees at most μd, have matchings with at least (1−β)|V|/r edges. (2) The fractional–integral triangle-packing gap is o(n²) uniformly over finite graphs: every large graph has an edge-disjoint triangle family P such that every fractional triangle packing has weight at most |P| + εn² (the triangle case of Haxell–Rödl). (3) The cover form: a fractional triangle cover of…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Integer and fractional packings in dense graphs","identifier":"doi:10.1007/s004930170003","relationship":"formalizes"}]}