A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem

摘要

In this paper we show how a thoughtful reusing of libraries can provide concise proofs of non-trivial mathematical results. Concretely, we formalise in Isabelle/HOL a proof of the Fundamental Theorem of Linear Algebra for vector spaces over inner product spaces, the Gram-Schmidt process of orthogonalising vectors over , its application to get the decomposition of a matrix, and the least squares approximation of systems of linear equations without solution, in a modest number of lines (ca. 2700). This work intensively reuses previous results, such as the Rank-Nullity theorem and various applications of the Gauss-Jordan algorithm. The formalisation is also accompanied by code generation and refinements that enable the execution of the presented algorithms in Isabelle and SML.