Skip to content

Robby955/FormalSLT

BranchesTags

Repository files navigation

FormalSLT

CI Lean 4 Mathlib License: MIT

theorems and lemmas FormalSLT modules Lean lines Zero sorry Axioms

Finite-sample statistical learning theory, checked in Lean 4. FormalSLT records explicit theorem statements, constants, and scope boundaries for finite learning-theory proof routes. TheoremPath uses these checked statements as source material for the web and iOS learning surfaces.

The public surface is intentionally small:

  • FormalSLT: checked Lean theorem statements, constants, and scope fences.
  • theorempath.com: theorem pages, source links, and audit pages keyed by the same theorem names.
  • theorem-path-ios: review paths and saved theorem cards keyed by the same theorem IDs.

Counts are surfaced by the badges above and checked against generated badge JSON by scripts/generate_badge_counts.py on every CI run.

FormalSLT is a Lean 4 library for finite-sample statistical learning theory. The current public surface includes:

  1. finite-class concentration and countable-time confidence sequences for [0,1] losses;
  2. Rademacher, VC, bounded-differences, stability, and finite PAC-Bayes theorem routes with explicit constants; and
  3. a finite Dudley ladder from sub-Gaussian finite maximal inequalities through finite-net chaining to a covering-number entropy-integral endpoint.

The Dudley layer is finite by design. It includes reusable finite-net and finite-covering APIs, a unit-interval worked example with explicit finite meshes, and a two-point Rademacher entropy-integral instantiation.

The concentration layer now carries the sharp McDiarmid bounded-differences inequality over a homogeneous product measure. For a function whose value changes by at most c k when coordinate k is altered, the library proves the one-sided tail exp(-2ε²/∑ₖcₖ²) (mcdiarmid_of_hasBoundedDifferences_sharp), its lower-tail form (mcdiarmid_of_hasBoundedDifferences_sharp_lower), and the two-sided bound 2·exp(-2ε²/∑ₖcₖ²) (mcdiarmid_twoSided_of_hasBoundedDifferences_sharp). The sharp 2B² exponent is propagated into the high-probability Rademacher, finite-class, VC, and algorithmic-stability wrappers listed below, replacing the looser Azuma 8B² constant on those paths. The localized-Rademacher wrapper still uses the older Azuma constant. The bounded-differences theorem is stated for the same product law in each coordinate, not for arbitrary non-iid product spaces.

The PAC-Bayes layer now includes a finite Bernstein margin-proxy shell. It adds a supplied per-hypothesis variance proxy, a normalized Bernstein prior-moment certificate, fixed-λ finite bad-event bounds, and a posterior-dependent square-root-plus-linear wrapper. This is a supplied-proxy finite shell: it is not yet a concrete classifier-margin extractor, an all-real-λ optimization theorem, or a continuous hypothesis-space theorem.

Zero sorry. Zero admit. Zero custom axioms. Live module, theorem, and line counts are in the badges at the top of this file.

Counts are generated with find FormalSLT -name '*.lean', find FormalSLT examples -name '*.lean', and find FormalSLT examples -name '*.lean' -print0 | xargs -0 wc -l.

The printed axiom profile for the v0.1 headline surface stays inside: [propext, Classical.choice, Quot.sound].

FormalSLT theorem chain

Checked Surfaces

Each surface has one machine-checked endpoint and a checker file you can run with lake env lean <checker>:

  • Finite-class Hoeffding confidence sequence endpoint FiniteClassConfidenceSequence.failure_probability_le, checker examples/CheckUniformConvergence.lean
  • Unit-interval finite-net Dudley bridge endpoint unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound_prefixFree, checker examples/CheckUnitIntervalDudley.lean
  • Packaged finite dyadic Dudley API endpoint FiniteDyadicDudleyInstance.suppliedSup_dudley_bound, checker examples/CheckV01Usability.lean
  • Two-point dyadic Dudley bound endpoint twoPointRademacherSup_dudley_m_bound, checker examples/CheckTwoPointDudley.lean
  • Fin n discrete dyadic Dudley bound endpoint finDiscreteRademacherSup_dudley_m_bound, checker examples/CheckFiniteDiscreteDudley.lean
  • Two-sided sharp McDiarmid over a homogeneous product measure endpoint mcdiarmid_twoSided_of_hasBoundedDifferences_sharp, checker examples/CheckSharpMcDiarmid.lean
  • PAC-Bayes Bernstein supplied margin-proxy shell endpoint finitePACBayesBernsteinMargin_badEventMass_le_delta, checker examples/CheckPACBayesBernstein.lean
  • Finite Dudley entropy-integral endpoint endpoint dudley_entropy_integral_of_antitone_coveringNumber, checker examples/CheckDudleyEntropyIntegral.lean
  • Two-point Rademacher entropy-integral instantiation endpoint twoPointRademacher_centered_dudley_entropy_integral, checker examples/CheckTwoPointDudleyIntegral.lean

