feat(ErdosProblems): add problems 533 and 579 (Ramsey–Turán with triangle-independence)

[henrykmichalewski]

fixes #775
fixes #806

Adds two closely-linked Ramsey–Turán problems (each cross-references the other on erdosproblems.com), following the framework established for problem 22 (ErdosProblems/22.lean).

ErdosProblems/533.lean — DISPROVED

For $\delta>0$ and large $n$: must every $K_5$-free graph on $n$ vertices with $\ge \delta n^2$ edges contain a triangle-free vertex set of size $\gg_\delta n$? Equivalently, is the triangle Ramsey–Turán density $\delta_3(5)=0$?

• erdos_533 — answer(False) (the density is not 0).
• variants.ehsss_upper — $\delta_3(5)\le 1/12$ (Erdős–Hajnal–Simonovits–Sós–Szemerédi).
• variants.lrss_lower — $\delta_3(5)\ge 1/12$ via the Liu–Reiher–Sharifzadeh–Staden construction (improving Balogh–Lenz's $\delta_3(5)>0$); refutes erdos_533.
• variants.delta_four_eq_zero — the contrasting positive $K_4$ result $\delta_3(4)=0$.
• variants.delta_seven_ge_quarter — the EHSSS observation $\delta_3(7)\ge 1/4$ (Erdős–Rogers).
• variants.test_bot — sanity check on the triangle-free-set condition.

The triangle-free-set condition uses SimpleGraph.CliqueFreeOn _ 3.

ErdosProblems/579.lean — OPEN

For $\delta>0$ and large $n$: must every $K_{2,2,2}$-free (octahedron-free) graph on $n$ vertices with $\ge \delta n^2$ edges contain an independent set of size $\gg_\delta n$?

• erdos_579 — answer(sorry) (open).
• variants.ehss_large_delta — the EHSS partial result for $\delta>1/8$.
• variants.octahedron_not_free — sanity check that the forbidden structure is non-trivial.

The octahedron is completeMultipartiteGraph (fun _ : Fin 3 => Fin 2); "contains no $K_{2,2,2}$" uses SimpleGraph.Free.

Both files build with only the expected declaration uses 'sorry' warnings.

🤖 Generated with Claude Code

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[mo271]

Thanks!
Looks great mathematically, just a nit about removing docstrings.

[mo271]

Suggested change

	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 could
	prove the statement for $\delta > 1/8$; the difficulty is to push the edge-density threshold
	all the way down to an arbitrary $\delta > 0$.
	Here $K_{2,2,2}$ is the complete tripartite graph with all parts of size $2$, i.e. the
	octahedron, encoded as `completeMultipartiteGraph (fun _ : Fin 3 => Fin 2)`. "Contains no
	$K_{2,2,2}$" is expressed via `SimpleGraph.Free`: $G$ contains no copy of the octahedron.

[henrykmichalewski]

Done in 9ce4159 — the module header is now just the title + references, with the statement (including the octahedron encoding note) moved into the erdos_579 docstring.

[mo271]

let's not repeat the docstrings

[henrykmichalewski]

Done — slimmed both module headers to just the title and the *References:* block, and moved the full verbatim problem statement into the erdos_533 / erdos_579 theorem docstrings, so the text now appears only once (per ErdosProblems/README.md). Pushed in 9ce4159.

[Smetalo]

Does this resolve #775 and #806?

[henrykmichalewski]

@Smetalo Thanks for checking! No — #533 and #579 are different problems from #775 and #806, so this PR doesn't touch them:

• Erdős Problem 533 #775 asks whether a 3-uniform hypergraph on $n$ vertices can have $n - O(1)$ different clique sizes (recently disproved by Gao). That's about clique-size diversity in hypergraphs, unrelated to the Ramsey–Turán edge-density questions here.
• Erdős Problem 579 #806 is an additive-combinatorics question about covering a set $A$ by a small sumset $B+B$ (Erdős–Newman).

This PR only adds #533 ($K_5$-free, triangle Ramsey–Turán density $\delta_3(5)=1/12$) and #579 (octahedron-free, independence). The two cross-reference each other on erdosproblems.com, which may be where the association came from.

[mo271]

Thanks again