From 9cfdc006500a2474b152185eb93d1032e3bf4fc4 Mon Sep 17 00:00:00 2001
From: ruskaruma <ishaan.sinha10@gmail.com>
Date: Fri, 9 Jan 2026 04:18:35 +0530
Subject: [PATCH 1/3] =?UTF-8?q?feat:=20add=20Erd=C5=91s=20Problem=20567=20?=
 =?UTF-8?q?and=20refactor=20sizeRamsey?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 FormalConjectures/ErdosProblems/566.lean      | 61 ++++++++++++++++
 FormalConjectures/ErdosProblems/567.lean      | 71 +++++++++++++++++++
 .../Combinatorics/SimpleGraph/SizeRamsey.lean | 59 +++++++++++++++
 3 files changed, 191 insertions(+)
 create mode 100644 FormalConjectures/ErdosProblems/566.lean
 create mode 100644 FormalConjectures/ErdosProblems/567.lean
 create mode 100644 FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean

diff --git a/FormalConjectures/ErdosProblems/566.lean b/FormalConjectures/ErdosProblems/566.lean
new file mode 100644
index 000000000..acdb6daf3
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/566.lean
@@ -0,0 +1,61 @@
+/-
+Copyright 2025 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
+import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.SizeRamsey
+
+/-!
+# Erdős Problem 566
+
+Let $G$ be such that any subgraph on $k$ vertices has at most $2k-3$ edges.
+Is it true that, if $H$ has $m$ edges and no isolated vertices, then
+$$ \hat{r}(G,H) \ll m? $$
+
+In other words, is $G$ Ramsey size linear?
+
+*Reference:* [erdosproblems.com/566](https://www.erdosproblems.com/566)
+
+[EFRS93] Erdős, Faudree, Rousseau and Schelp, _Ramsey size linear graphs_.
+Combin. Probab. Comput. (1993), 389-399.
+-/
+
+namespace Erdos566
+
+open SimpleGraph
+
+/--
+**Erdős Problem 566**
+
+Let $G$ be such that any subgraph on $k$ vertices has at most $2k-3$ edges.
+Is it true that, if $H$ has $m$ edges and no isolated vertices, then $\hat{r}(G,H) \ll m$?
+
+In other words: if $G$ is sparse (every induced subgraph on $k$ vertices has $≤ 2k-3$ edges),
+is $G$ Ramsey size linear?
+-/
+@[category research open, AMS 05]
+theorem erdos_566 : answer(sorry) ↔
+    ∀ (p : ℕ) (G : SimpleGraph (Fin p)),
+      -- G is sparse: every induced subgraph on k ≥ 2 vertices has ≤ 2k - 3 edges
+      (∀ S : Finset (Fin p), 2 ≤ S.card → (G.induce S).edgeSet.ncard ≤ 2 * S.card - 3) →
+      -- Then G is Ramsey size linear
+      ∃ c > (0 : ℝ), ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [DecidableRel H.Adj],
+        -- H has no isolated vertices
+        (∀ v, 0 < H.degree v) →
+        -- r̂(G,H) ≤ c · m
+        (sizeRamsey G H : ℝ) ≤ c * H.edgeSet.ncard := by
+  sorry
+
+end Erdos566
diff --git a/FormalConjectures/ErdosProblems/567.lean b/FormalConjectures/ErdosProblems/567.lean
new file mode 100644
index 000000000..34114983f
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/567.lean
@@ -0,0 +1,71 @@
+/-
+Copyright 2025 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
+import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.SizeRamsey
+
+/-!
+# Erdős Problem 567
+
+Let $G$ be either $Q_3$ or $K_{3,3}$ or $H_5$ (the last formed by adding two vertex-disjoint chords
+to $C_5$). Is it true that, if $H$ has $m$ edges and no isolated vertices, then
+$$ \hat{r}(G,H) \ll m? $$
+
+In other words, is $G$ Ramsey size linear? A special case of Problem 566.
+
+*Reference:* [erdosproblems.com/567](https://www.erdosproblems.com/567)
+
+[EFRS93] Erdős, Faudree, Rousseau and Schelp, _Ramsey size linear graphs_.
+Combin. Probab. Comput. (1993), 389-399.
+-/
+
+namespace Erdos567
+
+open SimpleGraph
+
+/-- $Q_3$ is the 3-dimensional hypercube graph (8 vertices, 12 edges).
+Vertices are 3-bit vectors. Two vertices are adjacent iff they differ in exactly one bit. -/
+def Q3 : SimpleGraph (Fin 3 → Bool) :=
+  SimpleGraph.fromRel fun a b => (Finset.univ.filter fun i => a i ≠ b i).card = 1
+
+/-- $K_{3,3}$ is the complete bipartite graph with partition sizes 3, 3 (6 vertices, 9 edges). -/
+def K33 : SimpleGraph (Fin 3 ⊕ Fin 3) := completeBipartiteGraph (Fin 3) (Fin 3)
+
+/-- $H_5$ is $C_5$ with two vertex-disjoint chords (5 vertices, 7 edges).
+Edges: cycle 0-1-2-3-4-0 plus chords {0,2} and {1,3}. -/
+def H5 : SimpleGraph (Fin 5) :=
+  SimpleGraph.fromRel fun u v =>
+    -- Cycle C5 edges
+    (u.val + 1) % 5 = v.val ∨ (v.val + 1) % 5 = u.val ∨
+    -- Chord 0-2
+    ({u, v} : Finset (Fin 5)) = {0, 2} ∨
+    -- Chord 1-3
+    ({u, v} : Finset (Fin 5)) = {1, 3}
+
+/--
+**Erdős Problem 567**
+
+Let $G$ be either $Q_3$ or $K_{3,3}$ or $H_5$.
+Is it true that $G$ is Ramsey size linear?
+-/
+@[category research open, AMS 05]
+theorem erdos_567 : answer(sorry) ↔
+    IsRamseySizeLinear Q3 ∧
+    IsRamseySizeLinear K33 ∧
+    IsRamseySizeLinear H5 := by
+  sorry
+
+end Erdos567
diff --git a/FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean b/FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean
new file mode 100644
index 000000000..350870891
--- /dev/null
+++ b/FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean
@@ -0,0 +1,59 @@
+/-
+Copyright 2025 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 Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.SimpleGraph.Finite
+import Mathlib.Combinatorics.SimpleGraph.Copy
+import Mathlib.Data.Set.Card
+import Mathlib.Data.Nat.Lattice
+import Mathlib.Data.Real.Basic
+
+/-!
+# Size Ramsey Number
+
+This file defines the size Ramsey number for simple graphs.
+
+## Definition
+
+The size Ramsey number `r̂(G, H)` is the minimum number of edges in a graph `F`
+such that any 2-coloring of `F`'s edges contains a copy of `G` in one color or `H` in the other.
+-/
+
+namespace SimpleGraph
+
+/--
+The size Ramsey number `r̂(G, H)` is the minimum number of edges in a graph `F`
+such that any 2-coloring of `F`'s edges contains a copy of `G` in one color or `H` in the other.
+
+A 2-coloring is represented by a subgraph `R ≤ F` (the "red" edges); the "blue" edges are `F \ R`.
+-/
+noncomputable def sizeRamsey {α β : Type*} [Fintype α] [Fintype β]
+    (G : SimpleGraph α) (H : SimpleGraph β) : ℕ :=
+  sInf { m | ∃ (n : ℕ) (F : SimpleGraph (Fin n)),
+    F.edgeSet.ncard = m ∧
+    ∀ (R : SimpleGraph (Fin n)), R ≤ F →
+      G.IsContained R ∨ H.IsContained (F \ R) }
+
+/--
+A graph `G` is **Ramsey size linear** if there exists a constant `c > 0` such that
+for all graphs `H` with `m` edges and no isolated vertices, `r̂(G, H) ≤ c · m`.
+-/
+def IsRamseySizeLinear {α : Type*} [Fintype α] (G : SimpleGraph α) : Prop :=
+  ∃ c > (0 : ℝ), ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [DecidableRel H.Adj],
+    (∀ v, 0 < H.degree v) →
+    (sizeRamsey G H : ℝ) ≤ c * H.edgeSet.ncard
+
+end SimpleGraph

From 0573e3fe9b3022b50c89f8f16c2201fe8ac9f95e Mon Sep 17 00:00:00 2001
From: ruskaruma <ishaan.sinha10@gmail.com>
Date: Sat, 10 Jan 2026 00:50:28 +0530
Subject: [PATCH 2/3] address review

---
 FormalConjectures/ErdosProblems/566.lean |  1 -
 FormalConjectures/ErdosProblems/567.lean | 46 ++++++++++++++----------
 FormalConjectures/Util/ForMathlib.lean   |  1 +
 3 files changed, 29 insertions(+), 19 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/566.lean b/FormalConjectures/ErdosProblems/566.lean
index acdb6daf3..56711ca94 100644
--- a/FormalConjectures/ErdosProblems/566.lean
+++ b/FormalConjectures/ErdosProblems/566.lean
@@ -15,7 +15,6 @@ limitations under the License.
 -/
 
 import FormalConjectures.Util.ProblemImports
-import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.SizeRamsey
 
 /-!
 # Erdős Problem 566
diff --git a/FormalConjectures/ErdosProblems/567.lean b/FormalConjectures/ErdosProblems/567.lean
index 34114983f..273b71d62 100644
--- a/FormalConjectures/ErdosProblems/567.lean
+++ b/FormalConjectures/ErdosProblems/567.lean
@@ -15,7 +15,6 @@ limitations under the License.
 -/
 
 import FormalConjectures.Util.ProblemImports
-import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.SizeRamsey
 
 /-!
 # Erdős Problem 567
@@ -35,37 +34,48 @@ Combin. Probab. Comput. (1993), 389-399.
 namespace Erdos567
 
 open SimpleGraph
+open scoped Finset
 
 /-- $Q_3$ is the 3-dimensional hypercube graph (8 vertices, 12 edges).
 Vertices are 3-bit vectors. Two vertices are adjacent iff they differ in exactly one bit. -/
-def Q3 : SimpleGraph (Fin 3 → Bool) :=
-  SimpleGraph.fromRel fun a b => (Finset.univ.filter fun i => a i ≠ b i).card = 1
+def Q3 : SimpleGraph (Fin 3 → Bool) where
+  Adj u v := #{i | u i ≠ v i} = 1
+  symm _ _ := by simp [eq_comm]
+  loopless _ := by simp
 
 /-- $K_{3,3}$ is the complete bipartite graph with partition sizes 3, 3 (6 vertices, 9 edges). -/
 def K33 : SimpleGraph (Fin 3 ⊕ Fin 3) := completeBipartiteGraph (Fin 3) (Fin 3)
 
 /-- $H_5$ is $C_5$ with two vertex-disjoint chords (5 vertices, 7 edges).
-Edges: cycle 0-1-2-3-4-0 plus chords {0,2} and {1,3}. -/
+Also known as $K_4^*$ (the graph obtained from $K_4$ by subdividing one edge). -/
 def H5 : SimpleGraph (Fin 5) :=
-  SimpleGraph.fromRel fun u v =>
-    -- Cycle C5 edges
-    (u.val + 1) % 5 = v.val ∨ (v.val + 1) % 5 = u.val ∨
-    -- Chord 0-2
-    ({u, v} : Finset (Fin 5)) = {0, 2} ∨
-    -- Chord 1-3
-    ({u, v} : Finset (Fin 5)) = {1, 3}
+  .cycleGraph 5 ⊔ .edge 0 2 ⊔ .edge 1 3
 
 /--
-**Erdős Problem 567**
+**Erdős Problem 567 (Q3)**
 
-Let $G$ be either $Q_3$ or $K_{3,3}$ or $H_5$.
-Is it true that $G$ is Ramsey size linear?
+Is $Q_3$ (the 3-dimensional hypercube) Ramsey size linear?
 -/
 @[category research open, AMS 05]
-theorem erdos_567 : answer(sorry) ↔
-    IsRamseySizeLinear Q3 ∧
-    IsRamseySizeLinear K33 ∧
-    IsRamseySizeLinear H5 := by
+theorem erdos_567_Q3 : answer(sorry) ↔ IsRamseySizeLinear Q3 := by
+  sorry
+
+/--
+**Erdős Problem 567 (K33)**
+
+Is $K_{3,3}$ Ramsey size linear?
+-/
+@[category research open, AMS 05]
+theorem erdos_567_K33 : answer(sorry) ↔ IsRamseySizeLinear K33 := by
+  sorry
+
+/--
+**Erdős Problem 567 (H5)**
+
+Is $H_5$ ($C_5$ with two vertex-disjoint chords) Ramsey size linear?
+-/
+@[category research open, AMS 05]
+theorem erdos_567_H5 : answer(sorry) ↔ IsRamseySizeLinear H5 := by
   sorry
 
 end Erdos567
diff --git a/FormalConjectures/Util/ForMathlib.lean b/FormalConjectures/Util/ForMathlib.lean
index e97d5057c..c65e1563b 100644
--- a/FormalConjectures/Util/ForMathlib.lean
+++ b/FormalConjectures/Util/ForMathlib.lean
@@ -38,6 +38,7 @@ import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.DiamExtra
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Definitions
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Domination
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Invariants
+import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.SizeRamsey
 import FormalConjectures.ForMathlib.Computability.Encoding
 import FormalConjectures.ForMathlib.Computability.TuringMachine.BusyBeavers
 import FormalConjectures.ForMathlib.Computability.TuringMachine.Notation

From 5ff84165bad1f4be9085e48183788a3dc0ab2764 Mon Sep 17 00:00:00 2001
From: ruskaruma <ishaan.sinha10@gmail.com>
Date: Sat, 10 Jan 2026 00:52:35 +0530
Subject: [PATCH 3/3] fix: minimize imports in SizeRamsey.lean

---
 .../ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean      | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean b/FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean
index 350870891..164b6a001 100644
--- a/FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean
+++ b/FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean
@@ -14,12 +14,10 @@ See the License for the specific language governing permissions and
 limitations under the License.
 -/
 
-import Mathlib.Combinatorics.SimpleGraph.Basic
-import Mathlib.Combinatorics.SimpleGraph.Finite
 import Mathlib.Combinatorics.SimpleGraph.Copy
-import Mathlib.Data.Set.Card
 import Mathlib.Data.Nat.Lattice
 import Mathlib.Data.Real.Basic
+import Mathlib.Data.Set.Card
 
 /-!
 # Size Ramsey Number