# Five numerical methods: sources and prior work

Search date: 2026-09-09. Artifacts: Richardson, Kaczmarz, Hildreth,
Fletcher–Powell (DFP), and Broyden. These are new implementations in this
project of selected classical results, not new mathematical discoveries.

**No matching named formalization was located in this bounded search.
First-formalization status is unconfirmed.** Existing generic projection,
bilinear-form, finite-sum, inequality, and optimization lemmas overlap with
the mathematics used here. A name search cannot exclude equivalent proofs
under different names.

## Source inspection

- Richardson (1911), [original DOI](https://doi.org/10.1098/rsta.1911.0009),
  Philosophical Transactions A 210, 307–357. The original full text was
  inaccessible: the publisher PDF returned HTTP 403 and a public scan mirror
  could not be reached. The modern recurrence was checked in Dick, Goda and
  Yoshiki, [Richardson extrapolation of polynomial lattice rules,
  §2.4](https://arxiv.org/pdf/1707.03989). Our arbitrary-order spectral proof
  specializes to polynomial errors on a geometric grid. It does not establish
  a literal correspondence to a numbered theorem in the 1911 paper, or prove
  the later paper's quadrature results. It covers exact finite expansions,
  not asymptotic remainders.
- Kaczmarz (1937), [English translation and original
  scan](https://faculty.sites.iastate.edu/esweber/files/inline-files/kaczmarz_english_translation_1937.pdf).
  The original uses normalized rows and a left-hand constant term. Our
  nonnormalized formula changes that sign convention consistently. The
  unrelaxed projection is reconstructed; the parameterized relaxation and
  fixed-point characterization are modern extensions. The original's
  convergence argument is not included.
- Hildreth (1957), [publisher record](https://doi.org/10.1002/nav.3800040113),
  Naval Research Logistics Quarterly 4(1), 79–85. Full original text was not
  accessible. We inspected Shimazu, Fukushima and Ibaraki (1993),
  [A successive over-relaxation method for quadratic programming problems
  with interval constraints](https://www.jstage.jst.go.jp/article/jorsj/36/2/36_KJ00001202877/_pdf),
  §2, Algorithm 2.1 and its dual Gauss–Seidel interpretation. Our file proves
  the modern dual coordinate minimization formula and finite-sweep descent.
  It neither proves primal–dual equivalence nor formalizes the later paper's
  relaxation/convergence results. Positive diagonal entries suffice for the
  advertised local and finite-sweep results, even without global convexity.
- Fletcher and Powell (1963), [original
  scan](https://www.stat.uchicago.edu/~lekheng/courses/302/classics/fletcher-powell.pdf),
  equation (7) and §4 on p. 164. The scan was visually checked as well as read
  through extracted text. The form B(x,z) represents xᵀHz and the linear
  functional l(x) represents sᵀx. Our proof completes a square and treats its
  zero case explicitly to prove strict positivity. Positive curvature is an
  explicit hypothesis, not a line-search result silently assumed proved.
- Broyden (1965), [original
  scan](https://www.math.unm.edu/~vageli/courses/Ma576/papers/Broyden_65.pdf),
  §4 Method 1, equations (4.1)–(4.3), p. 581, visually inspected. Our s is
  the whole displacement (the paper's scalar step times its direction).
  The direct update and unchanged orthogonal directions correspond to those
  equations. The Frobenius Pythagorean identity and least-change uniqueness
  are a modern characterization, not a transcription of the paper's later
  spectral-norm error analysis. Rectangular matrices are allowed here.

Historical PDFs are linked, not redistributed. Source matching is an
editorial responsibility; Lean certifies the formal statements only.

## Direct repository searches

Case-insensitive name/comment searches covered the entire Mathlib source at:

- [Pinned v4.33.1](https://github.com/leanprover-community/mathlib4/tree/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib):
  `0df444a360eaa60ab8c11dca51a86af692955474`.
- [Upstream revision inspected](https://github.com/leanprover-community/mathlib4/tree/ac7917d6a517b3b710987e9f8037bdcac522a461/Mathlib):
  `ac7917d6a517b3b710987e9f8037bdcac522a461`.

Expression: `richardson|kaczmarz|broyden|hildreth|davidon|fletcher.?powell`.
Neither tree returned a match. This is not an exhaustive semantic search.

The same names, plus `DFP`, were searched across `.lean` and `.md` files in
fresh shallow clones of:

- [optsuite/optlib](https://github.com/optsuite/optlib/tree/5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3),
  revision `5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3`.
- [AquilaCheung/LEAN-formalization-lineSearchMethods](https://github.com/AquilaCheung/LEAN-formalization-lineSearchMethods/tree/234ad0ada8825abc17bd2b6660deb0a51a660f3d),
  revision `234ad0ada8825abc17bd2b6660deb0a51a660f3d`.

No name matches occurred. These repositories were inspected for discovery,
not compiled or independently audited. They contain related optimization
work; absence of these names does not establish absence of a relevant result.

The primary paper [Formalization of Line Search Methods by
Lean](https://arxiv.org/abs/2606.25412) describes Armijo, Goldstein, Wolfe and
Zoutendijk formalizations. It cites Fletcher–Powell historically; that
citation alone is not evidence of a checked DFP update. We did not select
those already-formalized line-search results as new artifacts.

## Indexed discovery queries

Representative queries actually issued:

```text
"Richardson" "extrapolation" "Lean"
"Richardson extrapolation" "formalization"
"Richardson" site:github.com "lean" extrapolation
"Richardson extrapolation" "Isabelle" OR "Coq" OR "Lean4"
"Kaczmarz" "Lean" "theorem"
"Kaczmarz" site:github.com "lean"
"Kaczmarz" "Isabelle" OR "Coq" formalization
"Broyden" "formalization"
"Broyden" site:github.com Lean
"Broyden" "Isabelle" OR "Coq" formalization
"Hildreth" "Lean" formalization
"Davidon" "Lean" formalization
"Fletcher Powell" "Isabelle" OR "Coq" OR "Lean4"
"DFP" "formalization" "Lean"
```

Many hits were numerical software rather than proof-assistant developments,
or unrelated uses of “Lean,” “DFP,” or the authors' surnames. No matching
checked artifact was located in these results. Native authenticated GitHub
code search, every proof-assistant library, and private/unindexed work were
not searched. Priority is therefore explicitly unconfirmed on each page.

## What was checked locally

All advertised theorems compile with Lean/Mathlib 4.33.1 and
`-DwarningAsError=true`. Each is audited with `#print axioms`; the build rejects
`sorryAx` and any nonstandard axiom. There are 40 new advertised theorems:
Richardson 9, Kaczmarz 9, Hildreth 8, Fletcher–Powell 6, Broyden 8. Generic
Mathlib facts are dependencies, not counted as new project theorems.