{"id":"palomar/PALOMAR-2026-10-15-000008","url":"https://github.com/jtraverso/dross-fractional-triangle-decomposition/tree/7720b7b591e606d5a56f1d935d8be650dcbf6c6f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000008-v1.json","repo":"https://github.com/jtraverso/dross-fractional-triangle-decomposition","tags":["math.CO","msc:05C70","msc:05C35","graph-theory","fractional-decomposition","formal-verification"],"score":0,"title":"Dross's theorem on fractional triangle decompositions","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Dross's theorem: every finite graph on n vertices with minimum degree at least 9n/10 has a fractional triangle decomposition, i.e. nonnegative real weights on its triangles such that every edge lies in triangles of total weight exactly one. The threshold 9/10 is the exact one of the paper. The proof follows the max-flow/min-cut approach: the existence of the weights is reduced to a flow problem, a finite max-flow/min-cut theorem (included) is applied, and every cut is bounded below by counting triangles and K4s, with a peeling reduction for heavy triangles.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Fractional Triangle Decompositions in Graphs with Large Minimum Degree","identifier":"doi:10.1137/15M1014310","relationship":"formalizes"}]}