The confidence-sequence chain makes the finite-class and countable-time union bound explicit. The Dudley chain proves the finite maximal inequality, the finite-net chaining sum, the sum-to-integral comparison, and the assembled covering-number endpoint without asserting a measurable supremum theorem over arbitrary non-finite classes.

Fast Verification

From the repository root:

lake exe cache get
lake build FormalSLT
lake env lean examples/CheckV01Usability.lean
lake env lean examples/CheckUniformConvergence.lean
lake env lean examples/CheckUnitIntervalDudley.lean
lake env lean examples/CheckTwoPointDudley.lean
lake env lean examples/CheckFiniteDiscreteDudley.lean
lake env lean examples/CheckDudleyEntropyIntegral.lean
lake env lean examples/CheckPACBayesBernstein.lean
python3 scripts/generate_proof_frontier_manifest.py --check
python3 scripts/generate_badge_counts.py --check

If lake is not on the shell path, use ~/.elan/bin/lake.

What This Does Not Prove

  • No general continuous Dudley theorem with arbitrary measurable suprema.
  • No arbitrary measurable-supremum construction over non-finite classes.
  • No general separability theorem.
  • No infinite-class confidence sequence.
  • No martingale or e-process stopping theorem in the v0.1 confidence-sequence surface.
  • No neural-network generalization theorem.

Where to start

TheoremPath Surfaces

FormalSLT is the checked source layer for TheoremPath learning surfaces. The connection is intentionally simple: theorem names and source links in this repository are reused by the site and app.

theorempath.com

The site renders FormalSLT theorem names with source links, prerequisite paths, and audit pages. Direct entry points include:

TheoremPath iOS

The Swift app uses the same theorem IDs for review paths and saved theorem cards. Build status and release notes live in the iOS repository.

Semantic Linker v0

In development: a theorem-to-code view that places selected FormalSLT Lean statements next to executable ML code. It is not part of the current public FormalSLT proof surface.

For researchers

If you work on statistical learning theory, mechanistic interpretability, or singular learning theory (SLT), the finite theorem surface is reusable today:

  • Pin against Robby955/FormalSLT in your lakefile.lean to import the checked statements directly. Hypothesis lists and constants are visible in the type signatures, not buried in tactic blocks.
  • Use the sharp McDiarmid wrappers (mcdiarmid_of_hasBoundedDifferences_sharp, mcdiarmid_twoSided_of_hasBoundedDifferences_sharp) when you need the 2B² exponent on high-probability Rademacher and VC paths (VC = Vapnik-Chervonenkis).
  • Fork the conditional sub-Gamma extractor for bounded, conditionally centered increments with an explicit conditional second-moment proxy.
  • Reuse the dyadic Dudley API instances (twoPointDudleyInstance, finDiscreteDudleyInstance, FiniteDyadicDudleyInstance) as templates for your own metric-index examples.
  • Reuse the PAC-Bayes Bernstein margin-proxy shell when you have a supplied per-hypothesis variance proxy (PAC = Probably Approximately Correct).
  • Import the finite Dudley entropy-integral endpoint through FormalSLT.Covering.DudleyEntropyIntegral when your application supplies finite covers and the required antitone covering-number profile.

See docs/related-work.md for how FormalSLT sits next to mathlib4's empirical-process and Rademacher generalization files.

