Problem CX-003 — the sample complexity of PAC learning

goaldef

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 ≠ ⊤

Builds on

Finite VC dimension
VC dimension

import Conjectura.Problems.CX003.Statement · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits