Mathematical Conversations

Computer algebra systems are large software systems and as such they have bugs. A recent issue of the Notices of the AMS features the article "The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?" in which the authors discuss a bug which makes Mathematica compute the wrong determinant of some integer matrices. A possible approach for increasing the trust in computer algebra systems is to formalize parts of them in an interactive theorem prover. In the talk I will discuss the formalization of Bareiss algorithm in the Coq proof assistant. This algorithm is a generalization of Gaussian elimination for computing the determinant of matrices over commutative rings in polynomial time. Using this formally verified implementation we have been able to compute the correct determinant of the integer matrices from the AMS article.