The other answers have already worked out the differences between CAS and proof assistants, but I think it's worthwhile to also to look at what's similar. Researchers in CAS also have a notion of theorem proving, which is explained in a recent paper by Sebastian Posur: Some mathematical objects are universal in the sense that if we can prove something for this specific object, it will hold for a larger class of objects as well. The paper gives an example with a specific Q-algebra which can be shown trivial using Gröbner bases. Since this implies that all Q-algebras satisfying a certain relation are trivial, the computation using Gröbner basis techniques have established a simple theorem.

On the other hand, one can embed methods from CAS into theorem provers.

There is nothing fundamental which keeps CAS and theorem provers apart, it is rather a difference in culture which has has led to both communities being largely distinct. Researchers in CAS are interested in devising new fast algorithms which can be used to solve problems of relevance for them and are content with checking correctness of the algorithms manually, whereas the theorem proving community is still mostly catching up with verifying established results. IMO, it would be very fruitful if more exchange between both communities happened, especially since most modern theorem provers are built with constructive type theories allowing one to implement algorithms in the same language that is used to conduct mathematical arguments.

The other answers have already worked out the differences between CAS and proof assistants, but I think it's worthwhile to also to look at what's similar. Researchers in CAS also have a notion of theorem proving, which is explained in a recent paper by Sebastian Posur: Some mathematical objects are universal in the sense that if we can prove something for this specific object, it will hold for a larger class of objects as well. The paper gives an example with a specific Q-algebra which can be shown trivial using Gröbner bases. Since this implies that all Q-algebras satisfying a certain relation are trivial, the computation using Gröbner basis techniques have established a simple theorem.

On the other hand, one can embed methods from CAS into theorem provers.

There is nothing fundamental which keeps CAS and theorem provers apart, it is rather a difference in culture which has has led to both communities being largely distinct. Researchers in CAS are interested in devising new fast algorithms which can be used to solve problems of relevance for them and are content with checking correctness of the algorithms manually, whereas the theorem proving community is still working on the right logical foundation to formalize mathematics. IMO, it would be very fruitful if more exchange between both communities happened, especially since most modern theorem provers are built with constructive type theories allowing one to implement algorithms in the same language that is used to conduct mathematical arguments.