Claim evidence, explained
Last reviewed: April 30, 2026 · Lean manifest 2026-04-28
TheoremPath tracks evidence at the claim level. A proof artifact can support one exact theorem statement; a source can support one specific claim; a diagnostic item can test one prerequisite skill. None of that turns a whole page into a blanket verification badge.
Machine-checked theorems
28
Lean declarations that compile in CI as claim-facing proof artifacts.
Exact claim matches
23
Formal statements whose recorded scope matches the governed claim.
Scoped support proofs
5
Useful bridges toward broader claims, kept separate to avoid overclaiming.
Incomplete proof markers
0
Lean placeholders across these checked entries: sorry=0, admit=0.
Lean is a proof checker. If a theorem compiles, the exact formal statement type-checks against Lean and mathlib.
Exact wrapper means the formal theorem matches the claim scope closely enough to count as claim-level evidence.
Scoped bridge means the proof is real, but it is only a step toward the public theorem. It stays labeled as a step.
These are not marketing badges. Each card says what the theorem means in normal mathematical language, what exact Lean declaration checked it, and whether the proof matches the public claim or only supports part of it.
concentration inequalities
In plain English
A nonnegative random variable with small expectation cannot be large very often.
Why this matters
This is the first tail-bound bridge from averages to probability guarantees.
Exact claim-facing mathlib wrapper for Markov's inequality in real-valued integrable form. The finite weighted-support theorem remains a bridge proof, not the canonical verification target.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
concentration inequalities
In plain English
A bounded finite sum has an exponential one-sided deviation bound under the recorded assumptions.
Why this matters
This is the concentration step behind finite-class generalization arguments.
Exact claim-facing wrapper for the one-sided finite-sum Hoeffding bound for bounded independent real random variables.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
subgaussian random variables
In plain English
A bounded centered random variable has a sub-Gaussian moment-generating-function bound.
Why this matters
This is the standard bridge from bounded variables to Hoeffding-style tails.
Exact mathlib wrapper for Hoeffding's lemma in sub-Gaussian MGF form. Source review now permits claim-level display without implying the whole page is Lean verified.
Checked April 29, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
measure theoretic probability
In plain English
If event probabilities are summable, the limsup event has probability zero in the mathlib formulation.
Why this matters
This turns a previous finite bridge into a direct probability theorem wrapper.
Exact claim-facing mathlib wrapper for the first Borel-Cantelli lemma in limsup-measure-zero form. The finite union-bound artifacts remain supporting bridge proofs, not the source of verification.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
kolmogorov probability axioms
In plain English
The probability of a finite union is at most the sum of the individual probabilities.
Why this matters
This is a foundational tool used throughout concentration and learning theory.
Exact claim-facing wrapper for the finite union bound for probability measures.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
common inequalities
In plain English
The absolute inner product is bounded by the product of the two norms.
Why this matters
This is a reusable inequality across linear algebra, statistics, and optimization.
Exact claim-facing mathlib wrapper for the core Cauchy-Schwarz inequality in real inner product spaces. Equality, probability, and finite-sum variants remain separate explanatory scopes until governed separately.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
vc dimension
In plain English
A finite set family with bounded VC dimension cannot shatter too many subsets.
Why this matters
This is a core combinatorial bridge behind classical learning-theory capacity bounds.
Exact claim-facing mathlib wrapper for the finite set-family Sauer-Shelah binomial-sum bound. The common (em/d)^d analytic estimate is treated as a downstream corollary, not as part of this verified claim.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
uniform convergence
In plain English
The checked artifact is a scoped reduction step toward the finite-class uniform convergence theorem.
Why this matters
It is useful evidence, but it is deliberately not labeled as the full stochastic theorem.
Scoped bridge artifact for finite-class uniform convergence. It proves the risk-facing high-probability reduction from paired one-sided true-risk/empirical-risk deviation tail bounds and a delta-sized finite-class union-bound expression to a simultaneous epsilon-representative failure bound, and now includes fixed-hypothesis empirical-average upper- and lower-tail Hoeffding bridges with explicit sample-size hypotheses; it does not verify iid sampling as the data-generating model or the closed-form sqrt/log sample-complexity display.
Checked April 30, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
Diagnostics should point to the same claim and prerequisite graph. If a learner misses a Hoeffding assumption question, the system should route them toward the bounded-difference or sub-Gaussian claim they actually missed, not simply say “study probability.”
That is why claim IDs, Q-matrix skill links, Lean evidence, and source support need to stay connected. The public page shows the standard; the internal dashboards hold the full review queue.
For the rules behind this page, see methodology. For the theorem list, see key theorems.