For students

If you are entering SLT or empirical process theory, the recommended path is:

  1. Start at theorempath.com and follow the prerequisite chain to the topic you need. The site maps the informal intuition.
  2. Click through to the linked Lean theorem. This repository holds the checked statement and the proof.
  3. Read How to read the proofs and Intuition for orientation on Lean syntax and the PAC-Bayes / Rademacher building blocks.
  4. Use theorempath.com/theorems/formalslt-v0-1 as the v0.1 walkthrough that ties the site and the library together.

The native iOS companion is the same content with offline review cards and local mastery tracking.

Library Map

FormalSLT records finite-sample statistical learning bounds as Lean theorems with explicit hypotheses and constants. Beyond the v0.1 headline chains, the library contains checked finite routes for:

  • finite-class ERM, Rademacher symmetrization, Massart, Sauer-Shelah, and VC-style sample-complexity wrappers;
  • high-probability Rademacher and VC sample-complexity bounds carrying the sharp McDiarmid 2B² exponent;
  • the sharp bounded-differences/McDiarmid concentration module (Concentration.SharpMcDiarmid): one-sided, lower-tail, and two-sided homogeneous product-measure tails, plus the additive independent special case;
  • finite contraction and linear-predictor Rademacher bounds;
  • finite Bennett/Bernstein and localized-Rademacher scaffolding;
  • conditional sub-Gamma MGF extraction for bounded, conditionally centered increments with an explicit conditional second-moment proxy;
  • finite covering, finite sub-Gaussian chaining, and finite Dudley entropy-budget wrappers;
  • finite algorithmic stability expected-gap and high-probability wrappers;
  • finite PAC-Bayes KL/DV/MGF, bounded-loss confidence bounds, and finite-grid peeling wrappers;
  • finite PAC-Bayes Bernstein margin-proxy bounds with a supplied per-hypothesis variance proxy.

Scope and assumptions

The main generalization theorems are intentionally finite and explicit.

  • Hypothesis classes: finite index types unless a theorem states a separate finite net/family
  • Samples: finite iid samples through product measures
  • Losses/processes: scalar real-valued, with boundedness or finite sub-Gaussian MGF assumptions
  • Conditional MGF layer: bounded, conditionally centered real increments with an explicit conditional second-moment proxy
  • Constants: high-probability Rademacher and VC sample-complexity bounds use the sharp McDiarmid 2B² exponent; the localized-Rademacher wrapper still cites the Azuma 8B² constant
  • PAC-Bayes Bernstein layer: finite posterior/prior setting with supplied variance proxy and normalized prior-moment certificate
  • Chaining: finite nets/images, finite support/outcome spaces, finite entropy sums; the unit-interval example instantiates the bridge on a non-finite metric index space with explicit finite meshes
  • Public axiom target: [propext, Classical.choice, Quot.sound] only

Open work

Short version:

  • The main Rademacher and VC results are finite-class and finite-sample theorems.
  • The sharp McDiarmid constant exp(-2t²/∑cᵢ²) is proved for the additive independent case (mcdiarmid_additive_independent), for Doob martingale increments with conditional sub-Gaussian MGF control (sharp_mcdiarmid_of_doob_increments), and for a general bounded-differences function over a homogeneous product measure, one-sided (mcdiarmid_of_hasBoundedDifferences_sharp) and two-sided (mcdiarmid_twoSided_of_hasBoundedDifferences_sharp). The high-probability Rademacher and VC sample-complexity wrappers now use this sharp 2B² exponent; the localized-Rademacher wrapper still uses the older Azuma 8B² constant. The bounded-differences theorem is stated for the same product law in each coordinate, not for arbitrary non-iid product spaces.
  • The chaining layer proves finite entropy-budget infrastructure, finite sum-to-integral comparisons, and finite-covering entropy-integral endpoints. It does not prove a general measurable-supremum theorem over arbitrary non-finite classes.
  • PAC-Bayes includes a finite [0,1] bounded-loss Catoni-style confidence bound, a closed high-confidence good-event theorem, a fixed-budget McAllester-style square-root corollary, a finite-grid peeling wrapper for posterior-dependent penalties, and a finite Bernstein margin-proxy shell with a supplied per-hypothesis variance proxy. Exact all-real-λ, concrete classifier-margin extractors, infinite-hypothesis, and continuous-posterior variants are not yet implemented.
  • Algorithmic stability includes finite iid and measure-theoretic iid expected-gap wrappers, plus bounded-loss high-probability wrappers for finite measurable hypothesis interfaces.

