Skip to content

Erdős problem 794

Is it true that every 33-uniform hypergraph on 3n3n vertices with at least n3+1n^3+1 edges must contain either a subgraph on 44 vertices with 33 edges or a subgraph on 55 vertices with 77 edges?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

794.lean

Retained formal statement2 of 4

Balogh has observed that this problem is probably misstated by Erdős - indeed, every graph with 55 vertices spanning 77 edges contains a graph on 44 vertices spanning 33 edges, so the second condition can be dropped.

FormalConjectures/ErdosProblems/794.leanErdos794.erdos_794.variants.balogh2 linesExact file
∀ {V : Type u_1} [inst : DecidableEq V] (H : Finset (Finset V)),  H.IsThreeUniform → H.ContainsSubgraph 5 7 → H.ContainsSubgraph 4 3
SolvedStatement only, no proof