Erdős Problem #644

The question

erdos_644.parts.i. Let $f(k,r)$ be minimal such that if $A_1,A_2,\dots$ is a family of sets, all of size $k$, such that for every collection of $r$ of the $A_{i}s$ there is some pair $\{x,y\}$ which intersects all of the $A_j$, then there is some set of size $f(k,r)$ which intersects all of the sets $A_i$. Is it true that $$f(k,7)=(1+o(1))\frac{3}{4}k?$$

erdos_644.parts.ii. Is it true that for any $r\ge 3$ there exists some constant $c_r$ such that $$f(k,r)=(1+o(1))c_{r}k?$$

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«644» (2 statements).

theorem erdos_644.parts.i :
    (fun k ↦ ((Hypergraph.subfamilyTransversalBound k 7 2).toNat : ℝ)) ~[atTop]
      (fun k ↦ (3 / 4 : ℝ) * k)

theorem erdos_644.parts.ii :
    ∀ r : ℕ, 3 ≤ r → ∃ c : ℝ, 0 < c ∧
    (fun k ↦ ((Hypergraph.subfamilyTransversalBound k r 2).toNat : ℝ)) ~[atTop]
      (fun k ↦ c * k)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/644. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/644
• [EFKT92] Erdős, P. and Fon-Der-Flaass, D. and Kostochka, A. V. and Tuza, Zs., Small transversals in uniform hypergraphs. Siberian Adv. Math. (1992), 82-88.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.