google-deepmind · ryantuck · Mar 17, 2026 · Mar 19, 2026 · Mar 19, 2026 · Mar 19, 2026
diff --git a/FormalConjectures/ErdosProblems/1014.lean b/FormalConjectures/ErdosProblems/1014.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 1014
+
+Erdős conjectured that for fixed $k \geq 3$, the ratio of consecutive Ramsey numbers
+$R(k, l+1) / R(k, l)$ tends to $1$ as $l \to \infty$.
+
-Erdős conjectured that for fixed $k \geq 3$, the ratio of consecutive Ramsey numbers
-$R(k, l+1) / R(k, l)$ tends to $1$ as $l \to \infty$.
-Erdős conjectured that for fixed $k \geq 3$, the ratio of consecutive Ramsey numbers
-$R(k, l+1) / R(k, l)$ tends to $1$ as $l \to \infty$.
+See also problems [544] and [1030].
+
+*Reference:* [erdosproblems.com/1014](https://www.erdosproblems.com/1014)
+
+[Er71] Erdős, P., _Topics in combinatorial analysis_, pp. 95-99, 1971.
+-/
+
+open SimpleGraph
+
+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.
+
+Formulated as: for every $\varepsilon > 0$, there exists $L_0$ such that for all $l \geq L_0$,
+$|R(k, l+1) / R(k, l) - 1| \leq \varepsilon$.
+-/
+@[category research open, AMS 5]
+theorem erdos_1014 (k : ℕ) (hk : k ≥ 3) :
+    ∀ ε : ℝ, ε > 0 →
+    ∃ L₀ : ℕ, ∀ l : ℕ, l ≥ L₀ →
+      |(graphRamseyNumber k (l + 1) : ℝ) / (graphRamseyNumber k l : ℝ) - 1| ≤ ε := by
+  sorry
+
+end Erdos1014
diff --git a/FormalConjectures/ErdosProblems/1029.lean b/FormalConjectures/ErdosProblems/1029.lean
@@ -0,0 +1,62 @@
+/-
+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
+
+*Reference:* [erdosproblems.com/1029](https://www.erdosproblems.com/1029)
+
+If $R(k)$ is the diagonal 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$, then
+$$
+  R(k) / (k \cdot 2^{k/2}) \to \infty.
+$$
+
+Erdős and Szekeres [ErSz35] proved $k \cdot 2^{k/2} \ll R(k) \leq \binom{2k-1}{k-1}$.
+The probabilistic method gives $R(k) \geq (1+o(1)) \cdot \frac{1}{\sqrt{2}\, e} \cdot k \cdot 2^{k/2}$,
+improved by Spencer [Sp75] to $R(k) \geq (1+o(1)) \cdot \frac{\sqrt{2}}{e} \cdot k \cdot 2^{k/2}$.
-If $R(k)$ is the diagonal 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$, then
-$$
-  R(k) / (k \cdot 2^{k/2}) \to \infty.
-$$
-
-Erdős and Szekeres [ErSz35] proved $k \cdot 2^{k/2} \ll R(k) \leq \binom{2k-1}{k-1}$.
-The probabilistic method gives $R(k) \geq (1+o(1)) \cdot \frac{1}{\sqrt{2}\, e} \cdot k \cdot 2^{k/2}$,
-improved by Spencer [Sp75] to $R(k) \geq (1+o(1)) \cdot \frac{\sqrt{2}}{e} \cdot k \cdot 2^{k/2}$.
-If $R(k)$ is the diagonal 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$, then
-$$
-  R(k) / (k \cdot 2^{k/2}) \to \infty.
-$$
-
-Erdős and Szekeres [ErSz35] proved $k \cdot 2^{k/2} \ll R(k) \leq \binom{2k-1}{k-1}$.
-The probabilistic method gives $R(k) \geq (1+o(1)) \cdot \frac{1}{\sqrt{2}\, e} \cdot k \cdot 2^{k/2}$,
-improved by Spencer [Sp75] to $R(k) \geq (1+o(1)) \cdot \frac{\sqrt{2}}{e} \cdot k \cdot 2^{k/2}$.
+
+[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 Finset SimpleGraph
+
+namespace Erdos1029
+
+/--
+Erdős Problem 1029 [Er93, p.337]:
+
+$R(k) / (k \cdot 2^{k/2}) \to \infty$ as $k \to \infty$.
+
+Formulated as: for every $C > 0$, there exists $K_0$ such that for all $k \geq K_0$,
+$R(k) \geq C \cdot k \cdot 2^{k/2}$.
+
+Here $R(k)$ is the diagonal Ramsey number, expressed as `diagRamseyNumber k`.
+-/
+@[category research open, AMS 5]
+theorem erdos_1029 :
+    ∀ C : ℝ, C > 0 →
+    ∃ K₀ : ℕ, ∀ k : ℕ, k ≥ K₀ →
+      (diagRamseyNumber k : ℝ) ≥ C * (k : ℝ) * (2 : ℝ) ^ ((k : ℝ) / 2) := by
+  sorry
+
+end Erdos1029
diff --git a/FormalConjectures/ErdosProblems/1030.lean b/FormalConjectures/ErdosProblems/1030.lean
@@ -0,0 +1,82 @@
+/-
+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
+
+*Reference:* [erdosproblems.com/1030](https://www.erdosproblems.com/1030)
+
+If $R(k,l)$ is the Ramsey number then prove the existence of some $c > 0$ such that
+$$
+  \lim_{k \to \infty} \frac{R(k+1, k)}{R(k, k)} > 1 + c.
+$$
+
+A problem of Erdős and Sós, who could not even prove whether
+$R(k+1,k) - R(k,k) > k^c$ for any $c > 1$.
+
+Burr, Erdős, Faudree, and Schelp [BEFS89] proved that
+$R(k+1,k) - R(k,k) \geq 2k - 5$.
-If $R(k,l)$ is the Ramsey number then prove the existence of some $c > 0$ such that
-$$
-  \lim_{k \to \infty} \frac{R(k+1, k)}{R(k, k)} > 1 + c.
-$$
-
-A problem of Erdős and Sós, who could not even prove whether
-$R(k+1,k) - R(k,k) > k^c$ for any $c > 1$.
-
-Burr, Erdős, Faudree, and Schelp [BEFS89] proved that
-$R(k+1,k) - R(k,k) \geq 2k - 5$.
-If $R(k,l)$ is the Ramsey number then prove the existence of some $c > 0$ such that
-$$
-  \lim_{k \to \infty} \frac{R(k+1, k)}{R(k, k)} > 1 + c.
-$$
-
-A problem of Erdős and Sós, who could not even prove whether
-$R(k+1,k) - R(k,k) > k^c$ for any $c > 1$.
-
-Burr, Erdős, Faudree, and Schelp [BEFS89] proved that
-$R(k+1,k) - R(k,k) \geq 2k - 5$.
+
+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).
+
+[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 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 exist $c > 0$ and $K_0$ such that for all $k \geq K_0$,
+$R(k+1, k) / R(k, k) \geq 1 + c$.
+-/
+@[category research open, AMS 5]
+theorem erdos_1030 :
+    ∃ c : ℝ, c > 0 ∧
+    ∃ K₀ : ℕ, ∀ k : ℕ, k ≥ K₀ →
+      (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_weak :
-theorem erdos_1030_weak :
+theorem erdos_1030.variants.weak :
-theorem erdos_1030_weak :
+theorem erdos_1030.variants.weak :
+    ∃ c : ℝ, c > 1 ∧ ∃ K₀ : ℕ, ∀ k : ℕ, k ≥ K₀ →
+      (graphRamseyNumber (k + 1) k : ℝ) - (graphRamseyNumber k k : ℝ) > (k : ℝ) ^ c := by
+  sorry
+
+end Erdos1030
diff --git a/FormalConjectures/ErdosProblems/112.lean b/FormalConjectures/ErdosProblems/112.lean
@@ -0,0 +1,154 @@
+/-
+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
+
+*Reference:* [erdosproblems.com/112](https://www.erdosproblems.com/112)
+
+A problem of Erdős and Rado on directed Ramsey numbers $k(n,m)$: the minimal $k$ such that
+any directed graph on $k$ vertices must contain either an independent set of size $n$ or a
+transitive tournament of size $m$. Determine $k(n,m)$.
+
+[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)$.
+The exact value is still open.
+-/
+@[category research open, AMS 5]
+theorem erdos_112 :
+    ∀ n m : ℕ, 2 ≤ n → 2 ≤ m →
+      dirRamseyNum n m = answer(sorry) := by
-      dirRamseyNum n m = answer(sorry) := by
+      dirRamseyNum n m = (answer(sorry) : ℕ → ℕ → ℕ) n m := by
+
-      dirRamseyNum n m = answer(sorry) := by
+      dirRamseyNum n m = (answer(sorry) : ℕ → ℕ → ℕ) n m := 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
+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),
+    (∃ 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
+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),
+    (∃ 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
+
+end Erdos112