Do the two definitions of finite VC dimension agree?
A bridge between the corpus's two ways of saying a concept class has bounded shattering.
▸Motivation
The library states finiteness of VC dimension in two ways: HasFiniteVCDim, a uniform bound on shattered sets, and vcDim ≠ ⊤, a supremum in the extended naturals. They should be equivalent.
This is a formalization target rather than a research question, and it is here for a specific reason: two definitions of the same thing that have never been proved equal are exactly the kind of quiet inconsistency a corpus accumulates. Proving it closes that gap; failing to would mean one of them is wrong.
Internal to this corpus. Definitions adapted from cslib.
▸Lean API
import Conjectura.Defs.ComputerScience.Learning.HasFiniteVCDim
import Conjectura.Defs.ComputerScience.Learning.VCDimension
namespace Conjectura.CX003
/-- Is a class of finite VC dimension shattered by no set larger than that dimension?
The definitional direction is immediate; the content is that `vcDim` and
`HasFiniteVCDim` agree, which is the bridge between the two ways the corpus states
finiteness. A formalization target rather than an open question. -/
def goal : Prop :=
∀ (α : Type) (C : ConceptClass α Bool),
HasFiniteVCDim C ↔ vcDim C ≠ ⊤
end Conjectura.CX003▸Definition8
- concept classConjectura.Learning.ConceptClass
A concept class over a domain
αwith labels inβis a set of functionsα → β— the hypotheses a learner is allowed to consider. For binary labels it is equivalently a family of subsets ofα.abbrev ConceptClass (α β : Type*) := Set (α → β)- finite VC dimensionConjectura.Learning.HasFiniteVCDim
A class has finite VC dimension when some
nbounds the size of every set itShatters. By the fundamental theorem of statistical learning this is equivalent to being PAC learnable in the binary agnostic setting.def HasFiniteVCDim {α : Type*} (C : ConceptClass α Bool) : Prop := ∃ n : ℕ, ∀ W : Finset α, Shatters C (W : Set α) → W.card ≤ n- shattersConjectura.Learning.Shatters
A binary concept class shatters a set when every one of its subsets is cut out by some concept — the class can realise every possible labelling of those points.
def Shatters {α : Type*} (C : ConceptClass α Bool) (W : Set α) : Prop := ∀ W' ⊆ W, ∃ c ∈ C, ∀ x ∈ W, (c x = true ↔ x ∈ W')- Vapnik–Chervonenkis dimensionConjectura.Learning.vcDim
The Vapnik–Chervonenkis dimension of a binary concept class is the largest size of a set it
Shatters. It is the combinatorial quantity that controls how much data is needed to learn the class.noncomputable def vcDim {α : Type*} (C : ConceptClass α Bool) : ENat := ⨆ W ∈ {W : Finset α | Shatters C (W : Set α)}, (W.card : ENat)- SetSet
abbrev
- FinsetFinset
structure
- cardW.card
theorem
- ENatENat
def
▸Related work0
▸For your AI
I am proving a theorem in Lean 4 and submitting it to Conjectura.
## Problem CX003 — Do the two definitions of finite VC dimension agree?
A bridge between the corpus's two ways of saying a concept class has bounded shattering.
## Environment (fixed — do not assume anything newer)
- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`
If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.
## The exact statement I must prove
```lean
theorem solution : ∀ (α : Type) (C : ConceptClass α Bool), HasFiniteVCDim C ↔ vcDim C ≠ ⊤ := by
sorry
```
## The file I submit
```lean
import Conjectura.Problems.CX003.Statement
namespace Submission
theorem solution : Conjectura.CX003.goal := by
sorry
end Submission
```
## The Lean definitions of every term in this problem
These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.
### concept class
A concept class over a domain `α` with labels in `β` is a set of functions `α → β` — the hypotheses a learner is allowed to consider. For binary labels it is equivalently a family of subsets of `α`.
```lean
Conjectura.Learning.ConceptClass
-- unfolds to:
abbrev ConceptClass (α β : Type*) := Set (α → β)
```
Defined in this corpus.
### finite VC dimension
A class has finite VC dimension when some `n` bounds the size of every set it `Shatters`. By the fundamental theorem of statistical learning this is equivalent to being PAC learnable in the binary agnostic setting.
```lean
Conjectura.Learning.HasFiniteVCDim
-- unfolds to:
def HasFiniteVCDim {α : Type*} (C : ConceptClass α Bool) : Prop :=
∃ n : ℕ, ∀ W : Finset α, Shatters C (W : Set α) → W.card ≤ n
```
Defined in this corpus.
### shatters
A binary concept class shatters a set when every one of its subsets is cut out by some concept — the class can realise every possible labelling of those points.
```lean
Conjectura.Learning.Shatters
-- unfolds to:
def Shatters {α : Type*} (C : ConceptClass α Bool) (W : Set α) : Prop :=
∀ W' ⊆ W, ∃ c ∈ C, ∀ x ∈ W, (c x = true ↔ x ∈ W')
```
Defined in this corpus.
### Vapnik–Chervonenkis dimension
The Vapnik–Chervonenkis dimension of a binary concept class is the largest size of a set it `Shatters`. It is the combinatorial quantity that controls how much data is needed to learn the class.
```lean
Conjectura.Learning.vcDim
-- unfolds to:
noncomputable def vcDim {α : Type*} (C : ConceptClass α Bool) : ENat :=
⨆ W ∈ {W : Finset α | Shatters C (W : Set α)}, (W.card : ENat)
```
Defined in this corpus.
### Set
abbrev
```lean
Set
```
Defined in Mathlib.
### Finset
structure
```lean
Finset
```
Defined in Mathlib.
### card
theorem
```lean
W.card
```
Defined in Mathlib.
### ENat
def
```lean
ENat
```
Defined in Mathlib.
## Rules — submissions violating these are rejected automatically
1. **Do not change the name or type of `solution`.** It must satisfy the
statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
Declaring your own `goal`, or redefining a name it depends on, produces a
proof of a *different* statement and is rejected. This is the single most
common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
`Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
`snake_case` theorem names, `UpperCamelCase` types.
## What I want from you
Here is my argument in informal mathematics:
> [PASTE YOUR PROOF SKETCH HERE]
Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.Submissions are not open yet
Conjectura is in beta. You can read every statement, every definition and the Lean behind them, and download the exact files the checker uses — but proofs are not being accepted yet.
The reason is a deliberate order of operations. Accepting a proof means running a stranger’s code and standing behind a verdict, and no statement here yet carries a researcher’s name. A machine-checked answer to a question nobody has vouched for is worth very little, so the vouching comes first.
The English write-ups are also switched off during the beta. Nothing on this page is generated by a model.
Discussion
- Nothing yet.
Sign in to take part.