A small Lean 4 / mathlib development that proves the mathematical claims a statistical control battery relies on, instead of asserting them.
The motivation is narrow and, I think, fair: a methodology that tells other people measured, not believed should not itself rest on inequalities quoted from memory. Each claim below is stated in Lean and checked by the kernel.
sidak_le_bonferroni — Bonferroni is never less conservative than Šidák:
∀ (p : ℝ), p ≤ 2 → ∀ (K : ℕ), 1 - (1 - p) ^ K ≤ K * p
For a per-comparison significance level p and K comparisons, the Šidák
family-wise level 1 - (1 - p)^K never exceeds the Bonferroni bound K * p. The
practical consequence is the one a practitioner actually needs: a result that
survives a Bonferroni correction survives a Šidák correction too, so using the
blunter instrument can cost power but can never falsely license a finding.
bonferroni_union_bound — and Bonferroni holds under arbitrary dependence:
if every one of K events has probability ≤ p, then P(⋃ Aᵢ) ≤ K · p
No independence hypothesis appears anywhere in it, because the union bound does not
need one. Šidák's (1-p)^K does. Since Šidák is always the smaller correction, it is
the less conservative of the two — so it is precisely the one that can be too
permissive exactly when its independence assumption fails. Per-subset results on a
single benchmark are not independent: the same model is scored throughout.
expected_false_positives_le — the other question a practitioner asks:
E[ number of the K events that occur ] ≤ K · p
The union bound answers "will any of them fire?"; this answers "how many should I expect?", and is the second, independent justification for the Bonferroni correction. It also needs no independence — expectation is linear regardless.
Supporting facts, also checked: the Šidák level is a genuine probability
(sidak_nonneg, sidak_le_one on 0 ≤ p ≤ 1).
The proof is Bernoulli's inequality (one_add_mul_le_pow in mathlib) and nothing
else. The p ≤ 2 hypothesis is not decoration — the inequality genuinely fails
above it, which was confirmed numerically before the proof was attempted.
Proving sidak_le_bonferroni needed Bernoulli's inequality in its 1 - a form, which
mathlib did not have — it carries one_add_mul_le_pow and one reformulation of it, but
not the mirror. That gap is now offered back:
leanprover-community/mathlib4#42446
adds one_sub_mul_le_pow. If it lands, the proof here reduces to a single application
of it.
It isn't there. As of mathlib v4.32.2 a search for sidak, bonferroni,
familywise or multiple compar returns nothing statistical. The
measure-theoretic union bound (measure_iUnion_le) exists, but the
multiple-comparison corrections built on top of it do not.
lake exe cache get # mathlib build cache, ~7 GB
lake build
A successful build is not the entire claim, and that is worth being explicit about:
lake build goes green on a development whose theorems are all proved by sorry,
because sorry emits a warning rather than an error. So CI runs a second step:
bash scripts/axiom_check.sh
which fails if any result depends on sorryAx, if a literal sorry appears in the
sources, or if the audit produces no output at all — an empty measurement otherwise
reads as a pass. Before trusting a pass it runs the same check against a deliberately
planted sorry and requires that run to be rejected, because a gate never observed
rejecting anything is decoration.
It also checks its own coverage. The audit lists theorems by name, so a new result could be added to the development and simply never audited, while CI went on reporting success — the same silent failure the audit exists to catch, one level up. The script therefore diffs the theorems declared in the sources against the ones audited and fails, naming them, if any are missing.
Every result currently depends on exactly [propext, Classical.choice, Quot.sound],
the three standard mathlib axioms.
Early. This is one file. The intent is to keep adding the battery's load-bearing claims as they get used: the union bound in the form practitioners state it, the relationship between per-comparison and family-wise error, and the conditions under which a "corrected" p-value means what it is taken to mean.
Corrections especially welcome. If a statement here is wrong, the compiler is the referee.