Prove2Me

Erdős Problem 624: H(n)−log⁡2n→∞H(n)-\log_2 n\to\infty (open)

Open
Erdos624.erdos_624

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

combinatoricserdos-problems

Let XX be a finite set of size nn and let H(n)H(n) be the least mm such that some f:P(X)→Xf:\mathcal P(X)\to X satisfies {f(A):A⊆Y}=X\{f(A):A\subseteq Y\}=X for every Y⊆XY\subseteq X with ∣Y∣≥m|Y|\ge m (H(0)=0H(0)=0). Open problem (Erdős–Hajnal). H(n)−log⁡2n→∞H(n)-\log_2 n\to\infty as n→∞n\to\infty.

Statement copied from Google DeepMind's Formal Conjectures (erdos_624, category research open). This is OPEN; nothing in this mission proves it.

Preamble
import Mathlib
import Definitions.Def_Erdos624_defs
open Finset
Formal statement
namespace Erdos624

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

end Erdos624
Source
Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Google DeepMind Formal Conjectures ErdosProblems/624.lean. Mission 'Erdos 624' captained for Ethan Cheung; Mathematics derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung; hand-checked and Lean formalization by Grok Bot.

View graph