Computer algebra systems, formal proofs and interactive theorem proving

Mathematical Conversations
Topic:Computer algebra systems, formal proofs and interactive theorem proving
Speaker:Anders Mörtberg
Affiliation:Member, School of Mathematics
Date:Friday, February 5
Time/Room:6:00pm - 7:00pm/Dilworth Room

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.