A Lean 4 Proof of the Sherman Morrison Theorem
Abstract
A complete formal verification of the Sherman-Morrison theorem in Lean 4 with Mathlib. This theorem provides an efficient formula for computing the inverse of a rank-one update to an invertible matrix, which is fundamental in numerical linear algebra, optimization algorithms, and statistical computing.
Fields of Study & Subjects
Logic
programming
and type systems
Matrix Theory and Algorithms
Mathematics
Computing
and Information Processing
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 17 January 2026