Formalization of basic linear algebra
Se ha publicado una tesis de máster de razonamiento formalizado en Isabelle/HOL titulada Formalization of basic linear algebra.
Su autor es Bhavisha M. Talsania (de la California State University, San Marcos).
Su resumen es
This thesis discusses the formalization of basic results from linear algebra up to the following theorems, using the computer proof checker Isabelle:
- Theorem 1 (Basis Size Theorem): Suppose that V is a finite dimensional vector space. Then any two bases have the same number of elements.
- Theorem 2 (Basis Characterization Theorem): Suppose that V is a vector space of dimension n. Then any spanning set has at least n elements, and any spanning set with exactly n elements is a basis. In addition, any linearly independent set of vectors has at most n elements, and any set of linearly independent vectors with exactly n elements is a basis.
- Theorem 3 (Rank-Nullity Theorem): Let L : V1 → V2 be a linear map between finite dimensional vector spaces. Then the nullity of L plus the rank of L equals the dimension of V1 : dim(V1 ) = rank(L) + null(L).
Chapter 1 provides a discussion of informal and formal proofs and an introduction to the thesis topic. Chapter 2 provides a brief overview of the proof assistant Isabelle and it’s layout and syntax. Chapter 3 to Chapter 13 go into detail of the formalized proofs done in Isabelle. In Chapter 14, we end with remarks and conclusion of the thesis.