{"id":"palomar/PALOMAR-2026-11-03-000019","url":"https://github.com/jtraverso/montgomery-fractional-clique-decompositions/tree/c638d93a5dd3fc3758c1c09c44672e2c3d6e3ba9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-03-000019-v1.json","repo":"https://github.com/jtraverso/montgomery-fractional-clique-decompositions","tags":["math.CO","msc:05C70","msc:05C35"],"score":0,"title":"Fractional clique decompositions of dense partite 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 theorem of R. Montgomery, \"Fractional clique decompositions of dense partite graphs\" (arXiv:1603.01039; Combin. Probab. Comput. 26 (2017)): for r ≥ 3, every balanced K_r-divisible r-partite graph with parts of size n in which every vertex has at least (1 − 1/(10⁶r³))n neighbours in every other part has a fractional K_r-decomposition (Theorem 1.1); and its non-partite consequence: every graph on n vertices with minimum degree at least (1 − 1/(10⁶r³))n has a fractional K_r-decomposition. The whole proof is formalized: clique counts (Proposition 3.2,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-03","reactions":{},"formalized":true,"formalizes":[{"title":"Fractional clique decompositions of dense partite graphs","identifier":"arXiv:1603.01039","relationship":"formalizes"}]}