{"id":"palomar/PALOMAR-2026-11-04-000014","url":"https://github.com/jtraverso/cdr-bicolouring-sts/tree/a768a98a648e94ad38d0d84501867c999927c546","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-04-000014-v1.json","repo":"https://github.com/jtraverso/cdr-bicolouring-sts","tags":["math.CO","msc:05B07","msc:05C15","msc:05B15"],"score":0,"title":"Bicolouring Steiner triple systems (Colbourn–Dinitz–Rosa product, Dinitz–Stinson conditions)","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 product theorem of Colbourn, Dinitz and Rosa for bicoloured Steiner triple systems and of the necessary conditions of Dinitz and Stinson. A bicolouring of an STS colours the points so that every block receives exactly two colours. bicolourable3_mul (CDR 1999, Theorem 2.4): if there is an (a, b, c)-bicolourable STS(u) with c = max(a, b, c) and c ≤ a + b, and an (x, y, z)-bicolourable STS(v), then there is an (ax + by + cz, ay + bz + cx, az + bx + cy)-bicolourable STS(uv). Dinitz–Stinson Proposition 1.2: for a bicoloured STS on v points with colour…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-04","reactions":{},"formalized":true,"formalizes":[{"title":"Bicoloring Steiner Triple Systems","identifier":"doi:10.37236/1457","relationship":"formalizes"},{"title":"A Singular Direct Product for Bicolorable Steiner Triple Systems","identifier":"","relationship":"formalizes"},{"title":"A combinatorial theorem with an application to latin rectangles","identifier":"","relationship":"formalizes"},{"title":"Balanced schedules","identifier":"","relationship":"formalizes"}]}