{"id":"palomar/PALOMAR-2026-10-30-000008","url":"https://github.com/jtraverso/fractional-triangle-decompositions-tripartite/tree/d2331132eac8b9c9c1891ba14162745d567ebfdb","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000008-v1.json","repo":"https://github.com/jtraverso/fractional-triangle-decompositions-tripartite","tags":["math.CO","msc:05C70","msc:05B15","msc:90C05"],"score":0,"title":"Fractional triangle decompositions of dense tripartite graphs","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 main results of Allsop, Bowtell, Lesgourgues and Petrova, \"Improved bounds on completion of partial Latin squares\" (arXiv:2609.37877, 2026): there is η > 0 (here η = 1/20000) such that every K₃-divisible spanning subgraph of K_{n,n,n} with minimum partite degree at least (0.769 − η)n has a fractional triangle decomposition (Theorem 1.3). Also formalized: the Farkas characterization (Lemma 2.1); the reduction to triangle-covered, balanced, untied and nonzero edge weightings (Proposition 3.1, Corollary 3.5), with Lemma 3.4 proved through an integral…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"Improved bounds on completion of partial Latin squares","identifier":"arXiv:2609.37877","relationship":"formalizes"}]}