[reikonomusha]

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.

[davnn]

The intersection is also interesting when you look at equational proofs in Mathematica.

https://reference.wolfram.com/language/ref/FindEquationalPro...