Computer algebra systems are not as rigorous as many provers. They are not logically sound reasoning systems, but collections of algorithms. We classify soundness problems that occur in computer algebra systems. While many algorithms and their implementations are perfectly trustworthy, the semantics of symbols is often unclear and leads to errors. On the other hand, more robust approaches to interface external reasoners to provers are not always practical because the mathematical depth of proofs algorithms in computer algebra are based on can be enormous.
Our own approach takes both trustworthiness of the overall system and efficiency into account. It relies on using only reliable parts of a computer algebra system, which can be achieved by choosing a suitable library, and deriving specifications for these algorithms from theirliterature.
We design and implement an interface between the prover Isabelle and the computer algebra library Sumit and use it to prove non-trivial theorems from coding theory. This is based on the mechanisation of the algebraic theories of rings and polynomials. Coding theory is an area where proofs do have a substantial amount of computational content. Also, it is realistic to assume that the verification of an encoding or decoding device could be undertaken in, and indeed, be simplified by, such a system.
The reason why semantics of symbols is often unclear in current computer
algebra systems is not mathematical difficulty, but the design of those
systems. For Gaussian elimination we show how the soundness problem can
be fixed by a small extension, and without losing efficiency. This is a
prerequisite for the efficient use of the algorithm in a prover.