Problem CX-001 — the fundamental theorem of statistical learning

goaldef

A binary concept class is PAC learnable over all distributions exactly when its VC dimension is finite. The forward direction is the hard half.

def goal : Prop :=
  ∀ (α : Type) [MeasurableSpace α] (C : ConceptClass α Bool),
    IsPACLearnable C Set.univ ↔ HasFiniteVCDim C

Builds on

Finite VC dimension
PAC learnability

From Mathlib

MeasureTheory.Measure.MeasureSpace

import Conjectura.Problems.CX001.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