{"id":"palomar/PALOMAR-2026-11-01-000005","url":"https://github.com/jtraverso/triangle-decompositions-tripartite/tree/fd5c713e00cc03454878cdfc3acd8a7c9b0c19de","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000005-v3.json","repo":"https://github.com/jtraverso/triangle-decompositions-tripartite","tags":["math.CO","msc:05C70","msc:05B15"],"score":0,"title":"Triangle decompositions of dense tripartite graphs and completion of partial Latin squares","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Corollary 1.6 for r = 3 of Barber, Kühn, Lo, Osthus and Taylor, \"Clique decompositions of multipartite graphs and completion of Latin squares\" (J. Combin. Theory Ser. A 151 (2017), arXiv:1603.01043): fractional triangle decompositions above a threshold give triangle decompositions above the same threshold. Precisely: if δ ≥ 3/4 and, for every ε > 0, every K₃-divisible tripartite graph with three parts of size n ≥ n₀(ε) and minimum partite degree at least (δ + ε)n has a fractional triangle decomposition, then for every ε > 0 there is n₀ such that every…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Clique decompositions of multipartite graphs and completion of Latin squares","identifier":"doi:10.1016/j.jcta.2017.04.005","relationship":"formalizes"}]}