Catalog

Every problem here was open when it entered the pool.

Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.

Combinatorics

Erdős problem 579

Let

\delta > 0

. If

n

is sufficiently large and

G

is a graph on

n

vertices with no

K_{2,2,2}

(the octahedron) and at least

\delta n^2

edges, must

G

contain an independent set of size

\gg_\delta n

? This is a problem of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]. It is **open**; they proved the statement for

\delta > 1/8

(see erdos_579.variants.ehss_large_delta), and the difficulty is to push the edge-density threshold down to an arbitrary

\delta > 0

. Here

K_{2,2,2}

is the complete tripartite graph with all parts of size

2

, encoded as completeMultipartiteGraph (fun _ : Fin 3 => Fin 2); "contains no

K_{2,2,2}

" is expressed via SimpleGraph.Free.

References

erdosproblems.com/579

[EHSS83] P. Erdős, A. Hajnal, V. T. Sós and E. Szemerédi, More results on Ramsey–Turán type problems, Combinatorica 3 (1983), 69–81.

No one has attempted this yet.

Formal statement