Problem 716

Let $\mathcal{F}$ be the family of all $3$ -uniform hypergraphs with $6$ vertices and $3$ $3$ -edges. Is it true that

\mathrm{ex}_3(n,\mathcal{F})=o(n^2)?

Source: erdosproblems.com/716

Graph theory
Hypergraphs

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

PROVED (LEAN): the site labels the problem PROVED (LEAN), notes that the question is a conjecture of Brown, Erdős and Sós [BES73], and credits the answer yes to Ruzsa and Szemerédi [RuSz78], the result known as the Ruzsa–Szemerédi or $(6,3)$ -theorem. The Lean qualification refers to a Lean 4 proof posted on the site's discussion thread on 2026-06-20 and held in Boris Alexeev's lean-proofs collection, linked from the Ruzsa and Szemerédi six-three theorem; this corpus has not built it.

BES73: Brown, W. G. and Erdős, P. and Sós, V. T., Some extremal problems on $r$ -graphs. New Directions in the Theory of Graphs (Proc. Third Ann Arbor Conf., Univ. Michigan, 1971), Academic Press (1973), 53-63.
RuSz78: Ruzsa, I. Z. and Szemerédi, E., Triple systems with no six points carrying three triangles. Combinatorics (Proc. Fifth Hungarian Colloq., Keszthely, 1976), Vol. II, Colloq. Math. Soc. János Bolyai 18, North-Holland (1978), 939-945. Not held.

Problem 716

Status

Proof claims

Discussion