For the full scope statement, see Scope and assumptions.

Installation

This project requires elan, the Lean toolchain manager. elan will read lean-toolchain and fetch the pinned Lean version automatically.

git clone https://github.com/Robby955/FormalSLT.git
cd FormalSLT
lake exe cache get      # download pre-built Mathlib oleans
lake build FormalSLT    # build the library

If lake is not on your shell path, use the elan binary directly:

~/.elan/bin/lake exe cache get
~/.elan/bin/lake build FormalSLT

The first build takes a few minutes (downloading the Mathlib cache); after that, builds are incremental.

Release-candidate checks

Run these before treating a branch as a release candidate:

lake exe cache get
lake build FormalSLT
lake env lean examples/CheckV01Usability.lean
lake env lean examples/CheckSubGammaExtractor.lean
lake env lean examples/CheckUnitIntervalDudley.lean
lake env lean examples/CheckTwoPointDudley.lean
lake env lean examples/CheckFiniteDiscreteDudley.lean
lake env lean examples/CheckPACBayesBernstein.lean
python3 scripts/generate_proof_frontier_manifest.py --check
python3 scripts/check_doc_anchors.py \
  docs/formalslt-v0.1-technical-note.md \
  docs/formalslt-v0.1-artifact-map-2026-06-01.md \
  docs/formalslt-v0.1-release-review-2026-06-01.md \
  docs/theorempath-formalslt-v0.1-page-draft.mdx

Audit commands

Use the release-candidate checks above, then run the proof-debt and whitespace audits:

rg -n --pcre2 '^\s*(?:by\s+)?(?:sorry|admit)\b|:=\s*(?:by\s+)?(?:sorry|admit)\b' FormalSLT examples
rg -n --pcre2 '^\s*(?:axiom|constant)\s+[A-Za-z_]' FormalSLT examples
python3 scripts/generate_proof_frontier_manifest.py --check
python3 scripts/generate_badge_counts.py --check
python3 scripts/check_doc_anchors.py \
  docs/formalslt-v0.1-technical-note.md \
  docs/formalslt-v0.1-artifact-map-2026-06-01.md \
  docs/formalslt-v0.1-release-review-2026-06-01.md \
  docs/theorempath-formalslt-v0.1-page-draft.mdx
git diff --check

The badge counts script regenerates the JSON files under docs/badges/ that the shields.io endpoint badges in this README consume; running it without --check rewrites them after any theorem/module/line-count change.

The expected result is:

  • lake build FormalSLT exits successfully;
  • examples/CheckV01Usability.lean resolves the v0.1 citation targets and prints standard Lean/Mathlib axioms for the bundled confidence-sequence API, the dyadic-net sequence API, and the concrete dyadic-net instances;
  • examples/CheckShowcaseTheorems.lean prints standard Lean/Mathlib axioms for selected public theorems;
  • examples/CheckSubGammaExtractor.lean prints standard Lean/Mathlib axioms for the conditional sub-Gamma extractor and its helper lemmas;
  • examples/CheckUnitIntervalDudley.lean prints standard Lean/Mathlib axioms for the concrete unit-interval Dudley example;
  • examples/CheckTwoPointDudley.lean prints standard Lean/Mathlib axioms for the second dyadic-net example;
  • examples/CheckFiniteDiscreteDudley.lean prints standard Lean/Mathlib axioms for the finite discrete embedded Rademacher dyadic-net family;
  • the rg commands find no executable sorry, no executable admit, and no custom axioms/constants in FormalSLT or examples;
  • the proof-frontier manifest is in sync with the theorem map and source counts;
  • documented FormalSLT/...lean:line anchors point at the named declarations;
  • git diff --check reports no whitespace errors.

