Non-trivial difference(s) between Computer Algebra System and Proof Assistant

Question

Disclaimer: I am not even an expert user of these two kinds of software.

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. Whereas CAS are used to perform various transformations on mathematical expressions to find results that are useful.

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?

Answer 1

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 < 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 "interesting" path. You have to figure out that at this step, x>=3, so you guide the proof by telling the proof assistant to consider the cases x<3 and x>=3 separately, then you repeat with y+z>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).