Erdős and Ulam asked how large a monochromatic union-closed family must be in any colouring of the subsets of [n]. Erdős asked whether F(n) ≥ n^{ω(n)} for some ω(n)→∞ and whether F(n) < (1+o(1))^n. The question is listed as open as Problem 1183 in Bloom's collection.

The lower bound is built from monochromatic cubes inside block chains, using a Cauchy–Schwarz-type box inequality, supersaturation, and averaging over permutations and block-size vectors. The upper bound uses a random colouring together with independent systems and the Sauer–Shelah lemma. Further sections treat cardinality colourings via Hilbert cubes and arithmetic progressions, and bound the sublattice function using a Birkhoff-type description of sublattices. Everything is formalized in Lean 4 (v4.34.1) with Mathlib, with probabilistic arguments replaced by counting arguments.

Both conjectures are proved for any number of colours: F_k(n) grows faster than any fixed power of n, and F(n) ≤ n^{O(log n)}, which is subexponential. Lean confirms the proofs use only the standard axioms and contain no unproved steps.