Archive of Formal Proofs

The formalizations that we have developed are presented in the Archive of Formal Proofs:

• A verified factorization algorithm for integer polynomials with polynomial complexity
• A verified LLL algorithm
• The Factorization Algorithm of Berlekamp and Zassenhaus
• Perron-Frobenius Theorem for Spectral Radius Analysis
• Hermite Normal Form
• Echelon Form
• QR Decomposition
• Gauss-Jordan Algorithm and Its Applications
• Rank-Nullity Theorem in Linear Algebra

Nevertheless, for the sake of completeness some other earlier versions are shown here.

---

Gauss - Jordan 2013-2 - Generalized

This development completes the previous one about the Gauss-Jordan algorithm. Now we have generalized some parts of the HOL-Multivariate Analysis library of Isabelle. Above all, we have carried out four kinds of generalizations:

• Lemmas involving real vector spaces are now generalized to vector spaces over any field.
• Some lemmas involving euclidean spaces have been generalized to finite dimensional vector spaces (since the first time that the notion of a finite basis appeared in the library was in the class euclidean_space).
• Lemmas involving real matrices have been generalized to matrices over any field.
• Lemmas about determinants involving the class linordered_idom, such as the lemma "det_identical_columns". These lemmas are now proven using the class comm_ring_1.

The following facts are formalized and can be computed involving matrices over any field (in the previous development, we had only verified computations over real matrices):

• Ranks
• Determinants
• Inverses
• Bases and dimensions of the null space, left null space, column space and row space of a matrix
• Solutions of systems of linear equations (in any case, including systems with one solution, multiple solutions and with no solution)

Code from this formalisation can be exported to both SML and Haskell. Some benchmarks have been carried out, showing a remarkable efficience (the performance has been improved with respect to the previous version of the development).

• Link to the development

---

Gauss - Jordan 2013-2

This development is based on the previous one about the Gauss-Jordan algorithm, but it has been improved in several ways. Now, the following facts have been formalized and can be computed:

• Ranks
• Determinants
• Inverses
• Bases and dimensions of the null space, left null space, column space and row space of a matrix
• Solutions of systems of linear equations

Code from this formalisation can be exported to both SML and Haskell. Some benchmarks have been carried out, showing a remarkable efficience. Nevertheless, due to some restrictions in the HMA library, some computations are only verified over real matrices.

• Link to the development

---

Gauss - Jordan

In this development is formalized the well-known Gauss-Jordan algorithm, in order to compute the reduce row echelon form of a matrix. It makes use of the HOL-Multivariate-Analysis session of Isabelle and its matrix representation (function over finite types). We have set up the Isabelle code generator to allow the execution of that representation. In addition, we present an alternative verified type refinement (using nested immutable arrays) that outperforms the original version. Thanks to this algorithm and the Rank Nullity Theorem, ranks and dimensions of some fundamental subspaces can be computed.

• Link to the development

---

Other developments

• Diagonal Form
• Degree's Thesis

Links

• ForMath Project