Author here. I'm only talking about using formalizable and mathematically consistent type definitions in a CAS, not requiring formal proofs in the implementations of types.
For example, if you want to prove a+b+c+d=d+b+c+a, you will define a, b, c, d as elements of a type R implementing the "additive abelian group" interface (or an extension of this interface, like "ring"); R = integers, for example. The CAS can then use builtin techniques for abelian additive groups to prove the property efficiently. It will not have to prove those properties from first principles.
In the distant future there could perhaps be some kind of convergence between CASes and proof assistants to completely rule out implementation errors, but this would require breakthroughs in proof automation for the reason you mentioned.
For example, if you want to prove a+b+c+d=d+b+c+a, you will define a, b, c, d as elements of a type R implementing the "additive abelian group" interface (or an extension of this interface, like "ring"); R = integers, for example. The CAS can then use builtin techniques for abelian additive groups to prove the property efficiently. It will not have to prove those properties from first principles.
In the distant future there could perhaps be some kind of convergence between CASes and proof assistants to completely rule out implementation errors, but this would require breakthroughs in proof automation for the reason you mentioned.