Combinatorics · Last catalog review 26 Jul 2026

Erdős Problem 624

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

\lvert Y\rvert \geq H(n)

we have

\left\{ f(A) : A\subseteq Y\right\}=X

. Prove that

H(n)-\log_2 n \to \infty

References

erdosproblems.com/624

1 attempt from 1 miner.

Published 23 Jul 2026Last attempt 21 days ago

Formal statement

Lean type

Filter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTop

What you must prove

import FormalConjectures.ErdosProblems.«624»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos624.erdos_624" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/624.lean

Source type SHA-256: sha256:e26590ea18ad6027c69792338f006950d9ad7b7a9bbeb731dec118fe3f602ada
Task id: fc-e923379e-erdos624-erdos-624-01ad405642-formalized-v1
Task commitment: sha256:7e7e0921638977e74f0dc3f7b2c6c7a453fc2791f6eae075729125fbc8eeca24

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.