feat(ErdosProblems): 15x ramsey theory formalizations

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., _Topics in combinatorial analysis_, Proc. Second Louisiana Conference on
+  Combinatorics (1971), 95–99.
+-/
+
+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

FormalConjectures/ErdosProblems/1029.lean

@@ -0,0 +1,52 @@
+/-
+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., *On some of my favourite theorems* (1993).
+-/
+
+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

FormalConjectures/ErdosProblems/1030.lean

@@ -0,0 +1,73 @@
+/-
+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., _On some of my favourite theorems_. Combinatorics, Paul Erdős is eighty,
+  Vol. 2 (Keszthely, 1993), 97–132, p. 339.
+- [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
+
+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.
+$$
+
+Formulated as: there exists $c > 0$ such that eventually (for all sufficiently large $k$),
+$R(k+1, k) / R(k, k) \geq 1 + c$.
+-/
+@[category research open, AMS 5]
+theorem erdos_1030 :
+    ∃ 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
+
+-- TODO: Formalize the Burr–Erdős–Faudree–Schelp bound R(k+1,k) - R(k,k) ≥ 2k - 5 [BEFS89].
+
+end Erdos1030

FormalConjectures/ErdosProblems/112.lean

@@ -0,0 +1,163 @@
+/-
+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.
+-/
+
+namespace Erdos112
+
+/-- An oriented graph on vertex type $V$: an irreflexive, antisymmetric binary relation
+representing directed edges ($\mathrm{adj}(u, v)$ means there is a directed edge from $u$ to $v$).
+Each pair of distinct vertices has at most one directed edge between them. -/
+structure Digraph (V : Type*) where
+  adj : V → V → Prop
+  loopless : ∀ v, ¬ adj v v
+  antisymm : ∀ u v, adj u v → ¬ adj v u
+
+/-- An independent set in a directed graph: a set $S$ of vertices with no directed
+edges between any two of its members (in either direction). -/
+def Digraph.IsIndepSet {V : Type*} (G : Digraph V) (S : Finset V) : Prop :=
+  ∀ u ∈ S, ∀ v ∈ S, ¬ G.adj u v
+
+/-- A transitive tournament on vertex set $S$ in directed graph $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 Digraph.IsTransTournament {V : Type*} (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
+
+/-- The directed Ramsey number $k(n,m)$: the minimal $k$ such that every directed graph
+on $k$ vertices contains either an independent set of size $n$ or a transitive
+tournament of size $m$. -/
+noncomputable def dirRamseyNum (n m : ℕ) : ℕ :=
+  sInf {k : ℕ | ∀ (V : Type) [Fintype V], Fintype.card V = k →
+    ∀ G : Digraph V,
+      (∃ S : Finset V, S.card = n ∧ G.IsIndepSet S) ∨
+      (∃ S : Finset V, S.card = m ∧ G.IsTransTournament S)}
+
+/--
+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 →
+      dirRamseyNum 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 :
+    dirRamseyNum 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 :
+    dirRamseyNum 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 →
+      dirRamseyNum 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 →
+      dirRamseyNum n 3 ≤ n ^ 2 := by
+  sorry
+
+/-- The classical 2-color graph Ramsey number $R(n, m)$: the minimal $k$ such that every
+symmetric 2-coloring of the edges of $K_k$ contains either a red clique of size $n$ or a
+blue clique of size $m$. -/
+noncomputable def graphRamseyNum (n m : ℕ) : ℕ :=
+  sInf {k : ℕ | ∀ (c : Fin k → Fin k → Bool), (∀ x y, c x y = c y x) →
+    (∃ S : Finset (Fin k), S.card = n ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → c u v = true) ∨
+    (∃ S : Finset (Fin k), S.card = m ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → c u v = false)}
+
+/-- 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 →
+      graphRamseyNum n m ≤ dirRamseyNum n m ∧
+      dirRamseyNum n m ≤ graphRamseyNum3 n m m := by
+  sorry
+
+/-- A directed path on vertex set $S$ in directed graph $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. Unlike a transitive tournament, only consecutive vertices need to
+be connected. -/
+def Digraph.IsDirectedPath {V : Type*} (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)
+
+/-- The directed path Ramsey number: the minimal $k$ such that every directed graph on $k$
+vertices contains either an independent set of size $n$ or a directed path of size $m$. -/
+noncomputable def dirPathRamseyNum (n m : ℕ) : ℕ :=
+  sInf {k : ℕ | ∀ (V : Type) [Fintype V], Fintype.card V = k →
+    ∀ G : Digraph V,
+      (∃ S : Finset V, S.card = n ∧ G.IsIndepSet S) ∨
+      (∃ S : Finset V, S.card = m ∧ G.IsDirectedPath S)}
+
+/--
+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 →
+      dirPathRamseyNum 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