# Ten historical methods: source correspondence and prior work

Checked on 2026-09-10. This batch contains 10 independently written Lean files
with 59 advertised theorem statements. These include supporting lemmas; they
are not 59 separate historical discoveries. Each page explains a selected result,
not a complete paper. All mathematical novelty and first-formalization claims
remain **unconfirmed**. A bounded name search cannot find every equivalent theorem.

## What was inspected

The complete tracked `Mathlib/` source tree was searched with `git grep -n -i -E`
at both of these locally available revisions:

- Pinned v4.33.1: `0df444a360eaa60ab8c11dca51a86af692955474`.
- Locally available `origin/master`: `ac7917d6a517b3b710987e9f8037bdcac522a461`.
  This is an inspected revision, not a claim to have inspected every subsequent
  upstream change or open pull request.

The consolidated whole-word pattern was:

```text
\b(Halley|Schulz|Steffensen|Clenshaw|Frisch|Waugh|Kantorovich|Samuelson|Gruss|Grüss|Welford|Jury)\b
```

Neither revision returned a name match. This searches names and documentation,
not mathematical equivalence. Finite sums, Cauchy–Schwarz, bilinear forms,
complex arithmetic, and many stronger general facts already exist in Mathlib.
All ten proofs use that library; their generic ingredients are not new.

Indexed web searches included the following literal queries:

```text
"Halley" "Lean" formalization
"Clenshaw" "Lean" proof
"Clenshaw" "formal verification"
"Clenshaw" "Lean" theorem github
"Frisch Waugh" "Lean"
"Kantorovich inequality" formalization
"Schulz" "inverse" "Lean" formalization
"Schulz" matrix inverse "formalization"
"Welford" "formal" "Lean" OR "Isabelle" OR "Coq"
"Welford" "Isabelle"
"Welford" "formal verification"
"Welford" "Lean" theorem github
"Samuelson" "inequality" "Lean"
"Gruss" "Lean" inequality
"Grüss inequality" "formalization" OR "Isabelle" OR "Lean4"
"Steffensen" "Lean" formalization
"Jury stability" "Lean" OR "Isabelle" formalization
```

Search results did not identify a matching complete named proof for nine of
these scoped results. Welford has explicit related work, described below.
No exhaustive GitHub code search or audit of all Isabelle, Coq, HOL, or Lean
repositories was performed. Unindexed, differently named, private, and
unpublished formalizations may exist. Missing search results are not evidence
of a first-ever proof.

## Related Welford source found