Module map

  • Core definitions: Risk, ERM, UniformConvergence, GhostSample
  • Probability utilities: Probability.Concentration, Probability.FiniteUnionBound, Probability.FiniteExpectation
  • Conditional sub-Gamma infrastructure: Concentration.SubGamma.BennettBound, Concentration.SubGamma.BoundedExpIntegrable, Concentration.SubGamma.CondExpProduct, Concentration.SubGamma.CondJensen, Concentration.SubGamma.CondMarkov, Concentration.SubGamma.CondVarianceFromSquare, Concentration.SubGamma.Extractor
  • Rademacher route: Rademacher.FiniteSample, Rademacher.FiniteSampleSymmetrization, Rademacher.ProbabilityBridge, Rademacher.Decoupling, Rademacher.Symmetrization, Rademacher.Massart, Rademacher.HighProbability, Rademacher.FiniteClassHighProb, Rademacher.UniformDeviation, Rademacher.ERMGeneralization, Rademacher.Contraction, Rademacher.LinearPredictor, Rademacher.Localized
  • Azuma infrastructure: Azuma.ExposureMartingale, Azuma.BoundedDifferences, Azuma.BoundedDiffMartingale, Azuma.BoundedDiffsAzumaInput, Azuma.BoundedIncrementBound, Azuma.HasBoundedDifferences, Azuma.ExposureIncrementHoeffding, Azuma.ExposureIncrementCondMGF, Azuma.GenGapTail
  • VC route: VC.Dimension, VC.PACBridge, VC.SauerShelah, VC.Rademacher, VC.SampleComplexity, VC.BinaryVCBridge
  • Covering and chaining: Covering.Rademacher, Covering.DudleyChaining, Covering.FiniteSubGaussianChaining, Covering.TotalBoundedDudley, Covering.UnitIntervalDudley, Covering.TwoPointDudley, Covering.FiniteDiscreteDudley, Covering.DudleyChainingSum, Covering.DudleySumToIntegral, Covering.DudleyEntropyIntegral, Covering.TwoPointDudleyIntegral
  • Sub-Gaussian finite maximal inequalities: Probability.SubGaussianFiniteMax
  • Stability and PAC-Bayes foundations: AlgorithmicStability, Stability.BousquetElisseeff, PACBayesKL, PACBayesMcAllester, PACBayesFiniteProductMGF, PACBayesBoundedLoss, PACBayesBernstein

