Classical theorems, checked in Lean

What is verified

Lean checks the statements and proofs in the linked files. The release includes tests for singleton samples, sharp bounds, zero variance, and zero-probability outcomes. The axiom audit permits only Lean’s standard foundational axioms.

These are formalizations of established results. The probability statements cover arbitrary finite distributions. They do not assert the unrestricted measure-theoretic versions.

The September 5, 2026 search found no matching theorem in the inspected mathlib and StatLean revisions or the recorded public code searches. This is a scoped search result; worldwide priority is not established. Read the prior-art report.

Lean 4 · Finite statistics

Samuelson’s inequality

(x_j-\bar{x})^2\le(n-1)v

For every observation in a nonempty finite real sample, $\bar{x}=\frac1n\sum_i x_i$ and $v=\frac1n\sum_i(x_i-\bar{x})^2$ . The proof includes the square-root form and the one-observation case.

A sharp limit on how far one observation can lie from the mean. No distributional assumption is required. Variance uses the population divisor n.

Samuelson · How Deviant Can You Be? · 1968

Lean declaration

FrontierTheorems.Samuelson.sq_deviation_le

Download .lean Read proof on GitHub

Lean 4 · Finite statistics

Hammersley–Chapman–Robbins bound

\frac{(\eta-\theta)^2}{\chi^2(q\Vert p)}\le\operatorname{Var}_p(T)

For probability masses $p,q$ on any finite sample space, $q_i=0$ whenever $p_i=0$ , and positive $\chi^2(q\Vert p)=\sum_i(q_i-p_i)^2/p_i$ . The estimator satisfies $\mathbb{E}_pT=\theta$ and $\mathbb{E}_qT=\eta$ . Zero-mass summands are zero.

A lower bound on an unbiased estimator’s variance without likelihood derivatives. The accompanying expectation-shift theorem also covers zero divergence. This is the finite two-point bound.

Chapman & Robbins · Minimum Variance Estimation Without Regularity Assumptions · 1951

Lean declaration

FrontierTheorems.HCR.lower_bound

Download .lean Read proof on GitHub

Lean 4 · Finite statistics

Pearson’s skewness–kurtosis inequality

m_3^2+m_2^3\le m_2m_4

For any finite probability distribution, $m_k=\sum_i p_i(x_i-\mu)^k$ and $\mu=\sum_i p_ix_i$ . The polynomial statement includes zero variance. For $m_2>0$ , the proof also gives $m_3^2/m_2^3+1\le m_4/m_2^2$ .

A constraint on possible combinations of skewness and kurtosis. It applies to weighted data and finite distribution models. Kurtosis here is the fourth standardized moment, not excess kurtosis.

Pearson · Mathematical Contributions to the Theory of Evolution XIX · 1916

Lean declaration

FrontierTheorems.Pearson.central_moment_inequality

Download .lean Read proof on GitHub

Reproduce the checks

Install elan, download and extract the project, then run:

cd mathfrontier-lean-v1.0.0
lake exe cache get
./scripts/verify.sh

The release pins Lean 4.30.0-rc2 and mathlib commit 5450b53e5ddc. The archive includes the dependency manifest, examples, verification script, and license.

Build and axiom audit · Download checksums · GitHub build history

Original code and documentation are available under the MIT license. Mathlib and cited papers retain their own licenses.