Resolving Erdős–Ulam Monochromatic Union-Closed Family Conjectures

Abstract

We prove both Erdős–Ulam conjectures on monochromatic union-closed families, which are the two specific questions of Erdős Problem 1183. Every two-colouring of the subsets of a finite set contains a monochromatic union-closed family whose size grows faster than any fixed power of the size of the set, while suitable colourings admit no monochromatic union-closed family of exponential size. Both results hold for any number of colours. For families closed under union and intersection, the forced size f(n) satisfies 13n/24 ≤ f(n) ≤ (2+o(1)) n log2 n, so it exceeds the chain bound and is determined up to a logarithmic factor. The exact orders of f(n) and F(n), which the problem also asks for, remain open. This record contains the paper (PDF and LaTeX source with TikZ figures) and the Lean 4 formalisation with Mathlib. Every theorem, proposition and corollary of the paper, and every lemma except Lemmas 7.3 and 7.4, is checked in Lean with no sorry. In place of those two lemmas, the formal proof of Lemma 7.1 uses a finite check evaluated by the Lean kernel. Each audited statement uses only the standard axioms propext, Classical.choice and Quot.sound. Claude (Anthropic) assisted with the coding.