Trivial common hole for several maps $\mathcal P(U)\to U$ (Erdős 624)

Proved

Erdos624.commonHole

by Ethan Cheung Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problems

Theorem. Let $U$ and $I$ be finite sets, let $g_i:\mathcal P(U)\to U$ for $i\in I$ , and let $Y\subseteq U$ . If $|I|\cdot 2^{|Y|}<|U|$ , then some $u\in U$ is omitted by every $g_i$ on the subsets of $Y$ :

u\notin\bigcup_{i\in I}\{g_i(A):A\subseteq Y\}.

The union has at most $|I|\,2^{|Y|}$ elements. This is the counting-range common-hole lemma for Erdős Problem 624; it only works where $|Y|+\log_2|I|<\log_2|U|$ , so it gives no improvement over the counting bound $H(n)\ge\lceil\log_2 n\rceil$ .

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem commonHole {U ι : Type*} [Fintype U] [DecidableEq U] [Fintype ι]
    (g : ι → Finset U → U) (Y : Finset U) (h : Fintype.card ι * 2 ^ #Y < Fintype.card U) :
    ∃ u, ∀ i, ∀ A ⊆ Y, g i A ≠ u := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Formal Conjectures 624.lean; Claim B1 of claim from GPT 6.1 Sol (second answer, Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph

Trivial common hole for several maps P(U)→U\mathcal P(U)\to UP(U)→U (Erdős 624)

Trivial common hole for several maps $\mathcal P(U)\to U$ (Erdős 624)