Roadmap

  • Finite-sample Rademacher definitions
  • Rademacher symmetrization
  • Massart finite-class bound
  • Azuma-Hoeffding genGap tail
  • High-probability Rademacher bound
  • Sauer-Shelah polynomial bound
  • VC-style pointwise Rademacher
  • VC uniform deviation and ERM excess-risk tail
  • VC closed-form ERM sample-complexity theorem
  • Binary-class VC to effective loss-pattern bridge
  • Finite-sample scalar contraction
  • Finite-dimensional linear predictor Rademacher bound
  • Finite localized Rademacher/Bernstein variance-localization scaffold
  • Conditional sub-Gamma MGF extractor from boundedness, conditional centering, and a conditional second-moment proxy
  • Covering number peeling and two-scale chaining
  • Finite sub-Gaussian max and finite chaining entropy budgets
  • Algorithmic stability bounded-differences scaffold
  • Finite algorithmic stability expected-gap adapter under coordinate-swap identity
  • Finite iid coordinate-swap identity and literal expected-generalization-gap specialization
  • Finite iid two-sided algorithmic stability expected-gap wrappers
  • PAC-Bayes KL divergence and Donsker-Varadhan variational inequality
  • PAC-Bayes finite iid product MGF bridge for empirical-risk deviations
  • PAC-Bayes bounded-loss MGF, Markov confidence, and finite Catoni-style bound
  • PAC-Bayes closed high-confidence generalization payoff theorem
  • PAC-Bayes fixed-budget McAllester-style square-root corollary
  • PAC-Bayes finite-grid McAllester peeling and optimized finite-grid wrapper
  • PAC-Bayes finite Bernstein margin-proxy wrapper with supplied variance proxy and normalized prior-moment certificate
  • Finite Dudley discrete entropy-bound refinements: annulus, integral-budget, and prefix-envelope wrappers
  • Total-bounded finite-net extraction bridge for the continuous Dudley lane
  • Projected-sup total-bounded dyadic Dudley wrapper
  • Projected finite-net total-bounded dyadic Dudley wrapper without finite ambient index type
  • Finite dyadic-budget to entropy-at-radius upper-sum comparison
  • Shifted finite-annulus entropy budget collapsed to one truncated interval integral
  • Supplied-supremum boundary adapter with explicit terminal approximation error
  • Finite-skeleton/dense-net boundary adapter with explicit separability and terminal projection errors
  • Pathwise-modulus and finite-skeleton witness lemmas that discharge the continuous-boundary adapter hypotheses
  • Epsilonized finite-choice boundary adapter: every positive error budget can be discharged by a finite skeleton and terminal dyadic scale certificate
  • Finite-cover/pathwise-modulus certificate for the epsilonized total-bounded Dudley boundary layer
  • Dudley boundary epsilon elimination under a uniform global finite-budget hypothesis
  • Separable-terminal Dudley boundary adapter under explicit finite-skeleton and terminal-projection hypotheses
  • Pathwise terminal-modulus constructor for separable-terminal Dudley boundary certificates
  • Finite-cover/pathwise-modulus bridge into the separable-terminal Dudley boundary interface
  • Finite-terminal total-bounded dyadic Dudley wrapper
  • Concrete unit-interval Dudley example with explicit half/quarter meshes and a supplied-supremum projected-mesh bound
  • Continuous Dudley entropy-integral theorem over total-bounded classes
  • Measure-theoretic iid algorithmic stability expected bound, with explicit integrability assumptions
  • Bounded-loss measurability adapters for the measure-theoretic stability expected-gap theorem
  • Bounded-loss high-probability stability wrappers for finite measurable hypothesis interfaces
  • PAC-Bayes concrete margin-loss Bernstein extractor, all-real-λ, or continuous-posterior extensions
  • Sharp McDiarmid constant for the additive independent case and for Doob martingale increments with conditional sub-Gaussian MGF control
  • Sharp McDiarmid for a general bounded-differences function over a homogeneous product measure: one-sided, lower-tail, and two-sided (mcdiarmid_twoSided_of_hasBoundedDifferences_sharp), with the sharp 2B² exponent propagated into the high-probability Rademacher and VC wrappers
  • Sharp McDiarmid over arbitrary non-iid product spaces (different law per coordinate)
  • Continuous Dudley-style entropy integral

Dependencies

Contributing

Contributions are welcome. Please read CONTRIBUTING.md before opening a PR. The short version: one theorem per PR, no sorry / no admit, only the standard [propext, Classical.choice, Quot.sound] axioms, and assumptions stated in the type signature rather than buried in hypotheses.

For ideas, see the open-formalization-problems list, good first issues, and the unchecked items in the roadmap above. Before a public release, maintainers can use the public release checklist.

Citation

If you use FormalSLT in academic work, please cite:

@software{formal_slt,
  title  = {FormalSLT: Formal Statistical Learning Theory in Lean 4},
  author = {Sneiderman, Robert},
  year   = {2026},
  url    = {https://github.com/Robby955/FormalSLT},
  note   = {Lean 4 formalization of finite-sample SLT bounds.}
}

For audit commands that regenerate the badge counts above, see the audit commands section.

License

This project is released under the MIT License.

About

Zero-sorry Lean 4 library: finite-sample SLT bounds, sharp McDiarmid, PAC-Bayes Bernstein margin shell, and Dudley chaining. Standard Lean/Mathlib axioms only.

theorempath.com/theorems/formalslt-v0-1

Topics

machine-learning theorem-proving mathematics statistical-learning formal-verification pac-bayes pac-learning lean4 concentration-inequalities mathlib4

Resources

Readme

License

MIT license

Contributing

Contributing
Activity

Stars

33 stars

Watchers

1 watching

Forks

9 forks
Report repository

Releases

1 tags

Packages

 
 
 

Contributors

Languages