$H(2^k)>k$ for $k\ge3$ (Erdős 624)

Proved

Erdos624.lt_H_two_pow

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

combinatoricserdos-problems

Let $|X|=n$ and let $H(n)$ be the least $m$ such that some $f:\mathcal P(X)\to X$ satisfies $\{f(A):A\subseteq Y\}=X$ for every $Y\subseteq X$ with $|Y|\ge m$ (Erdős Problem 624). Theorem. For every $k\ge3$ ,

H(2^k)\ge k+1.

This weak form of Erdős Problem 624 at powers of two was noted by Erdős as open and given a simple proof by Alon (see erdosproblems.com/624); here it is derived as a corollary of the robust Alon bound robust_alon_sum. It is not new.

Formalization Note. Uses the Formal Conjectures definition of $H$ on $\mathrm{Fin}\,n$ .

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem lt_H_two_pow (k : ℕ) (hk : 3 ≤ k) : k < H (2 ^ k) := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Formal Conjectures 624.lean; corollary of the robust Alon bound in claim from GPT 6.1 Sol (fourth answer, Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026); known (Alon, via erdosproblems.com/624)

View graph

H(2k)>kH(2^k)>kH(2k)>k for k≥3k\ge3k≥3 (Erdős 624)

$H(2^k)>k$ for $k\ge3$ (Erdős 624)