Classical theorems, checked in Lean

Featured · Combinatorial optimization

The Nemhauser–Wolsey–Fisher theorem

Greedy selection has a provable guarantee when additional choices bring diminishing returns. After k choices, it achieves at least 63.2% of the best possible value.

\begin{aligned}f(G_k)&\ge\left[1-\left(1-\frac1k\right)^k\right]f(O)\\&\ge(1-e^{-1})f(O)\end{aligned}

The ground set is finite, $k\ge1$ , and $f$ is normalized ( $f(\varnothing)=0$ ), monotone, and submodular. Each step adds an unchosen element with maximum marginal gain. $O$ is an optimal set with at most $k$ elements. The finite-budget guarantee is stronger: 75% at $k=2$ and about 70.4% at $k=3$ .

The formalization constructs the greedy sequence, proves its feasibility, and establishes the guarantee against every feasible comparator. It also proves that an optimum exists. Once the ground set is exhausted, further steps leave the selection unchanged.

Nemhauser, Wolsey & Fisher · An analysis of approximations for maximizing submodular set functions—I · 1978

The proof dependencies

Five connected modules develop the theorem and its applications. Finite sums, maximum existence, and the real exponential come from the pinned mathlib dependency.

Submodularity
Lattice submodularity, diminishing returns, and the bound on gains from adding a set.
Basic.lean
Greedy selection
A maximum-marginal choice at every step, cardinality feasibility, and nonnegative gains.
Greedy.lean
The approximation theorem
The one-step residual bound, geometric decay, an optimal comparator, and both approximation factors.
Approximation.lean
Coverage objectives
Finite unions with nonnegative weights are normalized, monotone, and submodular.
Coverage.lean
Maximum coverage
Weighted and unweighted approximation guarantees, plus zero-budget and one-budget cases.
Applications.lean

Application: maximum coverage

Choose at most k sets to cover as much total weight as possible. Overlapping items count once. The library proves both approximation factors for arbitrary finite collections and nonnegative item weights, with ordinary set coverage as a special case.

Formal scope and declarations

FrontierTheorems.Submodular.nemhauser_wolsey_fisher

FrontierTheorems.Submodular.weighted_maximum_coverage

The real-valued greedy construction uses classical choice among marginal maximizers. This release provides mathematical proofs, not a runnable optimization package. Zero budget has a separate exact theorem. The result concerns a cardinality constraint; general knapsack and matroid constraints are outside its statement.

Download complete project Prior-art review

What is verified

Lean checks the statements and proofs in the linked files. The release includes examples covering the greedy guarantee and statistical edge cases. The axiom audit covers the public declarations throughout the library and 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-v2.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

Previous release: three statistical inequalities

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

The Nemhauser–Wolsey–Fisher theorem

The proof dependencies

Submodularity

Greedy selection

The approximation theorem

Coverage objectives

Maximum coverage

Application: maximum coverage

What is verified

Samuelson’s inequality

Hammersley–Chapman–Robbins bound

Pearson’s skewness–kurtosis inequality

Reproduce the checks