Non-trivial difference(s) between Computer Algebra System and Proof Assistant
There are two major differences: CAS and proof assistant tend to focus on different application domains, and they tend to take a different position on correctness vs ease of deriving results.
Most CAS focus on scientific calculations: calculations that are useful to physicists, to chemists, to mechanical engineers, to roboticists, etc. Proof assistants tend to focus on mathematics, computer science and software engineering.
In a proof assistant, it is crucial that you can only derive true propositions. That's the whole point. In contrast, CAS usually have hidden assumptions. For example, you might derive equations that are only true if one of the variables is nonzero, or if some intermediate result is nonnegative. These assumptions are not always explicit. When modelling a real-world problem, these assumptions are usually justified by the physics – if T is a temperature, there's no point in wondering what the equations would look like for T &lt; 0 K.
Some systems can be classified as both CAS and proof assistants because they make all such assumptions explicit.
There's a good reason why CAS take shortcuts: it makes them easier to use for their application domain. When you work in a proof assistant, you often spend a lot of effort directing the computer to the &quot;interesting&quot; path. You have to figure out that at this step, x&gt;=3, so you guide the proof by telling the proof assistant to consider the cases x&lt;3 and x&gt;=3 separately, then you repeat with y+z&gt;x, and so on. A proof assistant gives results that are true for all inputs, but the cost of that is that you have to make the proof work for all inputs. A CAS can give results for general inputs, which is generally good enough for physics and physical engineering (basically, anywhere that's modelled by continuous mathematics – as opposed to software engineering which is typically modelled by discrete maths and there's no such thing as general inputs).