On the Erdős–Ulam problem for monochromatic union-closed families (Erdős Problem 1183): paper, code and Lean formalisation

Paper, code and Lean 4 formalisation for Erdős Problem 1183 (Erdős–Ulam). Let F(n) be the largest m such that every 2-colouring of the subsets of {1,…,n} contains a monochromatic union-closed family of m sets, and f(n) the analogous quantity for families closed under union and intersection. Both conjectures recorded for the problem are proved. First: for every t ≥ 1 there is ct > 0 with F(n) ≥ ct nt+1, so F(n) ≥ nω(n) for some ω(n) → ∞. The proof glues monochromatic cubes of a chain of disjoint blocks into one union-closed family, using a supersaturated two-letter Hales–Jewett theorem over random orderings and random block sizes. Second: F(n) ≤ Σj nd + 2 (random colouring and the Sauer–Shelah lemma), so F(n) ≤ n(1+o(1)) log₂ n and F(n) < (1+o(1))n. Both conjectures, stated as on erdosproblems.com, are machine-checked in Lean 4 with Mathlib, with no sorry and only Lean's standard axioms (propext, Classical.choice, Quot.sound). The paper also shows ⌈(n+1)/2⌉ ≤ f(n) < 12 n (log₂(n+2))², treats colourings by cardinality through Hilbert cubes and van der Waerden's theorem, and computes f(n) for n ≤ 10 and F(n) for n ≤ 7 with a SAT-based search, whose code and witnesses are included. Claude (Anthropic) assisted with the coding.