Erdős problem 794 · problems.science

Is it true that every $3$ -uniform hypergraph on $3n$ vertices with at least $n^3+1$ edges must contain either a subgraph on $4$ vertices with $3$ edges or a subgraph on $5$ vertices with $7$ edges?

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

794.lean

Retained formal statement1 of 4

Is it true that every $3$ -uniform hypergraph on $3n$ vertices with at least $n^3+1$ edges must contain either a subgraph on $4$ vertices with $3$ edges or a subgraph on $5$ vertices with $7$ edges?

Harris has provided the following simple counterexample to the problem as stated: the $3$ -uniform graph on $\{1,\ldots,9\}$ with $28$ edges, formed by taking $27$ edges by choosing one element each from $\{1,2,3\},\{4,5,6\},\{7,8,9\}$ , and then adding the edge $\{1,2,3\}$ .

FormalConjectures/ErdosProblems/794.leanErdos794.erdos_7943 linesExact file

1False ↔2  ∀ (n : ℕ) (H : Finset (Finset (Fin (3 * n)))),3    H.IsThreeUniform → n ^ 3 + 1 ≤ H.card → H.ContainsSubgraph 4 3 ∨ H.ContainsSubgraph 5 7

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science