A Unified Framework for Formalizing Matrix Decomposition Proofs

DOI10.48550/arXiv.2607.05874MaRDI QIDQ7283911zbMATH OpenarXivFDO

Authors Wanli Ma, Zichen Wang, Zaiwen Wen

Publication date 7 July 2026

Published in arXiv

Tldr We formalize matrix decompositions uniformly using dependent type theory and provide a Lean 4 framework that supports many decomposition types and strategies, which are assembled into subtype-induction instances.

Full work available at URL https://doi.org/10.48550/arXiv.2607.05874

arXiv classification

math.NA

Cites work

• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• A formalization of the Smith normal form in higher-order logic
• A machine-checked proof of the odd order theorem
• A refinement-based approach to computational algebra in Coq
• Accuracy and Stability of Numerical Algorithms
• Calculating the Singular Values and Pseudo-Inverse of a Matrix
• Computation of Plain Unitary Rotations Transforming a General Matrix to Triangular Form
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Formalized linear algebra over elementary divisor rings in \textsc{Coq}
• Mathematics and the formal turn
• Matrix Analysis
• Matrix Computations
• Numerical Linear Algebra
• Numerical methods for least squares problems
• Packaging Mathematical Structures
• Point-free, set-free concrete linear algebra
• Proof assistants: history, ideas and future
• QR Decomposition
• The calculus of constructions
• The Lean 4 theorem prover and programming language
• The Lean mathematical library
• The Lean mathematical library
• The Lean theorem prover (system description)
• The Schur complement and its applications
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Unitary Triangularization of a Nonsymmetric Matrix
• What is the point of computers? A question for pure mathematicians
• Über die charakteristischen Wurzeln einer linearen Substitution mit einer Anwendung auf die Theorie der Integralgleichungen.

This page was built for publication: A Unified Framework for Formalizing Matrix Decomposition Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7283911)