Let $X$ be a finite set of size $n$ and $H (n)$ be such that there is a function $f : {A : A \subseteq X} \to X$ so that for every $Y \subseteq X$ with $∣ Y ∣ \geq H (n)$ we have ${f (A) : A \subseteq Y} = X .$ Prove that $H (n) - lo g_{2} n \to \infty.$

Worked, still open.

combinatorics · open · possible · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

I’m going to flag something important up front: the statement

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

AMS 5 · open (literature)

theorem erdos_624 :
    atTop.Tendsto (fun n : ℕ => H n - Real.logb 2 (n : ℝ)) atTop

open