Computer algebra systems are usually large, heuristic systems for doing algebraic manipulation of symbolic expressions by computer. Roughly, they’re there to ai

Computer algebra systems are usually large, heuristic systems for doing algebraic manipulation of symbolic expressions by computer. Roughly, they’re there to aid a human in doing mechanical algebra by working with symbols and not just numbers. Generally, the results coming out of a CAS are not considered to be “proved correct”, and ought to be verified by the programmer/user. Proof assistants aim to allow one to write down a mathematics assertion in a precise manner, and to help the user write a formally verifiable proof for that theorem. Extremely crudely, a CAS is like a super-powered calculator, while a proof assistant is like a super-powered unit test framework.