Every governed claim on this site that has a checked Lean declaration behind it. Each row links to the claim on its topic page and names the Lean declaration that was checked. A claim with no Lean declaration is not listed here. The evidence page carries the queue of formal claims still waiting for one.
The two status labels are the manifest's own distinction. Formalized means the checked Lean statement covers the claim as the topic page states it. Dependency formalized means it covers a stated part of the claim. The manifest records how it falls short for 20 of those 28 entries, and the row prints it. For the other 8 it records no shortfall in prose, and the row says so and names what was checked instead; an unrecorded gap is not a record that nothing is missing.
Read from data/verification/lean-manifest.json, version 2026-05-07, generated May 7, 2026. Counts are as of that date. The Lean dashboard carries the same entries with their toolchain pins and their public statement-source mapping class.
Two claims have a page of their own, with the exact statement, the proof scope, and the dependencies laid out.
Sharp McDiarmid, two-sided iid product, downstream constant propagation, and a finite PAC-Bayes Bernstein margin shell, checked on public FormalSLT main.
The claim with its Lean declaration, assumptions, dependencies, and diagnostic links on one page.
TheoremPath.LearningTheory.AlgorithmicStability.expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct
Scope gap. The Lean wrapper proves the finite one-sided expected bound E_S[R(A(S)) - Rhat_S(A(S))] <= beta. The page theorem also discusses an absolute-value expected form and a high-probability Bousquet-Elisseeff concentration bound, which remain outside this Lean entry.
TheoremPath.Statistics.AsymptoticStatistics.continuousMappingTheoremContinuous
Scope gap. Does not cover continuity only on a limit-a.s. set, convergence in probability variants, or almost-sure variants.
TheoremPath.Statistics.AsymptoticStatistics.slutskyTheoremPair
Scope gap. Mathlib requires Y_n to take values in a SeminormedAddCommGroup with SecondCountableTopology and BorelSpace. The product and ratio corollaries are reachable via slutskyTheoremContinuous but are not themselves wrapped as named theorems.
TheoremPath.LinearAlgebra.CommonInequalities.cauchySchwarzRealInner
TheoremPath.LinearAlgebra.CommonInequalities.jensenIntegralAverageConvex
TheoremPath.Probability.Concentration.markovInequalityRealIntegrable
TheoremPath.Probability.Concentration.chebyshevInequalityVariance
TheoremPath.Probability.Concentration.subGaussianFiniteSumTailBound
TheoremPath.Probability.Concentration.hoeffdingBoundedFiniteSumTail
TheoremPath.LearningTheory.ERMGeneralization.finiteClass_hoeffding_exactERM_excessRisk_tail
Scope gap. The manifest records none in prose. The checked statement is scoped to tail_bound_population_oracle_excess_risk_in_terms_of_hoeffding_sample_complexity.
TheoremPath.LearningTheory.ERMGeneralization.finiteClass_hoeffding_approxERM_excessRisk_tail
Scope gap. The manifest records none in prose. The checked statement is scoped to tail_bound_excess_risk_with_explicit_optimization_error_term.
TheoremPath.LearningTheory.VCSampleComplexity.vc_erm_excessRisk_tail
Scope gap. Azuma constant (8B² not 2B²). Binary VC bridge now closed for 0-1 loss. No contraction. No infinite classes.
TheoremPath.Probability.FiniteExpectation.linearityOfExpectationIntegrable
TheoremPath.Probability.Moments.varianceOfFiniteSumWithCovariance
TheoremPath.Probability.Moments.lawOfTotalVariance
TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureBasicIdentities
TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureFiniteAdditivity
TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureCountableAdditivity
TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureComplementRule
TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureFiniteUnionBound
TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureCountableUnionBound
TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureContinuityFromBelow
TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureContinuityFromAbove
TheoremPath.Probability.LawOfLargeNumbers.strongLawAverageTendstoAlmostSure
TheoremPath.Probability.LawOfLargeNumbers.weakLawAverageTendstoInMeasure
TheoremPath.Probability.Concentration.azumaHoeffdingConditionalSubGaussianTail
Scope gap. The manifest records none in prose. The checked statement is scoped to finite_martingale_difference_conditional_subgaussian_one_sided_tail.
TheoremPath.Probability.Martingale.doobWeakMaximalInequality
TheoremPath.Probability.BorelCantelli.borelCantelliFirstLimsupMeasureZero
TheoremPath.Probability.BorelCantelli.borelCantelliSecondIndependentLimsupMeasureOne
Scope gap. The governed claim records pairwise independence as sufficient; this wrapper proves the stronger mathlib iIndepSet version only.
TheoremPath.Probability.MeasureConvergence.monotoneConvergenceLIntegral
TheoremPath.Probability.MeasureConvergence.fatouLemmaLIntegral
TheoremPath.Probability.MeasureConvergence.dominatedConvergenceIntegral
TheoremPath.LearningTheory.PACBayesKL.klDiv_nonneg
Scope gap. Finite PMFs only. Does not prove continuous-measure KL nonnegativity or a sample-dependent PAC-Bayes bound.
TheoremPath.LearningTheory.PACBayesKL.donsker_varadhan
Scope gap. Finite PMFs and a real-valued function on the finite hypothesis index. The finite bounded-loss confidence theorem is separate; continuous posterior spaces remain outside this claim.
TheoremPath.LearningTheory.PACBayesKL.posterior_generalization_gap_change_of_measure
Scope gap. Finite PMFs and deterministic finite risk vectors only. Does not introduce an iid sample measure, an exponential-moment bound, or a confidence parameter.
TheoremPath.LearningTheory.PACBayesKL.posterior_risk_le_empiricalRisk_plus_of_log_moment_bound
Scope gap. Finite PMFs, positive lambda, deterministic risk vectors, and an external log-moment bound only. The bounded-loss confidence theorem supplies one finite iid instantiation; continuous posterior and optimized square-root forms remain separate.
TheoremPath.LearningTheory.PACBayesKL.priorExpMoment_tailMass_le_delta_of_expected_bound
Scope gap. Finite sample PMFs and finite hypothesis PMFs only. The bounded-loss confidence theorem supplies one finite iid instantiation; this adapter is not itself the full PAC-Bayes theorem.
TheoremPath.LearningTheory.PACBayesBoundedLoss.finiteCatoni_badEventMass_le_delta
Scope gap. Finite data domain, finite nonempty hypothesis index, finite prior/posterior PMFs, scalar [0,1] losses, positive n/lambda/delta, and fixed lambda only. The fixed-budget and finite-grid square-root corollaries are separate finite claims; continuous posterior PAC-Bayes and infinite hypothesis classes remain outside this claim.
TheoremPath.LearningTheory.PACBayesBoundedLoss.finiteMcAllesterBoundedComplexity_badEventMass_le_delta
Scope gap. Finite data domain, finite nonempty hypothesis index, finite prior/posterior PMFs, scalar [0,1] losses, positive n/delta, and one fixed positive complexity budget C. The finite-grid theorem removes the single-budget restriction under an explicit grid-cover certificate; continuous posteriors and infinite hypothesis classes remain outside this claim.
TheoremPath.LearningTheory.PACBayesBoundedLoss.finiteMcAllesterGridOptimized_badEventMass_le_delta
Scope gap. Finite data domain, finite nonempty hypothesis index, finite prior/posterior PMFs, scalar [0,1] losses, positive n and grid confidence allocations, and an explicit finite grid-cover certificate. Does not prove continuous posterior PAC-Bayes, infinite hypothesis classes, or all-real-lambda optimization.
TheoremPath.LearningTheory.HighProbRademacher.genGap_highProb_rademacher
Scope gap. Lean formalization proves the one-sided genGap bound with Azuma constant (factor-of-4 looser than sharp McDiarmid). The governed page claim states the full two-sided uniformDeviation form with sharp McDiarmid constant and confidence-delta parametrization. The Lean result is a strict subset of the page claim.
TheoremPath.LearningTheory.VCRademacher.empiricalRademacherComplexity_le_massart_effective
Scope gap. The manifest records none in prose. The checked statement is scoped to empirical_rademacher_bounded_by_sqrt_two_log_effective_class_over_n.
TheoremPath.LearningTheory.VCSampleComplexity.vcRademacher_pointwise
Scope gap. User supplies the effective-growth assumption for generic losses. For binary classifiers with 0-1 loss, the bridge is closed (BinaryVCBridge.lean).
TheoremPath.LearningTheory.RademacherContraction.empiricalRademacherComplexity_contraction_lipschitz
Scope gap. Finite sample, finite nonempty hypothesis class, scalar outputs only; not full general Talagrand contraction.
TheoremPath.LearningTheory.LinearPredictorRademacher.linearPredictor_rademacher
Scope gap. Finite sample, finite nonempty indexed weight family, finite-dimensional Euclidean feature space only.
TheoremPath.LearningTheory.RademacherContraction.contraction_empirical
Scope gap. This is the 1-Lipschitz empirical wrapper. It does not by itself prove all scaled L-Lipschitz variants or infinite-class measurable-supremum statements.
TheoremPath.Probability.Concentration.subGaussianIndependentFiniteLinearCombinationMGF
Scope gap. The manifest records none in prose. The checked statement is scoped to finite_independent_linear_combination_mgf_parameter.
TheoremPath.Probability.Concentration.subGaussianMGFImpliesRightTailBound
TheoremPath.Probability.Concentration.hoeffdingLemmaBoundedCenteredSubgaussianMGF
TheoremPath.LearningTheory.RademacherSymmetrization.expected_genGap_le_two_expected_empiricalRademacherComplexity
Scope gap. The manifest records none in prose. The checked statement is scoped to expected_genGap_bounded_by_two_times_expected_empirical_rademacher_complexity.
TheoremPath.Statistics.Rademacher.oneSampleFiniteClassSymmetrization
Scope gap. The manifest records none in prose. The checked statement is scoped to single_shared_rademacher_sign_finite_iota_supremum_bound.
TheoremPath.LearningTheory.UniformConvergence.epsilonRepresentativeERMWorks
TheoremPath.LearningTheory.UniformConvergence.finiteClassEpsilonRepresentativeHighProbabilityFromOneSidedTails
Scope gap. The manifest records none in prose. The checked statement is scoped to finite_class_epsilon_representative_failure_probability_from_one_sided_risk_deviation_tails.
TheoremPath.LearningTheory.VCSampleComplexity.uniformDeviation_highProb_vcClass
Scope gap. Azuma constant (8B² not 2B²). Binary VC bridge now closed for 0-1 loss. Generic losses still need user-supplied growth.
TheoremPath.LearningTheory.VCDimension.sauerShelahFiniteSetFamily
TheoremPath.LearningTheory.BinaryVCBridge.effectiveClass_zeroOneLoss_card_eq_binaryClassTrace
Scope gap. Binary classifiers with 0-1 loss only. Does not cover real-valued loss or multi-class. No contraction. The Lean sample is unlabeled and the loss is 1[h(x) ≠ true], so the machine-checked result is the fixed-label instance of the page statement. The general labeled-sample statement on the page is proved on paper, not in Lean.
These claims are stated on the site and supported by source review. They are recorded as deferrals rather than as Lean targets, because what is checked today covers less than the claim says.
Existing Lean artifacts cover scoped finite-class, VC-growth, ERM, and binary 0-1-loss bridge components, not the full equivalence theorem or infinite-class PAC framework.
This is a random-matrix covariance-shrinkage theorem involving asymptotic spectral behavior and population/sample covariance structure. Existing Lean artifacts do not cover the required matrix-probability, spectral-limit, or covariance-risk framework.
This read-only trail slice carries reviewed textbook locators but no Cramer-Rao Lean file. A narrower finite covariance-identity Lean wrapper must land with its actual Lean artifact before the claim can re-enter the Lean manifest.