{"id":"palomar/PALOMAR-2026-10-29-000006","url":"https://github.com/jtraverso/erdos81-split-clique-partitions/tree/a98dfa413428b3c532174575a39f89eb32b268b8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000006-v1.json","repo":"https://github.com/jtraverso/erdos81-split-clique-partitions","tags":["math.CO","msc:05C70","msc:05C35"],"score":0,"title":"Linear-error clique partitions of split 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 the author's preprint \"Linear-Error Clique Partitions of Split Graphs via Structured Triangle Packing\" (Erdős #81 series, Paper III): there is an absolute constant C such that every finite split graph G on n vertices satisfies |E(G)| − 2ν₃(G) ≤ n²/6 + C·n, where ν₃(G) is the maximum number of pairwise edge-disjoint triangles (Theorem 1.1); consequently G has a clique partition (a family of cliques covering every edge exactly once) with at most n²/6 + C·n cliques (Corollary 1.2). The quadratic coefficient 1/6 is the sharp one for split…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"Linear-Error Clique Partitions of Split Graphs via Structured Triangle Packing","identifier":"doi:10.5281/zenodo.23478825","relationship":"formalizes"}]}