A proof of the Colbourn–Dinitz–Rosa conjecture

In 1999 Colbourn, Dinitz and Rosa constructed all admissible profiles of order below 1000 and conjectured that every admissible profile occurs [1]. We prove their conjecture. Three prescribed positive class sizes occur in a strictly 3-bicolored Steiner triple system exactly when they satisfy the order congruence, the pair-count identity and the exclusion of two classes of size two. Our proof combines the product of Colbourn, Dinitz and Rosa with constructions by edge coloring. The regular remainder uses Chetwynd–Hilton; the narrow families use Plantholt, Cao–Chen–Jing–Shan, and vertex-distinguishing colorings. An exhaustive arithmetic check reduces the finite base to 49 profiles of order at most 487. Their existence already follows from Theorem 2.6 of [1]. English manuscript, Spanish translation, shared Lean companion, frozen sources and publication evidence. Publication repository. Manuscripts, companion and original figures: CC BY 4.0. Bundled Lean code retains its upstream licenses.