Your question seemingly implies that proof assistants are limited to proving only logical statements, but they are also used to construct interesting objects (here.
Here are some random picks: Maier-Vietoris sequence in Agda, perfectoid spaces in Lean, Dedekind real numbers in Coq).
Similarly, Computer algebra systems (CAS) can often carry out proofs of logical statements, although they do usually specialize in proving certain specific families of theorems, for example those expressible in the theory of a real closed field. And most of the time they do not let you inspect the proof, you just have to believe them.
As for differences between proof assistants and computer algebra systems, they arise because of different design goals:
Computer algebra systems are designed to be useful computational tools with emphasis on practicality and speed. They provide support for numerical computations, symbolic manipulation of algebraic expressions, and visualization.
Proof assistants are designed to be useful verification tools with emphasis on correctness and strict adherence to a chosen formal system. They provide support for mathematical abstraction and expression of new mathematical concepts and ideas.
A typical example is integration. We expect a CAS to have built-in support for symbolic integration that gives useful answers fast – but most people accept the fact that sometimes the answers are wrong. Also, nobody expect a CAS to be able to provide evidence that its answer is correct.
In contrast, a proof assistant has no built-in support whatsoever for integration – it does not even have built-in numbers of any kind. However, the user may define reals, and all sorts of integration (Riemann, Lebesgue, etc.) precisely and correctly. And when you compute an integral in a proof assistant, you will also have in your hands a proof that the result is correct.
Combining computer-algebra systems and proof assistants is an obvious thing to do that could lead to many exciting developments. From the point of view of proof assistants (we are on the "Proof assistants" SE site after all) a huge obstacle to doing so without sacrificing correctness is the ill-defined semantics of computer algebra systems. One is hard pressed to explain the precise mathematical meaning of the manipulations carried out by a CAS. They sort of make sense, and sort of make engineers happy – but that's not good enough for Real Math.
I will let someone else explain why computer algebra systems don't incorporate proof assistants.
