diff --git a/FormalConjectures/ForMathlib/Combinatorics/Additive/VCDim.lean b/FormalConjectures/ForMathlib/Combinatorics/Additive/VCDim.lean
new file mode 100644
index 000000000..ef01e12d4
--- /dev/null
+++ b/FormalConjectures/ForMathlib/Combinatorics/Additive/VCDim.lean
@@ -0,0 +1,106 @@
+/-
+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.ForMathlib.Combinatorics.SetFamily.VCDim
+import Mathlib
+
+open scoped Pointwise
+
+variable {G : Type*} [CommGroup G] {A B : Set G} {n d d' : ℕ}
+
+variable (A d n) in
+/-- A set `A` in an abelian group has VC dimension at most `d` iff one cannot find two sequences
+`x` and `y` of elements indexed by `[d + 1]` and `2 ^ [d + 1]ⁿ` respectively such that
+`y s * x i ∈ A ↔ i ∈ s` for all `i ∈ [d + 1]ⁿ`, `s ⊆ [d + 1]ⁿ`. -/
+@[to_additive
+/-- A set `A` in an abelian group has VCₙ dimension at most `d` iff one cannot find two sequences
+`x` and `y` of elements indexed by `[n] × [d + 1]` and `2 ^ [d + 1]ⁿ` respectively such that
+`y s + ∑ k, x (k, i k) ∈ A ↔ i ∈ s` for all `i ∈ [d + 1]ⁿ`, `s ⊆ [d + 1]ⁿ`. -/]
+def HasMulVCDimAtMost : Prop :=
+  ∀ (x : Fin (d + 1) → G) (y : Set (Fin (d + 1)) → G), ¬ ∀ i s, y s * x i ∈ A ↔ i ∈ s
+
+@[to_additive]
+lemma HasMulVCDimAtMost.mono (h : d ≤ d') (hd : HasMulVCDimAtMost A d) :
+    HasMulVCDimAtMost A d' := by
+  rintro x y hxy
+  replace h : d + 1 ≤ d' + 1 := by omega
+  exact hd (x ∘ Fin.castLE h) (y ∘ Set.image (Fin.castLE h)) fun i s ↦ (hxy ..).trans <| by simp
+
+@[to_additive (attr := simp)]
+lemma hasMulVCDimAtMost_compl : HasMulVCDimAtMost Aᶜ d ↔ HasMulVCDimAtMost A d :=
+  forall_congr' fun x ↦ (compl_involutive.toPerm.arrowCongr <| .refl _).forall_congr fun y ↦
+    not_congr <| forall_congr' fun i ↦ compl_involutive.toPerm.forall_congr <| by simp; tauto
+
+@[to_additive]
+protected alias ⟨HasMulVCDimAtMost.of_compl, HasMulVCDimAtMost.compl⟩ := hasMulVCDimAtMost_compl
+
+@[to_additive (attr := simp)]
+protected lemma HasMulVCDimAtMost.empty : HasMulVCDimAtMost (∅ : Set G) d := by
+  simpa [HasMulVCDimAtMost] using ⟨default, .univ, by simp⟩
+
+@[to_additive (attr := simp)]
+protected lemma HasMulVCDimAtMost.univ : HasMulVCDimAtMost (.univ : Set G) d := by
+  simpa [HasMulVCDimAtMost] using ⟨default, ∅, by simp⟩
+
+@[to_additive (attr := simp)]
+lemma hasVCDimAtMost_smul : HasVCDimAtMost {t • A | t : G} d ↔ HasMulVCDimAtMost A d := by
+  simpa [HasVCDimAtMost, HasMulVCDimAtMost, Classical.skolem (b := fun _ ↦ G), ← funext_iff,
+    Set.mem_smul_set_iff_inv_smul_mem]
+    using forall_congr' fun x ↦ (Equiv.inv _).forall_congr <| by simp
+
+variable (A d n) in
+/-- A set `A` in an abelian group has VCₙ dimension at most `d` iff one cannot find two sequences
+`x` and `y` of elements indexed by `[n] × [d + 1]` and `2 ^ [d + 1]ⁿ` respectively such that
+`y s * ∏ k, x (k, i k) ∈ A ↔ i ∈ s` for all `i ∈ [d + 1]ⁿ`, `s ⊆ [d + 1]ⁿ`. -/
+@[to_additive
+/-- A set `A` in an abelian group has VCₙ dimension at most `d` iff one cannot find two sequences
+`x` and `y` of elements indexed by `[n] × [d + 1]` and `2 ^ [d + 1]ⁿ` respectively such that
+`y s + ∑ k, x (k, i k) ∈ A ↔ i ∈ s` for all `i ∈ [d + 1]ⁿ`, `s ⊆ [d + 1]ⁿ`. -/]
+def HasMulVCNDimAtMost : Prop :=
+  ∀ (x : Fin n → Fin (d + 1) → G) (y : Set (Fin n → Fin (d + 1)) → G),
+    ¬ ∀ i s, y s * ∏ k, x k (i k) ∈ A ↔ i ∈ s
+
+@[to_additive]
+lemma HasMulVCNDimAtMost.mono (h : d ≤ d') (hd : HasMulVCNDimAtMost A n d) :
+    HasMulVCNDimAtMost A n d' := by
+  rintro x y hxy
+  replace h : d + 1 ≤ d' + 1 := by omega
+  exact hd (x · ∘ Fin.castLE h) (y ∘ Set.image (Fin.castLE h ∘ ·)) fun i s ↦
+    (hxy ..).trans <| by simp [funext_iff]; simp [← funext_iff]
+
+@[to_additive (attr := simp)]
+lemma hasMulVCNDimAtMost_compl : HasMulVCNDimAtMost Aᶜ n d ↔ HasMulVCNDimAtMost A n d :=
+  forall_congr' fun x ↦ (compl_involutive.toPerm.arrowCongr <| .refl _).forall_congr fun y ↦
+    not_congr <| forall_congr' fun i ↦ compl_involutive.toPerm.forall_congr <| by simp; tauto
+
+@[to_additive]
+protected alias ⟨HasMulVCNDimAtMost.of_compl, HasMulVCNDimAtMost.compl⟩ := hasMulVCNDimAtMost_compl
+
+@[to_additive (attr := simp)]
+protected lemma HasMulVCNDimAtMost.empty : HasMulVCNDimAtMost (∅ : Set G) n d := by
+  simpa [HasMulVCNDimAtMost] using ⟨default, .univ, by simp⟩
+
+@[to_additive (attr := simp)]
+protected lemma HasMulVCNDimAtMost.univ : HasMulVCNDimAtMost (.univ : Set G) n d := by
+  simpa [HasMulVCNDimAtMost] using ⟨default, ∅, by simp⟩
+
+@[to_additive (attr := simp)]
+lemma hasMulVCNDimAtMost_one : HasMulVCNDimAtMost A 1 d ↔ HasMulVCDimAtMost A d := by
+  symm
+  refine (Equiv.funUnique ..).symm.forall_congr fun x ↦
+    ((Equiv.Set.congr <| Equiv.funUnique ..).arrowCongr <| .refl _).symm.forall_congr fun y ↦
+    not_congr <| (Equiv.funUnique ..).symm.forall_congr fun i ↦
+    (Equiv.Set.congr <| Equiv.funUnique ..).symm.forall_congr fun s ↦ ?_
+  simp [Set.image_image, funext_iff]
diff --git a/FormalConjectures/ForMathlib/Combinatorics/SetFamily/VCDim.lean b/FormalConjectures/ForMathlib/Combinatorics/SetFamily/VCDim.lean
new file mode 100644
index 000000000..911c3cbb4
--- /dev/null
+++ b/FormalConjectures/ForMathlib/Combinatorics/SetFamily/VCDim.lean
@@ -0,0 +1,82 @@
+/-
+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.Data.Set.Card
+
+/-!
+# VC dimension of a set family
+
+This file defines the VC dimension of a set family as the maximum size of a set it shatters.
+-/
+
+variable {α : Type*} {𝒜 ℬ : Set (Set α)} {A B : Set α} {a : α} {d d' : ℕ}
+
+variable (𝒜 A) in
+/-- A set family `𝒜` shatters a set `A` if restricting `𝒜` to `A` gives rise to all subsets of `A`.
+-/
+def Shatters : Prop := ∀ ⦃B⦄, B ⊆ A → ∃ C ∈ 𝒜, A ∩ C = B
+
+lemma Shatters.exists_inter_eq_singleton (hs : Shatters 𝒜 A) (ha : a ∈ A) : ∃ B ∈ 𝒜, A ∩ B = {a} :=
+  hs <| Set.singleton_subset_iff.2 ha
+
+lemma Shatters.mono_left (h : 𝒜 ⊆ ℬ) (h𝒜 : Shatters 𝒜 A) : Shatters ℬ A :=
+  fun _B hB ↦ let ⟨u, hu, hut⟩ := h𝒜 hB; ⟨u, h hu, hut⟩
+
+lemma Shatters.mono_right (h : B ⊆ A) (hs : Shatters 𝒜 A) : Shatters 𝒜 B := fun u hu ↦ by
+  obtain ⟨v, hv, rfl⟩ := hs (hu.trans h); exact ⟨v, hv, inf_congr_right hu <| inf_le_of_left_le h⟩
+
+lemma Shatters.exists_superset (h : Shatters 𝒜 A) : ∃ B ∈ 𝒜, A ⊆ B :=
+  let ⟨B, hB, hst⟩ := h .rfl; ⟨B, hB, Set.inter_eq_left.1 hst⟩
+
+lemma Shatters.of_forall_subset (h : ∀ B, B ⊆ A → B ∈ 𝒜) : Shatters 𝒜 A :=
+  fun B hB ↦ ⟨B, h _ hB, Set.inter_eq_right.2 hB⟩
+
+protected lemma Shatters.nonempty (h : Shatters 𝒜 A) : 𝒜.Nonempty :=
+  let ⟨B, hB, _⟩ := h .rfl; ⟨B, hB⟩
+
+@[simp] lemma shatters_empty : Shatters 𝒜 ∅ ↔ 𝒜.Nonempty :=
+  ⟨Shatters.nonempty, fun ⟨A, hs⟩ B hB ↦ ⟨A, hs, by simpa [eq_comm] using hB⟩⟩
+
+protected lemma Shatters.subset_iff (h : Shatters 𝒜 A) : B ⊆ A ↔ ∃ u ∈ 𝒜, A ∩ u = B :=
+  ⟨fun hB ↦ h hB, by rintro ⟨u, _, rfl⟩; exact Set.inter_subset_left⟩
+
+lemma shatters_iff : Shatters 𝒜 A ↔ (A ∩ ·) '' 𝒜 = A.powerset :=
+  ⟨fun h ↦ by ext B; simp [h.subset_iff], fun h B hB ↦ h.superset hB⟩
+
+lemma univ_shatters : Shatters .univ A := .of_forall_subset <| by simp
+
+@[simp] lemma shatters_univ : Shatters 𝒜 .univ ↔ 𝒜 = .univ := by
+  simp [Shatters, Set.eq_univ_iff_forall]
+
+variable (𝒜 d) in
+/-- A set family `𝒜` has VC dimension at most `d` if there are no families `x` of elements indexed
+by `[d + 1]` and `A` of sets of `𝒜` indexed by `2^[d + 1]` such that `x i ∈ A s ↔ i ∈ s` for all
+`i ∈ [d], s ⊆ [d]`. -/
+def HasVCDimAtMost : Prop :=
+  ∀ (x : Fin (d + 1) → α) (A : Set (Fin (d + 1)) → Set α),
+    (∀ s, A s ∈ 𝒜) → ¬ ∀ i s, x i ∈ A s ↔ i ∈ s
+
+lemma HasVCDimAtMost.anti (h𝒜ℬ : 𝒜 ≤ ℬ) (hℬ : HasVCDimAtMost ℬ d) : HasVCDimAtMost 𝒜 d :=
+  fun _x _A hA ↦ hℬ _ _ fun _s ↦ h𝒜ℬ <| hA _
+
+lemma HasVCDimAtMost.mono (h : d ≤ d') (hd : HasVCDimAtMost 𝒜 d) : HasVCDimAtMost 𝒜 d' := by
+  rintro x A hA hxA
+  replace h : d + 1 ≤ d' + 1 := by omega
+  exact hd (x ∘ Fin.castLE h) (A ∘ Set.image (Fin.castLE h)) (by simp [hA]) fun i s ↦
+    (hxA ..).trans <| by simp
+
+@[simp] lemma HasVCDimAtMost.empty : HasVCDimAtMost (∅ : Set (Set α)) d := by simp [HasVCDimAtMost]
+
+proof_wanted hasVCDimAtMost_iff_shatters : HasVCDimAtMost 𝒜 d ↔ ∀ A, Shatters 𝒜 A → A.encard ≤ d
diff --git a/FormalConjectures/Other/VCDimConvex.lean b/FormalConjectures/Other/VCDimConvex.lean
new file mode 100644
index 000000000..3bf86b74f
--- /dev/null
+++ b/FormalConjectures/Other/VCDimConvex.lean
@@ -0,0 +1,67 @@
+/-
+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
+
+/-!
+# VCₙ dimension of convex sets in ℝⁿ, ℝⁿ⁺¹, ℝⁿ⁺²
+
+In the literature it is known that every convex set in ℝ² has VC dimension at most 3,
+and there exists a convex set in ℝ³ with infinite VC dimension (even more strongly,
+which shatters an infinite set).
+
+This file states that every convex set in ℝⁿ has finite VCₙ dimension, constructs a convex set in
+ℝⁿ⁺² with infinite VCₙ dimension (even more strongly, which n-shatters an infinite set),
+and conjectures that every convex set in ℝⁿ⁺¹ has finite VCₙ dimension.
+-/
+
+open scoped EuclideanGeometry Pointwise
+
+/-! ### What's known in the literature -/
+
+/-- Every convex set in ℝ² has VC dimension at most 3. -/
+@[category research solved, AMS 5 52]
+lemma hasAddVCDimAtMost_three_of_convex_r2 {C : Set ℝ²} (hC : Convex ℝ C) : HasAddVCDimAtMost C 3 :=
+  sorry
+
+/-- There exists a set in ℝ³ shattering an infinite set. -/
+@[category research solved, AMS 5 52]
+lemma exists_infinite_convex_r3_shatters :
+    ∃ A C : Set ℝ³, A.Infinite ∧ Convex ℝ C ∧ Shatters {t +ᵥ C | t : ℝ³} A := sorry
+
+/-! ### What's not in the literature -/
+
+/-- There exists a set of infinite VCₙ dimension in ℝⁿ⁺². -/
+@[category research solved, AMS 5 52]
+lemma exists_convex_rn_add_two_vc_n_forall_not_hasAddVCNDimAtMost (n : ℕ) :
+    ∃ C : Set (Fin (n + 2) → ℝ), Convex ℝ C ∧ ∀ d, ¬ HasAddVCNDimAtMost C n d := sorry
+
+/-! ### Conjectures -/
+
+/-- Every convex set in ℝ³ has VC₂ dimension at most 1. -/
+@[category research open, AMS 5 52]
+lemma hasAddVCNDimAtMost_two_one_of_convex_r3 {C : Set ℝ³} (hC : Convex ℝ C) :
+    HasAddVCNDimAtMost C 2 1 := sorry
+
+/-- For every `n` there exists some `d` such that every convex set in ℝⁿ⁺¹ has VCₙ dimension at
+most `d`. -/
+@[category research open, AMS 5 52]
+lemma exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one (n : ℕ) :
+    ∃ d : ℕ, ∀ C : Set (Fin (n + 1) → ℝ), Convex ℝ C → HasAddVCNDimAtMost C n d := sorry
+
+/-- If `n ≥ 2`, every convex set in ℝⁿ⁺¹ has VCₙ dimension at most 1. -/
+@[category research open, AMS 5 52]
+lemma hasAddVCNDimAtMost_n_one_of_convex_rn_add_one {n : ℕ} (hn : 2 ≤ n) {C : Set (Fin (n + 1) → ℝ)}
+    (hC : Convex ℝ C) : HasAddVCNDimAtMost C n 1 := sorry
diff --git a/FormalConjectures/Util/ForMathlib.lean b/FormalConjectures/Util/ForMathlib.lean
index b1ed7e74f..2e4e114f8 100644
--- a/FormalConjectures/Util/ForMathlib.lean
+++ b/FormalConjectures/Util/ForMathlib.lean
@@ -30,8 +30,10 @@ import FormalConjectures.ForMathlib.Analysis.SpecialFunctions.NthRoot
 import FormalConjectures.ForMathlib.Combinatorics.AP.Basic
 import FormalConjectures.ForMathlib.Combinatorics.Additive.Basis
 import FormalConjectures.ForMathlib.Combinatorics.Additive.Convolution
+import FormalConjectures.ForMathlib.Combinatorics.Additive.VCDim
 import FormalConjectures.ForMathlib.Combinatorics.Basic
 import FormalConjectures.ForMathlib.Combinatorics.Ramsey
+import FormalConjectures.ForMathlib.Combinatorics.SetFamily.VCDim
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Balanced
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Coloring
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.DiamExtra