A short introduction
What does a proof
actually establish?
Formal verification checks a precise claim against a mathematical model or specification. The choice of claim matters as much as the proof.
The same p-value, a different claim
Suppose an analysis declares one family of six comparisons. A later reporting step splits those results into two groups of three.
If that step recomputes Bonferroni corrections separately for each group, it changes the procedure. A raw p-value of 0.012 now receives a different adjustment.
Synthetic statistical example · Bonferroni adjustment
A report split can change the claim.
Six comparisons belong to one declared family. Two display groups should not silently become two new correction families.
Group the display only
Each report group keeps family F and the adjustment based on all six comparisons.
Recompute within each group
Using three comparisons for each correction changes the family attached to the result.
Composition obligation: the reporting stage must preserve the correction stage’s declared family and result bindings.
Inspect all six values and the rule
Bonferroni adjusted p-value = min(1, raw p-value × family size).
| Comparison | Raw p | Family of 6 | Family of 3 |
|---|---|---|---|
| H1 | 0.012 | 0.072 | 0.036 |
| H2 | 0.020 | 0.120 | 0.060 |
| H3 | 0.040 | 0.240 | 0.120 |
| H4 | 0.008 | 0.048 | 0.024 |
| H5 | 0.030 | 0.180 | 0.090 |
| H6 | 0.200 | 1.000 | 0.600 |
A different family can answer a different question. It needs an explicit rationale beyond how a report is grouped.
Hypothetical values, not study findings or a performance guarantee. Preserving a correction does not establish valid p-values or a suitable study design. Method reference: R’s p.adjust documentation.
The groups may be useful for presentation. They do not, by themselves, justify redefining the original family of claims.
A different family can be a legitimate choice for a different question. That choice needs to be explicit.
A possible contract
Every reported adjustment retains the membership and identity of the declared comparison family.
Splitting a report must not silently change the family used by the correction.
Four kinds of evidence
- Test
- Split a six-comparison example into report groups and check that its original correction is retained. This covers the cases tested.
- Runtime check
- Check family identifiers, membership and result binding during a run. Its coverage depends on the recorded information being complete.
- Proof
- Show that a formalized transformation preserves the declared family and its correction, for all inputs covered by its assumptions.
- Scientific assumption
- Assess whether the p-values are valid for the study design and model, and whether the chosen family answers the intended question. The transformation proof does not establish this.
The model is not automatically the program
A proof about a transformation model does not, by itself, verify the Python or R code that researchers run.
Connecting the two requires evidence: for example, verified implementation code, a checked translation, or a narrower interface with explicit assumptions.
Floating-point arithmetic, libraries, parsers, compilers, proof-checker axioms and hardware may sit inside the trusted boundary. That boundary must be stated.
Human review also remains essential. A proof checker can accept a precise specification that expresses the wrong scientific intention.
Other boundaries worth making explicit
What does a positive effect mean?
A contrast may mean treatment minus reference in one step and the reverse in another. Carrying the contrast definition can preserve meaning across transformations.
When is cached preprocessing still valid?
If gene selection depends on group labels, reusing that selection after permuting the labels may change the intended test. The required recomputation follows from the test’s definition.
A declared dependency rule can make this cache boundary explicit. It cannot establish whether the label permutations are scientifically justified.
Neither example proves an empirical model or a biological interpretation. Both offer precise computational questions that can be examined.
More precise guarantees, within a stated scope
The aim is to attach evidence to individual claims, then understand how those claims compose. Read how we approach that work.
Background: Lean’s proof-checking approach , R’s multiple-comparison adjustments, and SciPy’s permutation-test definitions. The scenarios above are illustrative.