I am not an expert user of these two kinds of software. I have dabbled with both.

I understand that the trivial difference between proof assistants and CAS is that in proof assistants, the goal is to show that the given proposition reduces to a tautology (or a contradiction as an intermediate step). Whereas CAS are used to perform various transformations on mathematical expressions to find results that are usable elsewhere.

When we are doing mathematics on paper, the techniques used while deriving something are not all that different from the techniques used while proving something. In each case, we start with an expression, and apply one (previously established) rule after another, until we reach our goal. As far as I know, the rules that are applied in derivations are exactly the same as the rules applied while proving something. Looking at it in another way, the human skills honed on derivations are perfectly applicable while performing proofs.

When comparing computer systems, the list of computer algebra systems has no titles in common with the list of proof assistants. From my lay perspective, to name a specific example, I think we can use CAS to derive the roots of a generalized quadratic equation, but only when we have the formula, can we use a proof assistant to verify it.

So, given the vast amount of mathematical knowledge encoded in the libraries of both CAS and proof assistants, why can't we use a CAS to perform proofs, and why can't we use proof assistants for deriving anything beyond tautologies?

I had asked the question at cs.stackexchange.com, but the posted answer did not attend to the core of my question. I'm hoping that the more fundamental difference(s) would be addressed here. For example, if I wanted to create my own proof-of-concept proof assistant, and my own CAS, starting from scratch, let's say, in Python and no additional packages, how would my approach for one be different from the other?

I am not an expert user of these two kinds of software. I have dabbled with both.

I understand that the trivial difference between proof assistants and CAS is that in proof assistants, the goal is to show that the given proposition reduces to a tautology (or a contradiction as an intermediate step). Whereas CAS are used to perform various transformations on mathematical expressions to find results that are usable elsewhere.

When we are doing mathematics on paper, the techniques used while deriving something are not all that different from the techniques used while proving something. In each case, we start with an expression, and apply one (previously established) rule after another, until we reach our goal. As far as I know, the rules that are applied in derivations are exactly the same as the rules applied while proving something. Looking at it in another way, the human skills honed on derivations are perfectly applicable while performing proofs.

When comparing computer systems, the list of computer algebra systems has no titles in common with the list of proof assistants. From my lay perspective, to name a specific example, I think we can use CAS to derive the roots of a generalized quadratic equation, but only when we have the formula, can we use a proof assistant to verify it.

So, given the vast amount of mathematical knowledge encoded in the libraries of both CAS and proof assistants, why can't we use a CAS to perform proofs, and why can't we use proof assistants for deriving anything beyond tautologies? For example, if I wanted to create my own proof-of-concept proof assistant, and my own CAS, starting from scratch, let's say, in Python and no additional packages, how would my approach for one be different from the other?