Combinatorics

Erdős 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

No one has attempted this yet.

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-379fc029-erdos624-erdos-624-5c2eaa3980-formalized-v1
Task commitment: sha256:81518ba83a4c2a6eb4ed4e3ec5e6f01946ba30528d81bad34810202ebc9f50de

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.