Prove2Me

Erdős Problem 624: eventually surjective maps f:P(X)→Xf:\mathcal P(X)\to X and the threshold H(n)H(n)

Definition
Erdos624_defs

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

combinatoricserdos-problems

Let XX be a set of size nn (represented by Fin n\mathrm{Fin}\,n). ExistsEventuallySurjective nn mm holds if there is a map f:P(X)→Xf:\mathcal P(X)\to X such that for every Y⊆XY\subseteq X with ∣Y∣≥m|Y|\ge m,

{f(A):A⊆Y}=X.\{f(A):A\subseteq Y\}=X.

H(n)H(n) is the least such mm (and H(0)=0H(0)=0). Erdős Problem 624 asks to prove H(n)−log⁡2n→∞H(n)-\log_2 n\to\infty. Both definitions are copied verbatim from Google DeepMind's Formal Conjectures file for Problem 624.

Definition code
import Mathlib

namespace Erdos624

open Finset

/-- Verbatim from Formal Conjectures `FormalConjectures/ErdosProblems/624.lean`. -/
def ExistsEventuallySurjective (n m : ℕ) : Prop :=
  ∃ (f : Finset (Fin n) → Fin n),
    ∀ (Y : Finset (Fin n)), #Y ≥ m →
      Y.powerset.image f = Finset.univ

/-- Verbatim from Formal Conjectures: `H n` is the least admissible threshold `m` (and `0` for `n = 0`). -/
noncomputable def H (n : ℕ) : ℕ :=
  if 0 < n then
    sInf {m : ℕ | ExistsEventuallySurjective n m}
  else 0

end Erdos624
Source
Erdős Problem 624, https://www.erdosproblems.com/624; Formal Conjectures FormalConjectures/ErdosProblems/624.lean (ExistsEventuallySurjective, H)

View graph