VCₙ dimension of convex sets in ℝⁿ, ℝⁿ⁺¹, ℝⁿ⁺²
Every convex set in ℝ^3 has VC_2 dimension at most 2.
From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim. A Lean proof is checked against the statement below by the Lean kernel; a curator confirms before the problem counts as resolved.
Cite
@misc{cairn-vc-dim-convex,
title = {VCₙ dimension of convex sets in ℝⁿ, ℝⁿ⁺¹, ℝⁿ⁺²},
author = {{Cairn Commons contributors}},
howpublished = {\url{https://cairn-commons.com/problems/vc-dim-convex}},
year = {2026},
note = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-29}
} Also: CITATION.cff · Atom feed of results
- Claims
- 0
- Verified
- 0
- Disputed
- 0
- Refuted
- 0
- On the literature board
- 0
Current state
No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.
The problem
The question
Every convex set in has dimension at most 2.
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.
Formal statement (Lean 4)
From Formal Conjectures, module FormalConjectures.Other.VCDimConvex. answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.
theorem hasAddVCNDimAtMost_two_two_of_convex_r3 {C : Set ℝ³} (hC : Convex ℝ C) :
HasAddVCNDimAtMost C 2 2 := sorry
/-- For every $n \ge 1$ there exists some $d$ such that every convex set in $\mathbb R^{n + 1}$ has
$\mathrm{VC}_n$ dimension at most $d$.
This holds with the explicit bound $d = 2^{8(n + 2)^n} - 1$; see
[Kitamura's Lean formalization](https://github.com/KitaKen1/vcdim-convex-finite-bound).
-/
@[category research solved, AMS 5 52,
formal_proof using lean4 at
"https://github.com/KitaKen1/vcdim-convex-finite-bound/blob/9d7685c7c7c8c8e82f47d59da5495a8d5374db99/lean/VCDimConvexBoundFC.lean#L14-L17"]
lemma exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one (n : ℕ) (hn : 1 ≤ n) :
∃ d : ℕ, ∀ C : Set (Fin (n + 1) → ℝ), Convex ℝ C → HasAddVCNDimAtMost C n d := sorry
/-- For every $n \ge 1$ there exists some $d$ such that every convex set in $\mathbb R^{n + 1}$ has
$\mathrm{VC}_n$ dimension at most $d$.
The bound can be taken to be $d = c^n$ for some constant $c \ge 2$ independent of $n$.
-/
@[category research open, AMS 5 52]
lemma exists_exponential_bound_hasAddVCNDimAtMost_n_of_convex_rn_add_one :
∃ c : ℕ, 2 ≤ c ∧ ∀ (n : ℕ) (hn : 1 ≤ n),
∀ C : Set (Fin (n + 1) → ℝ), Convex ℝ C → HasAddVCNDimAtMost C n (c ^ n) := sorry
/-- Is it true that, for all $n$, every convex set in $\mathbb R^{n + 1}$ has
$\mathrm{VC}_n$ dimension at most 3? -/
@[category research open, AMS 5 52]
lemma hasAddVCNDimAtMost_n_two_of_convex_rn_add_one :
answer(sorry) ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → ∀ ⦃C : Set (EuclideanSpace ℝ (Fin (n + 1)))⦄,
Convex ℝ C → HasAddVCNDimAtMost C n 3What counts as progress
- A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
- Partial results: special cases, weaker bounds, reductions — as verified claims.
- Computations and numerical evidence with published code (reproducible).
- Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
- A precise flaw in the formal statement (a misformalisation) — report it upstream too.
Source and licence
Imported from Formal Conjectures (Other), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.