diff --git a/FormalConjectures/ErdosProblems/1014.lean b/FormalConjectures/ErdosProblems/1014.lean new file mode 100644 index 000000000..c10f27401 --- /dev/null +++ b/FormalConjectures/ErdosProblems/1014.lean @@ -0,0 +1,76 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 1014 + +See also problems [544](https://www.erdosproblems.com/544) and +[1030](https://www.erdosproblems.com/1030). + +*References:* +- [erdosproblems.com/1014](https://www.erdosproblems.com/1014) +- [Er71] Erdős, P., _Some unsolved problems in graph theory and combinatorial analysis_. + Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97–109. +-/ + +open Filter SimpleGraph + +open scoped Topology + +namespace Erdos1014 + +/-- +Erdős Problem 1014 [Er71, p.99]: + +For fixed $k \geq 3$, +$$\lim_{l \to \infty} R(k, l+1) / R(k, l) = 1,$$ +where $R(k, l)$ is the Ramsey number. +-/ +@[category research open, AMS 5] +theorem erdos_1014 (k : ℕ) (hk : k ≥ 3) : + Tendsto (fun l : ℕ => + (graphRamseyNumber k (l + 1) : ℝ) / (graphRamseyNumber k l : ℝ)) + atTop (nhds 1) := by + sorry + +/-- +The $k = 3$ case of Erdős Problem 1014 [Er71]: + +$$\lim_{l \to \infty} R(3, l+1) / R(3, l) = 1.$$ + +This is already open. +-/ +@[category research open, AMS 5] +theorem erdos_1014.variants.k_eq_3 : + Tendsto (fun l : ℕ => + (graphRamseyNumber 3 (l + 1) : ℝ) / (graphRamseyNumber 3 l : ℝ)) + atTop (nhds 1) := by + sorry + +/-- +The $k = 2$ case of Erdős Problem 1014: $R(2, l+1) / R(2, l) \to 1$, since +$R(2, l) = l$ for all $l$. +-/ +@[category undergraduate, AMS 5] +theorem erdos_1014.variants.k_eq_2 : + Tendsto (fun l : ℕ => + (graphRamseyNumber 2 (l + 1) : ℝ) / (graphRamseyNumber 2 l : ℝ)) + atTop (nhds 1) := by + sorry + +end Erdos1014 diff --git a/FormalConjectures/ErdosProblems/1029.lean b/FormalConjectures/ErdosProblems/1029.lean new file mode 100644 index 000000000..7a2eb0c38 --- /dev/null +++ b/FormalConjectures/ErdosProblems/1029.lean @@ -0,0 +1,53 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 1029 + +*References:* +- [erdosproblems.com/1029](https://www.erdosproblems.com/1029) +- [ErSz35] Erdős, P. and Szekeres, G., *A combinatorial problem in geometry*, Compositio + Math. 2 (1935), 463–470. +- [Sp75] Spencer, J., *Ramsey's theorem — a new lower bound*, J. Combin. Theory Ser. A 18 + (1975), 108–115. +- [Er93] Erdős, P., *Some of my favorite solved and unsolved problems in graph theory*. + Quaestiones Math. (1993), 333–350. +-/ + +open Filter Finset SimpleGraph + +namespace Erdos1029 + +/-- +Erdős Problem 1029 [Er93, p.337]: + +$R(k) / (k \cdot 2^{k/2}) \to \infty$ as $k \to \infty$. + +Here $R(k)$ is the diagonal Ramsey number, expressed as `diagRamseyNumber k`. +-/ +@[category research open, AMS 5] +theorem erdos_1029 : + Tendsto (fun k : ℕ => + (diagRamseyNumber k : ℝ) / ((k : ℝ) * (2 : ℝ) ^ ((k : ℝ) / 2))) + atTop atTop := by + sorry + +-- TODO: Formalize the Erdős–Szekeres upper bound R(k) ≤ C(2k-2, k-1) and +-- Spencer's lower bound R(k) ≥ (1+o(1)) · (√2/e) · k · 2^{k/2}. + +end Erdos1029 diff --git a/FormalConjectures/ErdosProblems/1030.lean b/FormalConjectures/ErdosProblems/1030.lean new file mode 100644 index 000000000..c22f385fd --- /dev/null +++ b/FormalConjectures/ErdosProblems/1030.lean @@ -0,0 +1,104 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 1030 + +See also problems [544](https://www.erdosproblems.com/544) and +[1014](https://www.erdosproblems.com/1014). + +OEIS: [A000791](https://oeis.org/A000791), [A059442](https://oeis.org/A059442). + +*References:* +- [erdosproblems.com/1030](https://www.erdosproblems.com/1030) +- [Er93] Erdős, P., _Some of my favorite solved and unsolved problems in graph theory_. + Quaestiones Math. (1993), 333–350. +- [BEFS89] Burr, S.A., Erdős, P., Faudree, R.J., and Schelp, R.H., + _On the difference between consecutive Ramsey numbers_. Utilitas Math. (1989), 115–118. +-/ + +open Filter SimpleGraph + +open scoped Topology + +namespace Erdos1030 + +/-- +Erdős Problem 1030 [Er93, p. 339]: + +There exists $c > 0$ such that +$$ + \lim_{k \to \infty} \frac{R(k+1, k)}{R(k, k)} > 1 + c. +$$ +-/ +@[category research open, AMS 5] +theorem erdos_1030 : + ∃ c L : ℝ, c > 0 ∧ L > 1 + c ∧ + Tendsto (fun k : ℕ => + (graphRamseyNumber (k + 1) k : ℝ) / (graphRamseyNumber k k : ℝ)) + atTop (nhds L) := by + sorry + +/-- +Erdős Problem 1030 — eventually-larger variant [Er93, p. 339]: + +There exists $c > 0$ such that eventually (for all sufficiently large $k$), +$R(k+1, k) / R(k, k) \geq 1 + c$. This is implied by the limit formulation, but +is itself open since the limit need not exist. +-/ +@[category research open, AMS 5] +theorem erdos_1030.variants.eventually : + ∃ c : ℝ, c > 0 ∧ + ∀ᶠ k : ℕ in atTop, + (graphRamseyNumber (k + 1) k : ℝ) / (graphRamseyNumber k k : ℝ) ≥ 1 + c := by + sorry + +/-- +Weaker variant of Erdős Problem 1030 [Er93, p. 339]: + +There exists $c > 1$ such that $R(k+1,k) - R(k,k) > k^c$ for all sufficiently large $k$. + +Erdős and Sós could not even prove this weaker statement. +-/ +@[category research open, AMS 5] +theorem erdos_1030.variants.weak : + ∃ c : ℝ, c > 1 ∧ + ∀ᶠ k : ℕ in atTop, + (graphRamseyNumber (k + 1) k : ℝ) - (graphRamseyNumber k k : ℝ) > (k : ℝ) ^ c := by + sorry + +/-- +Trivial bound: $R(k+1, k) - R(k, k) \geq k - 2$ for all $k \geq 2$. +-/ +@[category research solved, AMS 5] +theorem erdos_1030.variants.trivial_bound : + ∀ k : ℕ, 2 ≤ k → + (k : ℤ) - 2 ≤ (graphRamseyNumber (k + 1) k : ℤ) - (graphRamseyNumber k k : ℤ) := by + sorry + +/-- +Burr–Erdős–Faudree–Schelp bound [BEFS89]: $R(k+1, k) - R(k, k) \geq 2k - 5$ for +all sufficiently large $k$. +-/ +@[category research solved, AMS 5] +theorem erdos_1030.variants.burr_erdos_faudree_schelp : + ∀ᶠ k : ℕ in atTop, + (2 * (k : ℤ) - 5) ≤ (graphRamseyNumber (k + 1) k : ℤ) - (graphRamseyNumber k k : ℤ) := by + sorry + +end Erdos1030 diff --git a/FormalConjectures/ErdosProblems/112.lean b/FormalConjectures/ErdosProblems/112.lean new file mode 100644 index 000000000..bb38547e8 --- /dev/null +++ b/FormalConjectures/ErdosProblems/112.lean @@ -0,0 +1,110 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 112 + +*References:* +- [erdosproblems.com/112](https://www.erdosproblems.com/112) +- [ErRa67] Erdős, P. and Rado, R., _Partition relations and transitivity domains of binary + relations_, J. London Math. Soc. (1967), 624–633. +- [LaMi97] Larson, J. and Mitchell, W., _On a problem of Erdős and Rado_, Ann. Comb. (1997), + 245–252. +-/ + +open Digraph SimpleGraph + +namespace Erdos112 + +/-- +Erdős Problem 112: Determine the directed Ramsey number $k(n,m)$. +-/ +@[category research open, AMS 5] +theorem erdos_112 : + ∀ n m : ℕ, 2 ≤ n → 2 ≤ m → + dirRamseyNumber n m = (answer(sorry) : ℕ → ℕ → ℕ) n m := by + sorry + +/-- Smallest open case: determine $k(3, 3)$. Known bounds: $7 \leq k(3,3) \leq 14$. -/ +@[category research open, AMS 5] +theorem erdos_112.variants.k_3_3 : + dirRamseyNumber 3 3 = answer(sorry) := by + sorry + +/-- Smallest open case: determine $k(3, 4)$. -/ +@[category research open, AMS 5] +theorem erdos_112.variants.k_3_4 : + dirRamseyNumber 3 4 = answer(sorry) := by + sorry + +/-- +Erdős–Rado upper bound [ErRa67]: +$$k(n,m) \leq \frac{2^{m-1} (n-1)^m + n - 2}{2n - 3}.$$ +-/ +@[category research solved, AMS 5] +theorem erdos_112.variants.erdos_rado_upper_bound : + ∀ n m : ℕ, 2 ≤ n → 2 ≤ m → + dirRamseyNumber n m ≤ (2 ^ (m - 1) * (n - 1) ^ m + n - 2) / (2 * n - 3) := by + sorry + +/-- +Larson–Mitchell bound [LaMi97]: $k(n, 3) \leq n^2$. +-/ +@[category research solved, AMS 5] +theorem erdos_112.variants.larson_mitchell : + ∀ n : ℕ, 2 ≤ n → + dirRamseyNumber n 3 ≤ n ^ 2 := by + sorry + +/-- The 3-color graph Ramsey number $R(a, b, c)$: the minimal $k$ such that every +symmetric 3-coloring of the edges of $K_k$ contains a monochromatic clique of size $a$, $b$, +or $c$ in the respective color. -/ +noncomputable def graphRamseyNum3 (a b c : ℕ) : ℕ := + sInf {k : ℕ | ∀ (col : Fin k → Fin k → Fin 3), (∀ x y, col x y = col y x) → + (∃ S : Finset (Fin k), S.card = a ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → col u v = 0) ∨ + (∃ S : Finset (Fin k), S.card = b ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → col u v = 1) ∨ + (∃ S : Finset (Fin k), S.card = c ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → col u v = 2)} + +/-- +Ramsey number sandwich (Hunter): $R(n,m) \leq k(n,m) \leq R(n,m,m)$, where $R$ is the +classical graph Ramsey number and $R(n,m,m)$ is the 3-color Ramsey number. The lower bound +holds because any undirected graph can be oriented, and the upper bound holds because the +three options for each pair of vertices (no edge, forward edge, backward edge) correspond +to a 3-coloring. +-/ +@[category research solved, AMS 5] +theorem erdos_112.variants.ramsey_sandwich : + ∀ n m : ℕ, 2 ≤ n → 2 ≤ m → + graphRamseyNumber n m ≤ dirRamseyNumber n m ∧ + dirRamseyNumber n m ≤ graphRamseyNum3 n m m := by + sorry + +/-- +Hunter–Steiner result: replacing "transitive tournament" with "directed path" in the +definition of $k(n,m)$ yields the exact answer $k(n,m) = (n-1)(m-1) + 1$. +-/ +@[category research solved, AMS 5] +theorem erdos_112.variants.hunter_steiner : + ∀ n m : ℕ, 2 ≤ n → 2 ≤ m → + dirPathRamseyNumber n m = (n - 1) * (m - 1) + 1 := by + sorry + +-- TODO: Formalize additional variants from erdosproblems.com/112 (e.g., exact values +-- for small cases, further bounds on k(n,m) for specific n,m). + +end Erdos112 diff --git a/FormalConjectures/ErdosProblems/129.lean b/FormalConjectures/ErdosProblems/129.lean new file mode 100644 index 000000000..920398b3b --- /dev/null +++ b/FormalConjectures/ErdosProblems/129.lean @@ -0,0 +1,104 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 129 + +*References:* +- [erdosproblems.com/129](https://www.erdosproblems.com/129) +- [Er97b] Erdős, P., *Some old and new problems in various branches of combinatorics*. + Discrete Math. (1997), 227–231. +-/ + +open Filter + +namespace Erdos129 + +/-- An $r$-edge-coloring of the complete graph $K_N$: a function that assigns a +color in $\operatorname{Fin} r$ to each ordered pair of vertices. +Note: this allows coloring of self-loops ($\chi\, x\, x$), which is semantically +meaningless for $K_N$ but harmless since `IsMonoKkFree` only examines pairs +with $x \ne y$. -/ +def EdgeColoring (N r : ℕ) : Type := Fin N → Fin N → Fin r + +/-- A vertex set $S$ is monochromatic-$K_k$-free in color $c$ under coloring $\chi$ if +there is no $k$-element subset of $S$ in which every pair of distinct vertices +receives color $c$. -/ +def IsMonoKkFree {N r : ℕ} (χ : EdgeColoring N r) (c : Fin r) + (k : ℕ) (S : Finset (Fin N)) : Prop := + ∀ T : Finset (Fin N), T ⊆ S → T.card = k → + ∃ x ∈ T, ∃ y ∈ T, x ≠ y ∧ χ x y ≠ c + +/-- The generalized Ramsey number $R(n; k, r)$: the smallest $N$ such that for +every symmetric $r$-coloring of the edges of $K_N$ (i.e., $\chi\, x\, y = \chi\, y\, x$), +there exists a set of $n$ vertices and a color $c$ such that the set is +$K_k$-free in color $c$. -/ +noncomputable def multicolorRamseyNum (n k r : ℕ) : ℕ := + sInf {N : ℕ | ∀ (χ : EdgeColoring N r), (∀ x y, χ x y = χ y x) → + ∃ (S : Finset (Fin N)) (c : Fin r), + S.card = n ∧ IsMonoKkFree χ c k S} + +/-- +Erdős–Gyárfás Conjecture (Problem 129) [Er97b]: +For every $r \geq 1$, does there exist a constant $C = C(r) > 1$ such that +$R(n; 3, r) < C^{\sqrt{n}}$ for all positive integers $n$? + +The conjecture is **disproved** (`answer(False)`): as observed by Antonio Girao, +a probabilistic coloring of $K_N$ (each edge independently uniformly at random +in $r$ colors) shows $R(n; 3, 2) \geq C^n$ for some $C > 1$, which grows faster +than $C^{\sqrt{n}}$, contradicting the conjectured upper bound. +-/ +@[category research solved, AMS 5] +theorem erdos_129 : answer(False) ↔ + ∀ r : ℕ, 1 ≤ r → + ∃ C : ℝ, 1 < C ∧ + ∀ n : ℕ, (multicolorRamseyNum n 3 r : ℝ) < C ^ Real.sqrt (n : ℝ) := by + sorry + +/-- +Lower bound proved by Erdős and Gyárfás [Er97b]: for every $r \geq 1$, +there exists a constant $C = C(r) > 1$ such that $R(n; 3, r) > C^{\sqrt{n}}$ +for all positive integers $n$. +-/ +@[category research solved, AMS 5] +theorem erdos_129_lower_bound : + ∀ r : ℕ, 1 ≤ r → + ∃ C : ℝ, 1 < C ∧ + ∀ n : ℕ, 1 ≤ n → + C ^ Real.sqrt (n : ℝ) < (multicolorRamseyNum n 3 r : ℝ) := by + sorry + +/-- +Generalized Erdős–Gyárfás conjecture [Er97b]: for all $r, k \geq 2$, +there exist constants $C_1, C_2 > 1$ (depending only on $r$) such that +$C_1^{n^{1/(k-1)}} < R(n; k, r) < C_2^{n^{1/(k-1)}}$ for all sufficiently large $n$. +The status of this generalized conjecture is unclear given the issues with +the $k = 3$ upper bound. +-/ +@[category research open, AMS 5] +theorem erdos_129_general_bounds : + ∀ r : ℕ, 2 ≤ r → ∀ k : ℕ, 2 ≤ k → + ∃ C₁ C₂ : ℝ, 1 < C₁ ∧ 1 < C₂ ∧ + ∀ᶠ n : ℕ in Filter.atTop, + C₁ ^ (n : ℝ) ^ ((1 : ℝ) / ((k : ℝ) - 1)) + < (multicolorRamseyNum n k r : ℝ) + ∧ (multicolorRamseyNum n k r : ℝ) + < C₂ ^ (n : ℝ) ^ ((1 : ℝ) / ((k : ℝ) - 1)) := by + sorry + +end Erdos129 diff --git a/FormalConjectures/ErdosProblems/159.lean b/FormalConjectures/ErdosProblems/159.lean new file mode 100644 index 000000000..d4c0727f8 --- /dev/null +++ b/FormalConjectures/ErdosProblems/159.lean @@ -0,0 +1,76 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 159 + +*References:* +- [erdosproblems.com/159](https://www.erdosproblems.com/159) +- [Er78] Erdős, P., *Problems and results in combinatorial analysis and combinatorial number + theory*, Proceedings of the Ninth Southeastern Conference on Combinatorics, Graph Theory, and + Computing (1978), 29–40. +- [Er81] Erdős, P., *On the combinatorial problems which I would most like to see solved*, + Combinatorica 1 (1981), 25–42. +- [Er84d] Erdős, P., *Extremal problems in number theory, combinatorics and geometry*. + Proceedings of the International Congress of Mathematicians, Vol. 1, 2 (Warsaw, 1983) + (1984), 51–70. +- [EFRS78] Erdős, P., Faudree, R. J., Rousseau, C. C., and Schelp, R. H., + *On cycle-complete graph Ramsey numbers*, J. Graph Theory 2 (1978), 53–64. +- [Sp77] Spencer, J., *Asymptotic lower bounds for Ramsey functions*, Discrete Math. + **20** (1977), 69–76. +-/ + +open Filter SimpleGraph + +namespace Erdos159 + +/-- The graph Ramsey number $R(C_4, K_n)$: the minimum $N$ such that every simple + graph $G$ on $N$ vertices either contains a copy of $C_4$ as a subgraph, or the + complement $G^c$ contains a copy of $K_n$ (i.e., $G$ has an independent set of + size $n$). -/ +noncomputable def ramseyC4Kn (n : ℕ) : ℕ := + sInf {N : ℕ | ∀ (G : SimpleGraph (Fin N)), + (cycleGraph 4).IsContained G ∨ (⊤ : SimpleGraph (Fin n)).IsContained Gᶜ} + +/-- +Erdős Conjecture (Problem 159) [Er78, Er81, Er84d]: + +There exists a constant $c > 0$ such that $R(C_4, K_n) \ll n^{2-c}$, i.e., +$R(C_4, K_n) = O(n^{2-c})$ as $n \to \infty$. + +The Ramsey number $R(C_4, K_n)$ is the minimum $N$ such that every 2-colouring +of the edges of $K_N$ contains a monochromatic $C_4$ in one colour or a +monochromatic $K_n$ in the other colour. + +The current bounds are: +$$n^{3/2} / (\log n)^{3/2} \ll R(C_4, K_n) \ll n^2 / (\log n)^2,$$ +where the upper bound is due to Szemerédi [EFRS78] and the lower bound +to Spencer [Sp77]. Improving the upper bound to $n^{2-c}$ for any fixed +$c > 0$ remains open. +-/ +@[category research open, AMS 5] +theorem erdos_159 : + ∃ c : ℝ, 0 < c ∧ + ∃ C : ℝ, 0 < C ∧ + ∀ᶠ n : ℕ in atTop, + (ramseyC4Kn n : ℝ) ≤ C * (n : ℝ) ^ (2 - c) := by + sorry + +-- TODO: Formalize the known bounds n^{3/2}/(log n)^{3/2} ≪ R(C₄, Kₙ) ≪ n²/(log n)². + +end Erdos159 diff --git a/FormalConjectures/ErdosProblems/165.lean b/FormalConjectures/ErdosProblems/165.lean new file mode 100644 index 000000000..14e7d3c0f --- /dev/null +++ b/FormalConjectures/ErdosProblems/165.lean @@ -0,0 +1,97 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 165 + +Related problems: [544](https://www.erdosproblems.com/544), +[986](https://www.erdosproblems.com/986), [1013](https://www.erdosproblems.com/1013). +OEIS: [A000791](https://oeis.org/A000791). + +*References:* +- [erdosproblems.com/165](https://www.erdosproblems.com/165) +- [AKS80] Ajtai, M., Komlós, J. and Szemerédi, E., _A note on Ramsey numbers_. + J. Combin. Theory Ser. A **29** (1980), 354–360. +- [Sh83] Shearer, J. B., _A note on the independence number of triangle-free + graphs_. Discrete Math. **46** (1983), 83–87. +- [Ki95] Kim, J. H., _The Ramsey number R(3,t) has order of magnitude t²/log t_. + Random Structures and Algorithms (1995), 173–207. +- [PGM20] Fiz Pontiveros, G., Griffiths, S. and Morris, R., _The triangle-free + process and the Ramsey number R(3,k)_. Mem. Amer. Math. Soc. (2020). +- [BoKe21] Bohman, T. and Keevash, P., _Dynamic concentration of the + triangle-free process_. Random Structures Algorithms (2021), 221–293. +- [CJMS25] Campos, M., Jenssen, M., Michelen, M. and Sahasrabudhe, J., + _A new lower bound for the Ramsey numbers R(3,k)_. arXiv:2505.13371 (2025). +- [HHKP25] Hefty, L., Horn, P., King, R. and Pfender, F., _Improving R(3,k) in + just two bites_. arXiv:2510.19718 (2025). +- [Er61] Erdős, P., _Some unsolved problems_. + Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221–254. +- [Er71] Erdős, P., _Some unsolved problems in graph theory and combinatorial analysis_. + Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97–109. +- [Er78] Erdős, P., _Problems and results in combinatorial analysis and combinatorial number + theory_. Proc. Ninth SE Conf. on Combinatorics, Graph Theory, and Computing (1978), 29–40. +- [Er90b] Erdős, P., _Problems and results on graphs and hypergraphs: similarities and + differences_. Mathematics of Ramsey theory (1990), 12–28. +- [Er93] Erdős, P., _Some of my favorite solved and unsolved problems in graph theory_. + Quaestiones Math. (1993), 333–350. +- [Er97c] Erdős, P., _Some of my favorite problems and results_. + The mathematics of Paul Erdős, I (1997), 47–67. +-/ + +open Filter SimpleGraph Real + +open scoped Topology + +namespace Erdos165 + +/-- +Erdős Conjecture (Problem 165) [Er61, Er71, Er90b, Er93, Er97c]: + +There exists a constant $c > 0$ such that $R(3,k) \sim c \cdot k^2 / \log k$, i.e., +$$ + \lim_{k \to \infty} \frac{R(3,k)}{k^2 / \log k} = c. +$$ + +The conjectured value is $c = 1/2$. +-/ +@[category research open, AMS 5] +theorem erdos_165 : answer(sorry) ↔ + ∃ c : ℝ, 0 < c ∧ + Tendsto (fun k : ℕ => + (graphRamseyNumber 3 k : ℝ) / ((k : ℝ) ^ 2 / Real.log (k : ℝ))) + atTop (nhds c) := by + sorry + +/-- +Erdős Problem 165 — conjectured value $c = 1/2$: + +$$ + \lim_{k \to \infty} \frac{R(3,k)}{k^2 / \log k} = \frac{1}{2}. +$$ +-/ +@[category research open, AMS 5] +theorem erdos_165_conjectured_value : + Tendsto (fun k : ℕ => + (graphRamseyNumber 3 k : ℝ) / ((k : ℝ) ^ 2 / Real.log (k : ℝ))) + atTop (nhds (1 / 2)) := by + sorry + +-- TODO: Formalize the known bounds (c+o(1))k²/log k ≤ R(3,k) ≤ (1+o(1))k²/log k +-- with c ≥ 1/2 [HHKP25]. + +end Erdos165 diff --git a/FormalConjectures/ErdosProblems/190.lean b/FormalConjectures/ErdosProblems/190.lean new file mode 100644 index 000000000..367c5db56 --- /dev/null +++ b/FormalConjectures/ErdosProblems/190.lean @@ -0,0 +1,74 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 190 + +*References:* +- [erdosproblems.com/190](https://www.erdosproblems.com/190) +- [ErGr79] Erdős, P. and Graham, R., _Old and new problems and results in combinatorial + number theory: van der Waerden's theorem and related topics_. Enseign. Math. (1979). +- [ErGr80] Erdős, P. and Graham, R., _Old and new problems and results in combinatorial + number theory_. Monographies de L'Enseignement Mathématique (1980). +-/ + +open Filter Real + +namespace Erdos190 + +/-- A colouring $\chi : \mathbb{N} \to \mathbb{N}$ has a monochromatic $k$-term arithmetic +progression within $\{1,\ldots,N\}$: there exist $a \geq 1$ and $d \geq 1$ such that +$a, a+d, \ldots, a+(k-1) \cdot d$ are all in $\{1,\ldots,N\}$ and all share the same colour. -/ +def HasMonoAP (χ : ℕ → ℕ) (N k : ℕ) : Prop := + ∃ a d : ℕ, 0 < d ∧ 1 ≤ a ∧ a + (k - 1) * d ≤ N ∧ + ∀ i : ℕ, i < k → χ (a + i * d) = χ a + +/-- A colouring $\chi : \mathbb{N} \to \mathbb{N}$ has a rainbow $3$-term arithmetic +progression within $\{1,\ldots,N\}$: there exist $a \geq 1$ and $d \geq 1$ such that +$a, a+d, a+2d$ are all in $\{1,\ldots,N\}$ and their colours are pairwise distinct. -/ +def HasRainbowAP (χ : ℕ → ℕ) (N : ℕ) : Prop := + ∃ a d : ℕ, 0 < d ∧ 1 ≤ a ∧ a + 2 * d ≤ N ∧ + χ a ≠ χ (a + d) ∧ χ a ≠ χ (a + 2 * d) ∧ χ (a + d) ≠ χ (a + 2 * d) + +/-- $H(k)$ is the smallest $N$ such that any colouring of $\{1,\ldots,N\}$ contains +either a monochromatic $k$-term AP or a rainbow $3$-term AP. -/ +noncomputable def H (k : ℕ) : ℕ := + sInf {N : ℕ | ∀ χ : ℕ → ℕ, HasMonoAP χ N k ∨ HasRainbowAP χ N} + +/-- +Erdős Problem 190 [ErGr79, ErGr80]: + +Is it true that $H(k)^{1/k}/k \to \infty$ as $k \to \infty$, where $H(k)$ is the smallest $N$ +such that any finite colouring of $\{1,\ldots,N\}$ always contains either a monochromatic +$k$-term arithmetic progression or a rainbow arithmetic progression? +-/ +@[category research open, AMS 5] +theorem erdos_190 : answer(sorry) ↔ + Tendsto (fun k : ℕ => (H k : ℝ) ^ ((1 : ℝ) / (k : ℝ)) / (k : ℝ)) atTop atTop := by + sorry + +/-- +Known weaker result: $H(k)^{1/k} \to \infty$ as $k \to \infty$ (without the additional +division by $k$). This is described as "easy to show" on the website. +-/ +@[category research solved, AMS 5] +theorem erdos_190_weaker : + Tendsto (fun k : ℕ => (H k : ℝ) ^ ((1 : ℝ) / (k : ℝ))) atTop atTop := by + sorry + +end Erdos190 diff --git a/FormalConjectures/ErdosProblems/483.lean b/FormalConjectures/ErdosProblems/483.lean new file mode 100644 index 000000000..082692ccb --- /dev/null +++ b/FormalConjectures/ErdosProblems/483.lean @@ -0,0 +1,74 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 483 + +See also Problem [183](https://www.erdosproblems.com/183). +OEIS: [A030126](https://oeis.org/A030126). + +*References:* +- [erdosproblems.com/483](https://www.erdosproblems.com/483) +- [Er61] Erdős, P., _Some unsolved problems_. Magyar Tud. Akad. Mat. Kutató Int. Közl. 6 (1961), + 221–254. +- [Er65] Erdős, P., _Extremal problems in number theory_. Proc. Sympos. Pure Math. 8 (1965), + 181–189. +- [ACPPRT21] Ageron, R., Casteras, P., Pellerin, T., Portella, Y., Rimmel, A., Tomasik, J., + _New lower bounds for Schur and weak Schur numbers_. arXiv:2112.03175 (2021). +- [Wh73] Whitehead, E. G., Jr., _The Ramsey number N(3,3,3,3;2)_. Discrete Mathematics (1973), + 389–396. +- [He17] Heule, M., _Schur Number Five_. arXiv:1711.08076 (2017). +-/ + +namespace Erdos483 + +/-- A coloring $f : \mathbb{N} \to \text{Fin}\ k$ has a *monochromatic Schur triple* in +$\{1, \ldots, N\}$ if there exist $a, b \geq 1$ with $a + b \leq N$ and +$f(a) = f(b) = f(a + b)$. -/ +def HasMonochromaticSchurTriple (k N : ℕ) (f : ℕ → Fin k) : Prop := + ∃ a b : ℕ, 1 ≤ a ∧ 1 ≤ b ∧ a + b ≤ N ∧ f a = f b ∧ f b = f (a + b) + +/-- +Erdős Problem 483 [Er61, p.233] [Er65, p.188]: + +Let $f(k)$ be the minimal $N$ such that if $\{1, \ldots, N\}$ is $k$-coloured then there is a +monochromatic solution to $a + b = c$. The values $f(k)$ are known as Schur numbers. + +Estimate $f(k)$. In particular, is it true that $f(k) < c^k$ for some constant $c > 0$? + +The best-known bounds for large $k$ are +$$ + 380^{k/5} - O(1) \leq f(k) \leq \lfloor (e - 1/24)\, k! \rfloor - 1. +$$ +The known values are $f(1) = 2$, $f(2) = 5$, $f(3) = 14$, $f(4) = 45$, $f(5) = 161$ +(OEIS A030126). + +We formalize the conjecture: there exists $c > 0$ such that for all $k \geq 1$, +every $k$-coloring of $\{1, \ldots, N\}$ with $N \geq c^k$ has a monochromatic Schur triple. +Equivalently, the Schur number $f(k)$ grows at most exponentially in $k$. +-/ +@[category research open, AMS 5] +theorem erdos_483 : answer(sorry) ↔ + ∃ c : ℝ, 0 < c ∧ + ∀ k : ℕ, 1 ≤ k → + ∀ N : ℕ, c ^ k ≤ (N : ℝ) → + ∀ f : ℕ → Fin k, + HasMonochromaticSchurTriple k N f := by + sorry + +end Erdos483 diff --git a/FormalConjectures/ErdosProblems/531.lean b/FormalConjectures/ErdosProblems/531.lean new file mode 100644 index 000000000..4119c3a8e --- /dev/null +++ b/FormalConjectures/ErdosProblems/531.lean @@ -0,0 +1,78 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 531 + +*References:* +- [erdosproblems.com/531](https://www.erdosproblems.com/531) +- [Er73] Erdős, P., _Problems and results on combinatorial number theory_. In: A Survey of + Combinatorial Theory (1973), 117–138. +- [ErSp89] Erdős, P. and Spencer, J., _Monochromatic sumsets_. Journal of Combinatorial + Theory, Series A **50** (1989), 162–163. +- [BENTW17] Balogh, J., Eberhard, S., Narayanan, B., Treglown, A. and Wagner, A. Z., +_An improved lower bound for Folkman's theorem_. Bulletin of the London Mathematical +Society **49** (2017), 745–747. +-/ + +open Filter Finset + +open scoped BigOperators + +namespace Erdos531 + +/-- A 2-coloring $\chi : \mathbb{N} \to \mathrm{Bool}$ admits a **monochromatic subset-sum +$k$-set** within $\{1, \ldots, N\}$ if there is a $k$-element set +$A \subseteq \{1, \ldots, N\}$ whose non-empty subset sums all lie in +$\{1, \ldots, N\}$ and receive the same color. -/ +def HasMonoSubsetSumSet (χ : ℕ → Bool) (k N : ℕ) : Prop := + ∃ A : Finset ℕ, + A.card = k ∧ + (∀ a ∈ A, 1 ≤ a ∧ a ≤ N) ∧ + (∀ S ∈ A.powerset, S.Nonempty → ∑ i ∈ S, i ≤ N) ∧ + ∃ c : Bool, ∀ S ∈ A.powerset, S.Nonempty → χ (∑ i ∈ S, i) = c + +/-- The **Folkman number** $F(k)$: the minimum $N$ such that every 2-coloring +of $\{1, \ldots, N\}$ admits a $k$-element subset whose non-empty subset sums +are monochromatic. -/ +noncomputable def folkmanNumber (k : ℕ) : ℕ := + sInf {N : ℕ | ∀ χ : ℕ → Bool, HasMonoSubsetSumSet χ k N} + +/-- Folkman's theorem: for every $k$, the Folkman number $F(k)$ is finite. +That is, there exists $N$ such that every 2-coloring of $\{1, \ldots, N\}$ has a +monochromatic subset-sum $k$-set. -/ +@[category research solved, AMS 5] +theorem folkman_theorem (k : ℕ) : + ∃ N : ℕ, ∀ χ : ℕ → Bool, HasMonoSubsetSumSet χ k N := by + sorry + +/-- +**Erdős Problem 531** (lower bound, [BENTW17]): + +$F(k) \geq 2^{2^{k-1}/k}$ for all sufficiently large $k$. + +This is the best known lower bound on the Folkman number, due to +Balogh, Eberhard, Narayanan, Treglown, and Wagner. +-/ +@[category research solved, AMS 5] +theorem erdos_531 : + ∀ᶠ k : ℕ in atTop, + (folkmanNumber k : ℝ) ≥ (2 : ℝ) ^ ((2 : ℝ) ^ ((k : ℝ) - 1) / (k : ℝ)) := by + sorry + +end Erdos531 diff --git a/FormalConjectures/ErdosProblems/77.lean b/FormalConjectures/ErdosProblems/77.lean new file mode 100644 index 000000000..023a22662 --- /dev/null +++ b/FormalConjectures/ErdosProblems/77.lean @@ -0,0 +1,105 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 77 + +See also OEIS sequence [A059442](https://oeis.org/A059442) and related problems +[627](https://www.erdosproblems.com/627), [1029](https://www.erdosproblems.com/1029). + +*References:* +- [erdosproblems.com/77](https://www.erdosproblems.com/77) +- [Er61] Erdős, P., _Some unsolved problems_. + Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221–254. +- [Er69b] Erdős, P., _Problems and results in chromatic graph theory_. + Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., 1968) (1969), 27–35. +- [Er71] Erdős, P., _Some unsolved problems in graph theory and combinatorial analysis_. + Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97–109. +- [Er81] Erdős, P., _On the combinatorial problems which I would most like to see solved_. + Combinatorica **1** (1981), 25–42. +- [Er88] Erdős, P., _Problems and results in combinatorial analysis and graph theory_. + Discrete Math. (1988), 81–92. +- [Er90b] Erdős, P., _Problems and results on graphs and hypergraphs: similarities and + differences_. Mathematics of Ramsey theory (1990), 12–28. +- [Er93] Erdős, P., _Some of my favorite solved and unsolved problems in graph theory_. + Quaestiones Math. (1993), 333–350. +- [Er95] Erdős, P., _Some of my favourite problems in number theory, combinatorics, and + geometry_. Resenhas (1995), 165–186. +- [Er97c] Erdős, P., _Some of my favorite problems and results_. + The mathematics of Paul Erdős, I (1997), 47–67. +- [Er97d] Erdős, P., _Some recent problems and results in graph theory_. + Discrete Math. (1997), 81–85. +- [Va99] Various authors, _Some of Paul's favorite problems_. Booklet produced for the + conference "Paul Erdős and his mathematics", Budapest (1999). +- [CGMS23] Campos, M., Griffiths, S., Morris, R., and Sahasrabudhe, J., + _An exponential improvement for diagonal Ramsey_. arXiv:2303.09521 (2023). +- [GNNW24] Gupta, P., Ndiaye, N., Norin, S., and Wei, L., + _Optimizing the CGMS upper bound on Ramsey numbers_. arXiv:2407.19026 (2024). +- [BBCGHMST24] Balister, P., Bollobás, B., Campos, M., Griffiths, S., Hurley, E., + Morris, R., Sahasrabudhe, J., and Tiba, M., _Upper bounds for multicolour Ramsey numbers_. + arXiv:2410.17197 (2024). +-/ + +open Filter SimpleGraph + +open scoped Topology + +namespace Erdos77 + +/-- +Erdős Problem 77: + +Find the value of $\lim_{k \to \infty} R(k)^{1/k}$, where $R(k)$ is the diagonal +Ramsey number. +-/ +@[category research open, AMS 5] +theorem erdos_77 : + Tendsto (fun k : ℕ => + (diagRamseyNumber k : ℝ) ^ ((1 : ℝ) / (k : ℝ))) + atTop (nhds (answer(sorry) : ℝ)) := by + sorry + +/-- +Erdős Problem 77 — Existence variant: + +The limit $\lim_{k \to \infty} R(k)^{1/k}$ exists. Erdős offered \$100 for a proof. +-/ +@[category research open, AMS 5] +theorem erdos_77.variants.limit_exists : + ∃ L : ℝ, Tendsto (fun k : ℕ => + (diagRamseyNumber k : ℝ) ^ ((1 : ℝ) / (k : ℝ))) + atTop (nhds L) := by + sorry + +/-- +Erdős Problem 77 — Non-existence variant: + +The limit $\lim_{k \to \infty} R(k)^{1/k}$ does not exist, i.e., +$\liminf R(k)^{1/k} < \limsup R(k)^{1/k}$. +Erdős offered \$1,000 (later raised to \$10,000) for a proof. +-/ +@[category research open, AMS 5] +theorem erdos_77.variants.limit_does_not_exist : + ¬ ∃ L : ℝ, Tendsto (fun k : ℕ => + (diagRamseyNumber k : ℝ) ^ ((1 : ℝ) / (k : ℝ))) + atTop (nhds L) := by + sorry + +-- TODO: Formalize the known bounds √2 ≤ liminf R(k)^{1/k} ≤ limsup R(k)^{1/k} ≤ 3.7992... + +end Erdos77 diff --git a/FormalConjectures/ErdosProblems/78.lean b/FormalConjectures/ErdosProblems/78.lean new file mode 100644 index 000000000..376441b5d --- /dev/null +++ b/FormalConjectures/ErdosProblems/78.lean @@ -0,0 +1,110 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 78 + +See also OEIS sequence [A059442](https://oeis.org/A059442) and related problems +[77](https://www.erdosproblems.com/77), [1029](https://www.erdosproblems.com/1029). + +*References:* +- [erdosproblems.com/78](https://www.erdosproblems.com/78) +- [Er69b] Erdős, P., _Problems and results in chromatic graph theory_. + Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., 1968) (1969), 27–35. +- [Er71] Erdős, P., _Some unsolved problems in graph theory and combinatorial analysis_. + Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97–109. +- [Er88] Erdős, P., _Problems and results in combinatorial analysis and graph theory_. + Discrete Math. (1988), 81–92. +- [Er93] Erdős, P., _Some of my favorite solved and unsolved problems in graph theory_. + Quaestiones Math. (1993), 333–350. +- [Er95] Erdős, P., _Some of my favourite problems in number theory, combinatorics, and + geometry_. Resenhas (1995), 165–186. +- [Er97c] Erdős, P., _Some of my favorite problems and results_. + The mathematics of Paul Erdős, I (1997), 47–67. +- [Va99] Various authors, _Some of Paul's favorite problems_. Booklet produced for the + conference "Paul Erdős and his mathematics", Budapest (1999). +- [Co15] Cohen, G., _Two-source dispersers for polylogarithmic entropy and improved Ramsey + graphs_. Electronic Colloquium on Computational Complexity (2015). +- [Li23b] Li, X., _Two source extractors for asymptotically optimal entropy, and (many) more_. + arXiv:2303.06802 (2023). +-/ + +open SimpleGraph + +namespace Erdos78 + +/-- +Erdős Problem 78 (Open, \$100 prize): + +Let $R(k)$ be the Ramsey number for $K_k$, the minimal $n$ such that every +2-colouring of the edges of $K_n$ contains a monochromatic copy of $K_k$. +Give a constructive proof that $R(k) > C^k$ for some constant $C > 1$. + +Erdős gave a simple probabilistic (non-constructive) proof that +$R(k) \gg k \cdot 2^{k/2}$. This problem asks for an explicit/constructive +lower bound that is still exponential in $k$. + +Equivalently, this asks for an explicit construction of a graph on $n$ +vertices which does not contain any clique or independent set of size +$\geq c \cdot \log(n)$ for some constant $c > 0$. + +We formalize the core mathematical content: there exists $C > 1$ such that +for all $k \geq 2$, there exists a graph on at least $C^k$ vertices with no +clique or independent set of size $k$ (an independent set of size $k$ in $G$ +is equivalent to a clique of size $k$ in the complement $G^c$, by +`SimpleGraph.isClique_compl`). The "constructive" requirement pertains +to the nature of the proof, not the formal statement itself. +-/ +@[category research open, AMS 5] +theorem erdos_78 : + ∃ C : ℝ, C > 1 ∧ ∀ k : ℕ, k ≥ 2 → + ∃ n : ℕ, (C ^ k : ℝ) ≤ ↑n ∧ + ∃ G : SimpleGraph (Fin n), + G.CliqueFree k ∧ Gᶜ.CliqueFree k := by + sorry + +/-- +Erdős Problem 78 — $o(\sqrt{n})$ variant [Er69b]: + +Erdős also asked for an explicit construction of a graph on $n$ vertices +with no clique or independent set of size $o(\sqrt{n})$. This is weaker +than the full exponential lower bound. The website notes this is now known. +-/ +@[category research solved, AMS 5] +theorem erdos_78_variant_sqrt : + ∃ (f : ℕ → ℕ), (∀ n, f n < n) ∧ + Filter.Tendsto (fun n => (f n : ℝ) / n ^ (1/2 : ℝ)) Filter.atTop (nhds 0) ∧ + ∀ n, ∃ G : SimpleGraph (Fin n), G.CliqueFree (f n) ∧ Gᶜ.CliqueFree (f n) := by + sorry + +/-- +Erdős Problem 78 — logarithmic formulation: + +Equivalently, there exists a constant $c > 0$ such that for all $n \geq 2$, +there is a graph on $n$ vertices with no clique or independent set of size +$\geq c \cdot \log(n)$. This is logically equivalent to `erdos_78` but +phrased in the "construct a graph on $n$ vertices" framing. +-/ +@[category research open, AMS 5] +theorem erdos_78_log : + ∃ c : ℝ, c > 0 ∧ ∀ n : ℕ, n ≥ 2 → + ∃ G : SimpleGraph (Fin n), + G.CliqueFree ⌈c * Real.log n⌉₊ ∧ Gᶜ.CliqueFree ⌈c * Real.log n⌉₊ := by + sorry + +end Erdos78 diff --git a/FormalConjectures/ErdosProblems/812.lean b/FormalConjectures/ErdosProblems/812.lean index e2eb52285..5c913ce1b 100644 --- a/FormalConjectures/ErdosProblems/812.lean +++ b/FormalConjectures/ErdosProblems/812.lean @@ -25,20 +25,18 @@ import FormalConjectures.Util.ProblemImports between consecutive {R}amsey numbers. Utilitas Math. (1989), 115--118. -/ -open Combinatorics Filter +open SimpleGraph Filter open scoped Topology namespace Erdos812 -/-- $R(n)$ denotes the diagonal Ramsey number $R(n,n)$, i.e., `hypergraphRamsey 2 n`. -/ -local notation "R" => hypergraphRamsey 2 - /-- Is it true that $\frac{R(n+1)}{R(n)}\geq 1+c$ for some constant $c>0$, for all large $n$? -/ @[category research open, AMS 5] theorem erdos_812.parts.i : - answer(sorry) ↔ ∃ c > 0, ∀ᶠ n in atTop, (R (n + 1) : ℝ) / (R n : ℝ) ≥ 1 + c:= by + answer(sorry) ↔ ∃ c > 0, ∀ᶠ n in atTop, + (graphRamseyNumber (n + 1) (n + 1) : ℝ) / (graphRamseyNumber n n : ℝ) ≥ 1 + c := by sorry /-- @@ -47,7 +45,8 @@ Is it true that $R(n+1)-R(n) \gg n^2$? @[category research open, AMS 5] theorem erdos_812.parts.ii : answer(sorry) ↔ - (fun n : ℕ ↦ (R (n + 1) : ℝ) - (R n : ℝ)) ≫ (fun n : ℕ ↦ (n : ℝ) ^ 2) := by + (fun n : ℕ ↦ (graphRamseyNumber (n + 1) (n + 1) : ℝ) - (graphRamseyNumber n n : ℝ)) ≫ + (fun n : ℕ ↦ (n : ℝ) ^ 2) := by sorry /-- @@ -55,7 +54,9 @@ Burr, Erdős, Faudree, and Schelp [BEFS89] proved that $R(n+1)-R(n) \geq 4n-8$ f -/ @[category research solved, AMS 5] theorem erdos_812.variants.lower_bound : - ∀ n : ℕ, n ≥ 2 → (R (n + 1) : ℤ) - (R n : ℤ) ≥ 4 * (n : ℤ) - 8 := by + ∀ n : ℕ, n ≥ 2 → + (graphRamseyNumber (n + 1) (n + 1) : ℤ) - (graphRamseyNumber n n : ℤ) ≥ + 4 * (n : ℤ) - 8 := by sorry -- TODO: Add Erdos Problem 165 implication when Erdos Problem 165 is formalized. diff --git a/FormalConjectures/ErdosProblems/87.lean b/FormalConjectures/ErdosProblems/87.lean new file mode 100644 index 000000000..6defeb80b --- /dev/null +++ b/FormalConjectures/ErdosProblems/87.lean @@ -0,0 +1,66 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 87 + +*References:* +- [erdosproblems.com/87](https://www.erdosproblems.com/87) +- [Er95] Erdős, P., _Some of my favourite problems in number theory, combinatorics, and + geometry_. Resenhas (1995), 165–186. +- [FaMc93] Faudree, R. J. and McKay, B., _A conjecture of Erdős and the Ramsey number r(W)_, + J. Combin. Math. Combin. Comput. **13** (1993), 23–31. +-/ + +open SimpleGraph + +namespace Erdos87 + +/-- +**Erdős Problem 87** — Weak form (open). [Er95, p. 14] + +Let $\varepsilon > 0$. Is it true that, if $k$ is sufficiently large, then +$$R(G) > (1 - \varepsilon)^k \cdot R(k)$$ +for every graph $G$ with chromatic number $\chi(G) = k$? +-/ +@[category research open, AMS 5] +theorem erdos_87 : answer(sorry) ↔ + ∀ ε : ℝ, 0 < ε → ε < 1 → + ∃ K : ℕ, ∀ k : ℕ, K ≤ k → + ∀ {V : Type*} [Fintype V] (G : SimpleGraph V), + G.chromaticNumber = k → + (diagRamseyNumber k : ℝ) * (1 - ε) ^ k < (ramseyNumber G : ℝ) := by + sorry + +/-- +**Erdős Problem 87** — Strong form (open). [Er95, p. 14] + +Is there some $c > 0$ such that, for all large $k$, +$$R(G) > c \cdot R(k)$$ +for every graph $G$ with chromatic number $\chi(G) = k$? +-/ +@[category research open, AMS 5] +theorem erdos_87.variants.strong : answer(sorry) ↔ + ∃ c : ℝ, 0 < c ∧ + ∃ K : ℕ, ∀ k : ℕ, K ≤ k → + ∀ {V : Type*} [Fintype V] (G : SimpleGraph V), + G.chromaticNumber = k → + c * (diagRamseyNumber k : ℝ) < (ramseyNumber G : ℝ) := by + sorry + +end Erdos87 diff --git a/FormalConjectures/ErdosProblems/948.lean b/FormalConjectures/ErdosProblems/948.lean new file mode 100644 index 000000000..cdc3e2128 --- /dev/null +++ b/FormalConjectures/ErdosProblems/948.lean @@ -0,0 +1,48 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 948 + +See also Problem [532](https://www.erdosproblems.com/532) (Hindman's theorem). + +*References:* +- [erdosproblems.com/948](https://www.erdosproblems.com/948) +- [Er77c] Erdős, P., _Problems and results on combinatorial number theory. III._. Number Theory + Day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43–72. +-/ + +open Finset BigOperators + +namespace Erdos948 + +/-- Is there a function $f : \mathbb{N} \to \mathbb{N}$ and $k \in \mathbb{N}$ such that for any +$k$-colouring $\chi$ of the natural numbers, there is a strictly increasing sequence $a$ with +$a(n) < f(n)$ for infinitely many $n$, and the finite subset sums of the sequence do not achieve +all $k$ colours? -/ +@[category research open, AMS 5] +theorem erdos_948 : answer(sorry) ↔ + ∃ (f : ℕ → ℕ) (k : ℕ), 0 < k ∧ + ∀ (χ : ℕ → Fin k), + ∃ (a : ℕ → ℕ), StrictMono a ∧ + Set.Infinite {n : ℕ | a n < f n} ∧ + ∃ (c : Fin k), ∀ (S : Finset ℕ), S.Nonempty → + χ (∑ i ∈ S, a i) ≠ c := by + sorry + +end Erdos948 diff --git a/FormalConjectures/ErdosProblems/986.lean b/FormalConjectures/ErdosProblems/986.lean new file mode 100644 index 000000000..a2cd74c99 --- /dev/null +++ b/FormalConjectures/ErdosProblems/986.lean @@ -0,0 +1,126 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 986 + +See also Problem [165](https://www.erdosproblems.com/165) (k=3 case), +Problem [166](https://www.erdosproblems.com/166) (k=4 case), +Problem [920](https://www.erdosproblems.com/920) (chromatic number connection). + +OEIS sequences: [A000791](https://oeis.org/A000791), [A059442](https://oeis.org/A059442). + +*References:* +- [erdosproblems.com/986](https://www.erdosproblems.com/986) +- [Sp77] Spencer, J., _Asymptotic lower bounds for Ramsey functions_. Discrete Math. 20 (1977), + 69–76. +- [MaVe23] Mattheus, S. and Verstraëte, J., _The asymptotics of $r(4,t)$_. Ann. of Math. 199 + (2024), 919–941. +- [BoKe10] Bohman, T. and Keevash, P., _The early evolution of the $H$-free process_. Invent. + Math. 181 (2010), 291–336. +- [AKS80] Ajtai, M., Komlós, J. and Szemerédi, E., _A note on Ramsey numbers_. J. Combin. + Theory Ser. A 29 (1980), 354–360. +- [LRZ01] Li, Y., Rousseau, C. C. and Zang, W., _Asymptotic upper bounds for Ramsey functions_. + Graphs Combin. 17 (2001), 123–128. +- [Er90b] Erdős, P., _Problems and results on graphs and hypergraphs: similarities and + differences_. Mathematics of Ramsey theory (1990), 12–28. +-/ + +open Filter SimpleGraph Real + +namespace Erdos986 + +/-- +Erdős Conjecture (Problem #986) [Er90b]: + +For any fixed $k \geq 3$, there exist constants $C > 0$ and $c \in \mathbb{N}$ with $c > 0$ +such that for all sufficiently large $n$: +$$ +R(k,n) \geq C \cdot n^{k-1} / (\log n)^c. +$$ +In asymptotic notation: $R(k,n) \gg n^{k-1}/(\log n)^c$ for some $c > 0$. +-/ +@[category research open, AMS 5] +theorem erdos_986 (k : ℕ) (hk : 3 ≤ k) : + ∃ C : ℝ, 0 < C ∧ + ∃ c : ℕ, 0 < c ∧ + ∀ᶠ n : ℕ in atTop, + C * ((n : ℝ) ^ (k - 1) / (Real.log (n : ℝ)) ^ c) ≤ (graphRamseyNumber k n : ℝ) := by + sorry + +/-- +Spencer's theorem (1977) [Sp77]: the $k = 3$ case of Erdős Problem 986. + +There exist constants $C > 0$ and $c \in \mathbb{N}$ with $c > 0$ such that for all +sufficiently large $n$, $R(3,n) \geq C \cdot n^2 / (\log n)^c$. + +See also Problem 165. +-/ +@[category research solved, AMS 5] +theorem erdos_986_k_eq_3 : + ∃ C : ℝ, 0 < C ∧ + ∃ c : ℕ, 0 < c ∧ + ∀ᶠ n : ℕ in atTop, + C * ((n : ℝ) ^ 2 / (Real.log (n : ℝ)) ^ c) ≤ (graphRamseyNumber 3 n : ℝ) := by + sorry + +/-- +Mattheus–Verstraëte theorem (2023) [MaVe23]: the $k = 4$ case of Erdős Problem 986. + +There exist constants $C > 0$ and $c \in \mathbb{N}$ with $c > 0$ such that for all +sufficiently large $n$, $R(4,n) \geq C \cdot n^3 / (\log n)^c$. + +See also Problem 166. +-/ +@[category research solved, AMS 5] +theorem erdos_986_k_eq_4 : + ∃ C : ℝ, 0 < C ∧ + ∃ c : ℕ, 0 < c ∧ + ∀ᶠ n : ℕ in atTop, + C * ((n : ℝ) ^ 3 / (Real.log (n : ℝ)) ^ c) ≤ (graphRamseyNumber 4 n : ℝ) := by + sorry + +/-- +Ajtai–Komlós–Szemerédi upper bound (1980) [AKS80]: + +For any fixed $k \geq 3$, there exists a constant $C > 0$ such that for all sufficiently +large $n$, $R(k,n) \leq C \cdot n^{k-1} / (\log n)^{k-2}$. +-/ +@[category research solved, AMS 5] +theorem erdos_986_upper (k : ℕ) (hk : 3 ≤ k) : + ∃ C : ℝ, 0 < C ∧ + ∀ᶠ n : ℕ in atTop, + (graphRamseyNumber k n : ℝ) ≤ C * ((n : ℝ) ^ (k - 1) / (Real.log (n : ℝ)) ^ (k - 2)) := by + sorry + +/-- +Bohman–Keevash lower bound (2010) [BoKe10]: + +For any fixed $k \geq 3$, there exists a constant $C > 0$ such that for all sufficiently +large $n$, $R(k,n) \geq C \cdot n^{(k+1)/2} / (\log n)^{(k+1)/2 - 1/(k-2)}$. +-/ +@[category research solved, AMS 5] +theorem erdos_986_lower (k : ℕ) (hk : 3 ≤ k) : + ∃ C : ℝ, 0 < C ∧ + ∀ᶠ n : ℕ in atTop, + C * (((n : ℝ) ^ (((k : ℝ) + 1) / 2)) / + ((Real.log (n : ℝ)) ^ (((k : ℝ) + 1) / 2 - 1 / ((k : ℝ) - 2)))) ≤ + (graphRamseyNumber k n : ℝ) := by + sorry + +end Erdos986 diff --git a/FormalConjectures/Wikipedia/RamseyNumbers.lean b/FormalConjectures/Wikipedia/RamseyNumbers.lean index efd3b29d2..e5a84ab01 100644 --- a/FormalConjectures/Wikipedia/RamseyNumbers.lean +++ b/FormalConjectures/Wikipedia/RamseyNumbers.lean @@ -40,48 +40,12 @@ $2$-subsets, as `Combinatorics.hypergraphRamsey 2 n` (see `FormalConjecturesForM - [MathWorld: Ramsey Number](https://mathworld.wolfram.com/RamseyNumber.html) -/ -namespace RamseyNumbers +open SimpleGraph -/-- -`IsGraphRamsey n k l` means that for every simple graph `G` on `n` vertices, either -- `G` contains a clique of size `k`, or -- the complement graph `Gᶜ` contains a clique of size `l` (equivalently, `G` contains an - independent set of size `l`). --/ -def IsGraphRamsey (n k l : ℕ) : Prop := - ∀ G : SimpleGraph (Fin n), ¬ (G.CliqueFree k ∧ (Gᶜ).CliqueFree l) - -/-- Monotonicity in the number of vertices. -/ -@[category API, AMS 5] -theorem IsGraphRamsey.succ (n k l : ℕ) : - IsGraphRamsey n k l → IsGraphRamsey (n + 1) k l := by - intro h G - -- Restrict to the induced subgraph on the first `n` vertices. - let H : SimpleGraph (Fin n) := G.comap (Fin.castSuccEmb : Fin n ↪ Fin (n + 1)) - have emb : H ↪g G := SimpleGraph.Embedding.comap (Fin.castSuccEmb : Fin n ↪ Fin (n + 1)) G - have embc : (Hᶜ) ↪g (Gᶜ) := (SimpleGraph.Embedding.complEquiv (G := H) (H := G)).toFun emb - rintro ⟨hG, hGc⟩ - have hH : H.CliqueFree k := SimpleGraph.CliqueFree.comap (f := emb) (n := k) hG - have hHc : (Hᶜ).CliqueFree l := SimpleGraph.CliqueFree.comap (f := embc) (n := l) hGc - exact (h H) ⟨hH, hHc⟩ - -/-- Symmetry in the clique / independent set sizes. -/ -@[category API, AMS 5] -theorem IsGraphRamsey.symm (n k l : ℕ) : - IsGraphRamsey n k l ↔ IsGraphRamsey n l k := by - constructor <;> intro h G - · simpa [IsGraphRamsey, and_comm, and_left_comm, and_assoc] using h (Gᶜ) - · simpa [IsGraphRamsey, and_comm, and_left_comm, and_assoc] using h (Gᶜ) - -/-- -The (graph) Ramsey number `R(k,l)` is the least natural number `n` such that `IsGraphRamsey n k l` -holds. --/ -noncomputable def graphRamseyNumber (k l : ℕ) : ℕ := - sInf {n : ℕ | IsGraphRamsey n k l} +namespace RamseyNumbers -- Notation used in the literature. -notation "R(" k ", " l ")" => graphRamseyNumber k l +notation "R(" k ", " l ")" => SimpleGraph.graphRamseyNumber k l /-- The open problem: determine the Ramsey number $R(5,5)$. @@ -111,4 +75,20 @@ theorem ramsey_number_five_five_upper_bound : IsGraphRamsey 46 5 5 := by sorry +/-- +Is $R(5,5) \geq 44$? The current best lower bound is $43$; improving it to $44$ +is an open problem. +-/ +@[category research open, AMS 5] +theorem ramsey_number_five_five_strict_lower : answer(sorry) ↔ 43 < R(5, 5) := by + sorry + +/-- +Is $R(5,5) \leq 45$? The current best upper bound is $46$; improving it to $45$ +is an open problem. +-/ +@[category research open, AMS 5] +theorem ramsey_number_five_five_strict_upper : answer(sorry) ↔ R(5, 5) < 46 := by + sorry + end RamseyNumbers diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean index 7d336b836..69a8a80e8 100644 --- a/FormalConjecturesForMathlib.lean +++ b/FormalConjecturesForMathlib.lean @@ -40,6 +40,7 @@ public import FormalConjecturesForMathlib.Combinatorics.Additive.Convolution public import FormalConjecturesForMathlib.Combinatorics.Additive.RestrictedSumset public import FormalConjecturesForMathlib.Combinatorics.Additive.VCDim public import FormalConjecturesForMathlib.Combinatorics.Basic +public import FormalConjecturesForMathlib.Combinatorics.Digraph.Ramsey public import FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform public import FormalConjecturesForMathlib.Combinatorics.LatinSquare public import FormalConjecturesForMathlib.Combinatorics.Ramsey @@ -59,6 +60,7 @@ public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConject public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.WellTotallyDominated public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HomDensity public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Johnson +public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Ramsey public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey public import FormalConjecturesForMathlib.Combinatorics.YoungDiagram public import FormalConjecturesForMathlib.Computability.Encoding diff --git a/FormalConjecturesForMathlib/Combinatorics/Digraph/Ramsey.lean b/FormalConjecturesForMathlib/Combinatorics/Digraph/Ramsey.lean new file mode 100644 index 000000000..4dba80452 --- /dev/null +++ b/FormalConjecturesForMathlib/Combinatorics/Digraph/Ramsey.lean @@ -0,0 +1,91 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ +module + +public import Mathlib.Combinatorics.Digraph.Basic +public import Mathlib.Data.Nat.Lattice + +@[expose] public section + +/-! +# Directed Ramsey Numbers + +This file defines the directed Ramsey number `k(n, m)` and related concepts on +`Digraph`s: independent sets, transitive tournaments and directed paths. The Ramsey +numbers here quantify over **oriented graphs**, i.e. digraphs that are loopless and +antisymmetric. +-/ + +namespace Digraph + +variable {V : Type*} + +/-- An *oriented graph* is a digraph that is loopless and antisymmetric (every pair of +distinct vertices has at most one directed edge between them). -/ +def IsOriented (G : Digraph V) : Prop := + (∀ v, ¬ G.Adj v v) ∧ (∀ u v, G.Adj u v → ¬ G.Adj v u) + +/-- An independent set in a digraph: a set $S$ of vertices with no directed edges +between any two of its members (in either direction). -/ +def IsIndepSet (G : Digraph V) (S : Finset V) : Prop := + ∀ u ∈ S, ∀ v ∈ S, ¬ G.Adj u v + +/-- A transitive tournament on vertex set $S$ in digraph $G$: there is a bijection +$f : \mathrm{Fin}(|S|) \to S$ such that $G.\mathrm{Adj}(f(i), f(j))$ holds if and only +if $i < j$. This encodes a total ordering of $S$ compatible with the edge relation. -/ +def IsTransTournament (G : Digraph V) (S : Finset V) : Prop := + ∃ f : Fin S.card → {x : V // x ∈ S}, Function.Bijective f ∧ + ∀ i j : Fin S.card, G.Adj (f i : V) (f j : V) ↔ i < j + +/-- A directed path on vertex set $S$ in digraph $G$: there is a bijection +$f : \mathrm{Fin}(|S|) \to S$ such that $G.\mathrm{Adj}(f(i), f(i+1))$ holds for +all consecutive indices. Only consecutive vertices need be connected. -/ +def IsDirectedPath (G : Digraph V) (S : Finset V) : Prop := + ∃ f : Fin S.card → {x : V // x ∈ S}, Function.Bijective f ∧ + ∀ i : Fin S.card, ∀ h : (i : ℕ) + 1 < S.card, + G.Adj (f i : V) (f ⟨i + 1, h⟩ : V) + +/-- +`IsDirRamsey k n m` means: every oriented graph on `k` vertices contains either an +independent set of size `n` or a transitive tournament of size `m`. +-/ +def IsDirRamsey (k n m : ℕ) : Prop := + ∀ G : Digraph (Fin k), G.IsOriented → + (∃ S : Finset (Fin k), S.card = n ∧ G.IsIndepSet S) ∨ + (∃ S : Finset (Fin k), S.card = m ∧ G.IsTransTournament S) + +/-- +The directed Ramsey number `k(n, m)`: the least `k` such that `IsDirRamsey k n m` holds. +-/ +noncomputable def dirRamseyNumber (n m : ℕ) : ℕ := + sInf {k : ℕ | IsDirRamsey k n m} + +/-- +`IsDirPathRamsey k n m` means: every oriented graph on `k` vertices contains either an +independent set of size `n` or a directed path of size `m`. +-/ +def IsDirPathRamsey (k n m : ℕ) : Prop := + ∀ G : Digraph (Fin k), G.IsOriented → + (∃ S : Finset (Fin k), S.card = n ∧ G.IsIndepSet S) ∨ + (∃ S : Finset (Fin k), S.card = m ∧ G.IsDirectedPath S) + +/-- +The directed-path Ramsey number: the least `k` such that `IsDirPathRamsey k n m` holds. +-/ +noncomputable def dirPathRamseyNumber (n m : ℕ) : ℕ := + sInf {k : ℕ | IsDirPathRamsey k n m} + +end Digraph diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Ramsey.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Ramsey.lean new file mode 100644 index 000000000..15f8b5f45 --- /dev/null +++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Ramsey.lean @@ -0,0 +1,96 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Clique +public import Mathlib.Combinatorics.SimpleGraph.Copy +public import Mathlib.Data.Nat.Lattice + +@[expose] public section + +/-! +# Graph Ramsey Numbers + +This file defines the classical 2-color graph Ramsey number `R(k, l)`, the diagonal graph +Ramsey number `R(H)` for a given graph `H`, and the diagonal Ramsey number `R(k)`. +-/ + +namespace SimpleGraph + +/-- +`IsGraphRamsey n k l` means that for every simple graph `G` on `n` vertices, either +- `G` contains a clique of size `k`, or +- the complement graph `Gᶜ` contains a clique of size `l` (equivalently, `G` contains an + independent set of size `l`). +-/ +def IsGraphRamsey (n k l : ℕ) : Prop := + ∀ G : SimpleGraph (Fin n), ¬ (G.CliqueFree k ∧ (Gᶜ).CliqueFree l) + +/-- Monotonicity in the number of vertices. -/ +theorem IsGraphRamsey.succ (n k l : ℕ) : + IsGraphRamsey n k l → IsGraphRamsey (n + 1) k l := by + intro h G + -- Restrict to the induced subgraph on the first `n` vertices. + let H : SimpleGraph (Fin n) := G.comap (Fin.castSuccEmb : Fin n ↪ Fin (n + 1)) + have emb : H ↪g G := SimpleGraph.Embedding.comap (Fin.castSuccEmb : Fin n ↪ Fin (n + 1)) G + have embc : (Hᶜ) ↪g (Gᶜ) := (SimpleGraph.Embedding.complEquiv (G := H) (H := G)).toFun emb + rintro ⟨hG, hGc⟩ + have hH : H.CliqueFree k := SimpleGraph.CliqueFree.comap (f := emb) (n := k) hG + have hHc : (Hᶜ).CliqueFree l := SimpleGraph.CliqueFree.comap (f := embc) (n := l) hGc + exact (h H) ⟨hH, hHc⟩ + +/-- Symmetry in the clique / independent set sizes. -/ +theorem IsGraphRamsey.symm (n k l : ℕ) : + IsGraphRamsey n k l ↔ IsGraphRamsey n l k := by + constructor <;> intro h G + · simpa [IsGraphRamsey, and_comm, and_left_comm, and_assoc] using h (Gᶜ) + · simpa [IsGraphRamsey, and_comm, and_left_comm, and_assoc] using h (Gᶜ) + +/-- +The (graph) Ramsey number `R(k, l)` is the least natural number `n` such that +`IsGraphRamsey n k l` holds. +-/ +noncomputable def graphRamseyNumber (k l : ℕ) : ℕ := + sInf {n : ℕ | IsGraphRamsey n k l} + +/-- The diagonal graph Ramsey number `R(H)`: the minimum `N` such that every simple +graph `G` on `N` vertices either contains a copy of `H` as a subgraph or its +complement contains a copy of `H`. -/ +noncomputable def ramseyNumber {U : Type*} (H : SimpleGraph U) : ℕ := + sInf {N : ℕ | ∀ (G : SimpleGraph (Fin N)), + H.IsContained G ∨ H.IsContained Gᶜ} + +/-- The classical diagonal Ramsey number `R(k) := R(K_k, K_k)`. -/ +noncomputable def diagRamseyNumber (k : ℕ) : ℕ := + ramseyNumber (⊤ : SimpleGraph (Fin k)) + +/-- The two Ramsey number definitions agree on the diagonal: +`graphRamseyNumber k k = diagRamseyNumber k`. -/ +theorem graphRamseyNumber_self_eq_diagRamseyNumber (k : ℕ) : + graphRamseyNumber k k = diagRamseyNumber k := by + sorry + +/-- `IsGraphRamsey n 2 l` holds iff `l ≤ n`: any graph on `n ≥ l` vertices +either has an edge (2-clique) or is edgeless (complement contains `l`-clique). -/ +theorem isGraphRamsey_two_iff {n l : ℕ} : + IsGraphRamsey n 2 l ↔ l ≤ n := by + sorry + +/-- `R(2, l) = l` for all `l`. -/ +theorem graphRamseyNumber_two (l : ℕ) : graphRamseyNumber 2 l = l := by + sorry + +end SimpleGraph