[lutar-lean PR #180](https://github.com/szl-holdings/lutar-lean/pull/180)
was merged on June 4, 2026. Its description discusses a Welford invariant.
The actual source inspected was
[`FrontierWelfordVariance.lean` at af2ed4fd1a5c744fd1f839549afd2180f8a9ce20](https://github.com/szl-holdings/lutar-lean/blob/af2ed4fd1a5c744fd1f839549afd2180f8a9ce20/Lutar/Innovations/round11/FrontierWelfordVariance.lean).

That file defines integer `total`, aliases `weightedMean` to it, and folds
`S + x[n]`. Its three theorems concern this running total. It does not define a
real mean update or a scatter accumulator, or establish that scatter equals
sum of centered squares. We inspected the text, not its compilation in its
original environment. The PR description and filenames alone overstate what
is relevant to our comparison.

Our `Welford.lean` was already independently written before this result was
found. It implements the real mean/scatter recurrence and proves full-list
correctness by moment invariants. The related work is acknowledged on the page;
this narrower difference does not certify novelty or justify saying that
Welford has never been formalized.

## Candidates excluded after finding existing work

- [Sherman–Morrison in Lean](https://zenodo.org/records/18283772), also linked
  to [kaneplusplus/ShermanMorrison](https://github.com/kaneplusplus/ShermanMorrison).
  The published record already describes a formalization; its code was not
  independently compiled here.
- Woodbury identities in Mathlib's `LinearAlgebra/Matrix/Invertible.lean`
  and `LinearAlgebra/Matrix/NonsingularInverse.lean`.
- Gershgorin in `LinearAlgebra/Matrix/Gershgorin.lean`.
- Bhatia–Davis and Popoviciu bounds in `Probability/Moments/Variance.lean`.
  The latter is also a related ingredient of our Grüss proof.
- Neville/Aitken interpolation overlaps Mathlib's
  `LinearAlgebra/Lagrange.lean`, `interpolate_eq_add_interpolate_erase`, and
  the Isabelle AFP [Polynomial Interpolation](https://isa-afp.org/browser_info/current/AFP/Polynomial_Interpolation/document.pdf)
  entry. This is different from the Aitken sequence-transformation artifact
  already on the site.

## Source correspondence and limitations

### Halley (1694)

Original: [DOI 10.1098/rstl.1694.0029](https://doi.org/10.1098/rstl.1694.0029).
We used Walter Gander's [On Halley's Iteration Method (1985)](https://math.unm.edu/~vageli/courses/Ma504/helleysmethod.pdf),
which distinguishes the rational and irrational formulas. Substituting
`f(x) = x² − r²` in the rational formula gives our update. We did not transcribe
the Latin original. The formal scope is exact square-root error identities,
brackets, a cubic bound, and a transformed ratio at every iteration. A general
smooth-function convergence theorem and an explicit limit theorem are absent.

### Schulz (1933)

Original: [Iterative Berechung der reziproken Matrix](https://onlinelibrary.wiley.com/doi/abs/10.1002/zamm.19330130111),
ZAMM 13(1), 57–59. The publisher's title drops the second `n` in `Berechnung`;
the catalog uses the conventional spelling. Original full text was inaccessible.
The update was checked in [Leplat et al. (2025), §3](https://arxiv.org/html/2508.16979v1#S3).
Our proof establishes polynomial residual identities in an arbitrary ring,
including both multiplication orders and arbitrary step counts. It contains
no norm, convergence, spectral initialization, or generalized inverse theorem.

### Steffensen (1933)

Original: [Remarks on iteration](https://doi.org/10.1080/03461238.1933.10419209),
64–72. Original full text was inaccessible. We read the scalar finite-difference
formula in [Zhao, Lai and Lim (2024)](https://galton.uchicago.edu/~lekheng/work/steffensen.pdf).
Our square-root specialization factors the difference exactly, removes a
removable root singularity, proves a safe bracket, and bounds the error
quadratically on a fixed interval. Lean's totalized division makes the raw
formula also return the root at `0/0`; that is not a floating-point prescription.
The page explicitly requires a numerical root check before raw division.

### Clenshaw (1955)

Original: [A note on the summation of Chebyshev series](https://doi.org/10.1090/S0025-5718-1955-0071856-0),
9(51), 118–120. The AMS PDF returned HTTP 403. The backwards recurrence was
checked against [NIST DLMF §3.11(ii), equation 3.11.15](https://dlmf.nist.gov/3.11#ii).
DLMF uses a half-weighted constant coefficient. Our local Chebyshev recurrence
and sum use a full constant coefficient and the readout `b₀ − x b₁`. To use
half-weighted input coefficients, halve the first input coefficient. The file
also proves an invariant for fixed α, β recurrences. It does not claim the
most general index-dependent Clenshaw recurrence or floating-point stability.

### Frisch and Waugh (1933)

Original: [Partial Time Regressions as Compared with Individual Trends](https://doi.org/10.2307/1907330),
Econometrica 1(4), 387–401; bibliography checked in the
[JSTOR issue](https://www.jstor.org/stable/i332559).
The original full text was inaccessible. We read
[Basu's historical and analytical treatment](https://arxiv.org/pdf/2307.00369).
The file models one nuisance direction and one target direction via a symmetric
real bilinear form. Positive sizes of the nuisance and residualized target
make the two penalties positive and give unique minimizing coefficients.
There is no implicit intercept, general nuisance matrix, or covariance estimator.
The paper's history includes Yule's earlier work and Lovell's later extension.

### Grüss (1935)

Original record: [EuDML 168548](https://eudml.org/doc/168548),
Mathematische Zeitschrift 39, 215–226. Its title contains the integral covariance
expression, abbreviated explicitly in our catalog. The bibliography was read;
the original Göttingen scan was not retrieved. We read the opening discrete
setting of [Gonska, Raşa and Rusu (2014)](https://arxiv.org/pdf/1401.7908).
Our theorem is a finite weighted analogue of the integral inequality. We use
Mathlib's finite Cauchy–Schwarz and prove a finite range-variance bound; related
Popoviciu bounds already exist. Neither integration nor the later paper's full
oscillation refinements is included.

### Newman (1960): Kantorovich inequality

[Original two-page NBS paper](https://nvlpubs.nist.gov/nistpubs/jres/64B/jresv64Bn1p33_A1b.pdf)
was read. Its Hermitian matrix setting is reduced to weighted scalar values;
it also gives a broader convex-function inequality. We formalize the finite
weighted scalar Kantorovich bound and the endpoint equality identity. Neither
diagonalization nor the general convex-function argument is formalized. The
volume is 64B (1960); the manuscript submission date is in 1959. This entry is
anchored to Newman, rather than pretending to formalize an unread earlier
Kantorovich paper.

### Welford (1962)

[Publisher record](https://www.tandfonline.com/doi/abs/10.1080/00401706.1962.10490022)
confirms Technometrics 4(3), 419–420. Original full text was inaccessible.
[Tony Finch's 2009 research note](https://fanf2.user.srcf.net/hermes/doc/antiforgery/stats.pdf),
equations (4) and (24), was read to check the mean and scatter updates.
The formalization tracks count, mean and unnormalized scatter over exact reals.
It proves scatter equals the centered squared sum, including for an empty list;
mean correctness requires a nonempty list. The list evaluator processes its
tail first. No floating-point error, weighted recurrence, or covariance-product
extension is proved. See the related Lean work comparison above.

### Jury (1962)

Original: [A Simplified Stability Criterion for Linear Discrete Systems](https://doi.org/10.1109/JRPROC.1962.288193),
Proceedings of the IRE 50(6), 1493–1500. Original full text was inaccessible
(the journal-volume PDF returned HTTP 403). We checked the degree-two conditions
in [Khalsaraei, Shokri and Ramos (2022), Lemma 2](https://gredos.usal.es/bitstream/handle/10366/156346/Khalsaraei%2CShokri%2CRamos-2022-Mathematics%20%28Efficient%20numerical%20solutions%20to%20a%20SIR%20model%29.pdf?sequence=1).
Their `λ² − Aλ + B` corresponds to our `z² + az + b` under `A = −a`, `B = b`.
Our independent proof establishes sufficiency for every complex root, splitting
real and nonreal cases. It does not establish necessity, construct a general
Jury table, or verify any epidemic/control model. The extra lower bound in
`|b| < 1` is redundant given the two positive endpoint evaluations.

### Samuelson (1968)

Original: [How Deviant Can You Be?](https://doi.org/10.1080/01621459.1968.10480944),
JASA 63(324), 1522–1525. Publisher abstract/bibliography were checked; original
full text was inaccessible. We read equation (1.1) of
[Goroncy and Rychlik (2006)](https://files.ele-math.com/articles/mia-09-57.pdf).
Our squared form uses the population variance divisor N and does not divide by
standard deviation. This includes constant data and N = 1. The equality lemma
uses centered values with every nonselected value equal. Simultaneous extremes,
order statistics, probabilistic interpretation and tail estimates are excluded.

## Verification contract

The build compiles every advertised theorem with Lean 4.33.1 and
`-DwarningAsError=true`, then checks each `#print axioms` result against the
catalog. Schulz uses `propext`; Clenshaw uses `propext` and `Quot.sound`;
the remaining eight use those plus `Classical.choice`. No custom axioms,
unfinished proofs, or native-decide certificates are accepted. Each page and
project download includes the original source, audit output, source hash, and
pinned toolchain/dependency configuration.

Kernel checking certifies the written mathematical statements. It cannot
certify the historical correspondence or absence of earlier formalizations.