Is Ihe use of computer algebra technology beneficial for mechanised reasoning in and about mathematical domains? Usually it is assumed that it is. Many works in this area, however, either have little reasoning content, or use symbolic computation only to simplify expressions. In work that has achieved more, the used methods do not scale up. They trust the computer algebra system either too much or too little.
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 their literature.
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.