Formalizing the Cholesky factorization theorem

DOI10.4230/LIPICS.ITP.2024.25MaRDI QIDQ6860005zbMATH OpenFDO

Authors Carl Kwan, Warren A. Hunt jun.

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2024.25

zbMATH Keywords

ACL2automated reasoningCholesky factorization theoremmatrix decompositionnumerical linear algebra

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• FLAME
• scientific article; zbMATH DE number 2107836 (Why is no real title available?)
• Integration of multiple formal matrix models in Coq
• Nonstandard analysis in ACL2
• Real vector spaces and the Cauchy-Schwarz inequality in ACL2(r)
• The HOL Light theory of Euclidean space

This page was built for publication: Formalizing the Cholesky factorization theorem

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