Skip to content

Commit eb95f93

Browse files
henrykmichalewskihenrykmichalewski
authored
feat(ErdosProblems): add problems 533 and 579 (Ramsey–Turán with triangle-independence) (#4293)
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](https://claude.com/claude-code)
1 parent 47f1df0 commit eb95f93

2 files changed

Lines changed: 222 additions & 0 deletions

File tree

‎FormalConjectures/ErdosProblems/533.lean‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import FormalConjectures.Util.ProblemImports
18+
19+
/-!
20+
# Erdős Problem 533
21+
22+
*References:*
23+
- [erdosproblems.com/533](https://www.erdosproblems.com/533)
24+
- [EHSSS94] P. Erdős, A. Hajnal, M. Simonovits, V. T. Sós and E. Szemerédi,
25+
*Turán-Ramsey theorems and $K_p$-independence numbers*,
26+
Combin. Probab. Comput. **3** (1994), 297–325.
27+
- [ErRo62] P. Erdős and C. A. Rogers, *The construction of certain graphs*,
28+
Canad. J. Math. **14** (1962), 702–707.
29+
- [BaLe13] J. Balogh and J. Lenz, *On the Ramsey–Turán numbers of graphs and hypergraphs*,
30+
Israel J. Math. **194** (2013), 45–68.
31+
- [LRSS21] H. Liu, C. Reiher, M. Sharifzadeh and K. Staden,
32+
*Geometric constructions for Ramsey–Turán theory*,
33+
[arXiv:2103.10423](https://arxiv.org/abs/2103.10423) (2021).
34+
-/
35+
36+
open Classical Filter SimpleGraph
37+
38+
namespace Erdos533
39+
40+
/--
41+
Let $\delta > 0$. If $n$ is sufficiently large and $G$ is a graph on $n$ vertices with no
42+
$K_5$ and at least $\delta n^2$ edges, must $G$ contain a set of $\gg_\delta n$ vertices
43+
spanning no triangle?
44+
45+
Equivalently, writing $\mathrm{RT}_3(n, K_5, m)$ for the maximum number of edges of a
46+
$K_5$-free graph on $n$ vertices in which every triangle-free vertex set has fewer than $m$
47+
vertices (the *triangle Ramsey–Turán number*), is
48+
$$\delta_3(5) = \lim_{\epsilon \to 0} \lim_{n \to \infty}
49+
\frac{\mathrm{RT}_3(n, K_5, \epsilon n)}{n^2} = 0?$$
50+
51+
This is a problem of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94], who proved
52+
$\delta_3(5) \leq 1/12$ and the analogous $\delta_3(4) = 0$, and observed $\delta_3(7) \geq 1/4$
53+
via a construction of Erdős and Rogers [ErRo62].
54+
55+
The answer is **no**: Balogh and Lenz [BaLe13] disproved it by showing $\delta_3(5) > 0$, and
56+
the exact value $\delta_3(5) = 1/12$ was determined by the matching lower-bound construction of
57+
Liu, Reiher, Sharifzadeh, and Staden [LRSS21] (see `erdos_533.variants.lrss_lower`).
58+
-/
59+
@[category research solved, AMS 5]
60+
theorem erdos_533 : answer(False) ↔
61+
∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
62+
∀ G : SimpleGraph (Fin n), G.CliqueFree 5 →
63+
δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
64+
∃ S : Finset (Fin n), c * n ≤ (S.card : ℝ) ∧
65+
G.CliqueFreeOn (S : Set (Fin n)) 3 := by
66+
sorry
67+
68+
/--
69+
The upper bound $\delta_3(5) \leq 1/12$ of Erdős, Hajnal, Simonovits, Sós, and Szemerédi
70+
[EHSSS94]: for every $\epsilon > 0$ there is a $\delta > 0$ such that for all sufficiently
71+
large $n$, every $K_5$-free graph $G$ on $n$ vertices in which every triangle-free vertex
72+
set has at most $\delta n$ vertices has at most $(1/12 + \epsilon)n^2$ edges.
73+
-/
74+
@[category research solved, AMS 5]
75+
theorem erdos_533.variants.ehsss_upper (ε : ℝ) (hε : 0 < ε) :
76+
∃ δ : ℝ, 0 < δ ∧ ∀ᶠ n : ℕ in atTop,
77+
∀ G : SimpleGraph (Fin n), G.CliqueFree 5 →
78+
(∀ S : Finset (Fin n),
79+
G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) →
80+
(G.edgeFinset.card : ℝ) ≤ (1 / 12 + ε) * n ^ 2 := by
81+
sorry
82+
83+
/--
84+
The matching lower bound $\delta_3(5) \geq 1/12$, from the construction of Liu, Reiher,
85+
Sharifzadeh, and Staden [LRSS21] (improving the earlier $\delta_3(5) > 0$ of Balogh and Lenz
86+
[BaLe13]): for every $\epsilon, \delta > 0$ and all sufficiently large $n$ there is a
87+
$K_5$-free graph $G$ on $n$ vertices in which every triangle-free vertex set has at most
88+
$\delta n$ vertices, yet which has at least $(1/12 - \epsilon)n^2$ edges. In particular this
89+
refutes `erdos_533`.
90+
-/
91+
@[category research solved, AMS 5]
92+
theorem erdos_533.variants.lrss_lower (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
93+
∀ᶠ n : ℕ in atTop,
94+
∃ G : SimpleGraph (Fin n), G.CliqueFree 5 ∧
95+
(∀ S : Finset (Fin n),
96+
G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) ∧
97+
(1 / 12 - ε) * (n : ℝ) ^ 2 ≤ G.edgeFinset.card := by
98+
sorry
99+
100+
/--
101+
The contrasting positive result $\delta_3(4) = 0$ of Erdős, Hajnal, Simonovits, Sós, and
102+
Szemerédi [EHSSS94]: the $K_4$ analogue of `erdos_533` is **true**. For every $\delta > 0$
103+
there is a $c > 0$ such that for all sufficiently large $n$, every $K_4$-free graph $G$ on
104+
$n$ vertices with at least $\delta n^2$ edges contains a triangle-free vertex set of size at
105+
least $c n$.
106+
-/
107+
@[category research solved, AMS 5]
108+
theorem erdos_533.variants.delta_four_eq_zero :
109+
∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
110+
∀ G : SimpleGraph (Fin n), G.CliqueFree 4 →
111+
δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
112+
∃ S : Finset (Fin n), c * n ≤ (S.card : ℝ) ∧
113+
G.CliqueFreeOn (S : Set (Fin n)) 3 := by
114+
sorry
115+
116+
/--
117+
The observation $\delta_3(7) \geq 1/4$ of Erdős, Hajnal, Simonovits, Sós, and Szemerédi
118+
[EHSSS94], via a construction of Erdős and Rogers [ErRo62]: for every $\epsilon, \delta > 0$
119+
and all sufficiently large $n$ there is a $K_7$-free graph $G$ on $n$ vertices in which every
120+
triangle-free vertex set has at most $\delta n$ vertices, yet which has at least
121+
$(1/4 - \epsilon)n^2$ edges.
122+
-/
123+
@[category research solved, AMS 5]
124+
theorem erdos_533.variants.delta_seven_ge_quarter (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
125+
∀ᶠ n : ℕ in atTop,
126+
∃ G : SimpleGraph (Fin n), G.CliqueFree 7 ∧
127+
(∀ S : Finset (Fin n),
128+
G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) ∧
129+
(1 / 4 - ε) * (n : ℝ) ^ 2 ≤ G.edgeFinset.card := by
130+
sorry
131+
132+
/--
133+
Sanity check for the triangle-free-set condition: in the empty graph every vertex set spans
134+
no triangle, since the empty graph has no $3$-clique.
135+
-/
136+
@[category test, AMS 5]
137+
theorem erdos_533.variants.test_bot (n : ℕ) (S : Finset (Fin n)) :
138+
(⊥ : SimpleGraph (Fin n)).CliqueFreeOn (S : Set (Fin n)) 3 :=
139+
fun t _ h => cliqueFree_bot (by norm_num) t h
140+
141+
end Erdos533

‎FormalConjectures/ErdosProblems/579.lean‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import FormalConjectures.Util.ProblemImports
18+
19+
/-!
20+
# Erdős Problem 579
21+
22+
*References:*
23+
- [erdosproblems.com/579](https://www.erdosproblems.com/579)
24+
- [EHSS83] P. Erdős, A. Hajnal, V. T. Sós and E. Szemerédi, *More results on Ramsey–Turán
25+
type problems*, Combinatorica **3** (1983), 69–81.
26+
-/
27+
28+
open Classical Filter SimpleGraph
29+
30+
namespace Erdos579
31+
32+
/-- The octahedron $K_{2,2,2}$: the complete tripartite graph with all three parts of
33+
size $2$. -/
34+
abbrev octahedron : SimpleGraph (Σ _ : Fin 3, Fin 2) :=
35+
completeMultipartiteGraph (fun _ : Fin 3 => Fin 2)
36+
37+
/--
38+
Let $\delta > 0$. If $n$ is sufficiently large and $G$ is a graph on $n$ vertices with no
39+
$K_{2,2,2}$ (the octahedron) and at least $\delta n^2$ edges, must $G$ contain an independent
40+
set of size $\gg_\delta n$?
41+
42+
This is a problem of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]. It is **open**; they proved
43+
the statement for $\delta > 1/8$ (see `erdos_579.variants.ehss_large_delta`), and the
44+
difficulty is to push the edge-density threshold down to an arbitrary $\delta > 0$.
45+
46+
Here $K_{2,2,2}$ is the complete tripartite graph with all parts of size $2$, encoded as
47+
`completeMultipartiteGraph (fun _ : Fin 3 => Fin 2)`; "contains no $K_{2,2,2}$" is expressed
48+
via `SimpleGraph.Free`.
49+
-/
50+
@[category research open, AMS 5]
51+
theorem erdos_579 : answer(sorry) ↔
52+
∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
53+
∀ G : SimpleGraph (Fin n), octahedron.Free G →
54+
δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
55+
c * n ≤ (G.indepNum : ℝ) := by
56+
sorry
57+
58+
/--
59+
The partial result of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]: the statement of
60+
`erdos_579` holds whenever the edge-density coefficient exceeds $1/8$. That is, for every
61+
$\delta > 1/8$ there is a $c > 0$ such that for all sufficiently large $n$, every
62+
$K_{2,2,2}$-free graph $G$ on $n$ vertices with at least $\delta n^2$ edges has an independent
63+
set of size at least $c n$.
64+
-/
65+
@[category research solved, AMS 5]
66+
theorem erdos_579.variants.ehss_large_delta (δ : ℝ) (hδ : 1 / 8 < δ) :
67+
∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
68+
∀ G : SimpleGraph (Fin n), octahedron.Free G →
69+
δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
70+
c * n ≤ (G.indepNum : ℝ) := by
71+
sorry
72+
73+
/--
74+
Sanity check that the forbidden structure is non-trivial: the octahedron is of course not
75+
octahedron-free, since it contains a copy of itself.
76+
-/
77+
@[category test, AMS 5]
78+
theorem erdos_579.variants.octahedron_not_free : ¬ octahedron.Free octahedron :=
79+
fun h => h IsContained.rfl
80+
81+
end Erdos579

0 commit comments

Comments
 (0)