Counting barrier for Erdős 624: $n\le 2^{H(n)}$ , i.e. $H(n)\ge\lceil\log_2 n\rceil$

Proved

Erdos624.counting_bound

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

combinatoricserdos-problems

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

n\le 2^{H(n)}\qquad\text{and hence}\qquad \lceil\log_2 n\rceil\le H(n).

A set $Y$ of size $m$ has only $2^m$ subsets, so its image under $f$ has at most $2^m$ elements. This is the trivial lower bound that Erdős Problem 624 asks to beat by an unbounded amount.

Formalization Note. $\lceil\log_2 n\rceil$ is Nat.clog 2 n.

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem counting_bound {n : ℕ} (hn : 0 < n) : n ≤ 2 ^ H n ∧ Nat.clog 2 n ≤ H n := by sorry

end Erdos624

Source

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

View graph

Counting barrier for Erdős 624: n≤2H(n)n\le 2^{H(n)}n≤2H(n), i.e. H(n)≥⌈log⁡2n⌉H(n)\ge\lceil\log_2 n\rceilH(n)≥⌈log2​n⌉

Counting barrier for Erdős 624: $n\le 2^{H(n)}$ , i.e. $H(n)\ge\lceil\log_2 n\rceil$