[hvocode]

Not unreasonable at all.

A rough way to think about a tool like Coq or Isabelle is that it provides a very simple core foundation built out of some mathematical logic and mechanisms for manipulating statements in that logic ("if P implies Q, then X"). Proofs end up being sequences of applications of rules that manipulate the statements until you reach some conclusion. People build up theories on top of this core (and other theories), which introduce new mathematical constructs and theorems/lemmas that represent their properties.

A computer algebra system (CAS) tends to have a more complex core because instead of only having some logic as its basis, it might know about higher level constructs like polynomials and such. This allows it to more easily operate on those constructs directly via specialized algorithms and heuristics without having to build up a huge foundation of theories that they live on top of.

That said, you could implement lots of things a CAS does in a theorem prover - it just would probably be pretty awkward to work with, and possibly quite slow. Similarly, lots of CAS tools (like Mathematica and Maple) provide features for doing proofs that are similar to theorem provers. One place I would expect those to differ though is that the small, simple core of a theorem prover allows people to careful verify it such that the theories atop it inherit the verification evidence of the core. I do not know if any such verification evidence exists when it comes to the large kernels that make up tools like Mathematica/Maple.