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

Question

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?

Answer 1

Your question seemingly implies that proof assistants are limited to proving only logical statements, but they are also used to construct interesting objects.

Here are some random picks: Maier-Vietoris sequence in Agda, perfectoid spaces in Lean, Dedekind real numbers in Coq.

Similarly, Computer algebra systems (CAS) can often carry out proofs of logical statements, although they do usually specialize in proving certain specific families of theorems, for example those expressible in the theory of a real closed field. And most of the time they do not let you inspect the proof, you just have to believe them.

As for differences between proof assistants and computer algebra systems, they arise because of different design goals:

• Computer algebra systems are designed to be useful computational tools with emphasis on practicality and speed. They provide support for numerical computations, symbolic manipulation of algebraic expressions, and visualization.

• Proof assistants are designed to be useful verification tools with emphasis on correctness and strict adherence to a chosen formal system. They provide support for mathematical abstraction and expression of new mathematical concepts and ideas.

A typical example is integration. We expect a CAS to have built-in support for symbolic integration that gives useful answers fast – but most people accept the fact that sometimes the answers are wrong. Also, nobody expect a CAS to be able to provide evidence that its answer is correct.

In contrast, a proof assistant has no built-in support whatsoever for integration – it does not even have built-in numbers of any kind. However, the user may define reals, and all sorts of integration (Riemann, Lebesgue, etc.) precisely and correctly. And when you compute an integral in a proof assistant, you will also have in your hands a proof that the result is correct.

Combining computer-algebra systems and proof assistants is an obvious thing to do that could lead to many exciting developments. From the point of view of proof assistants (we are on the "Proof assistants" SE site after all) a huge obstacle to doing so without sacrificing correctness is the ill-defined semantics of computer algebra systems. One is hard pressed to explain the precise mathematical meaning of the manipulations carried out by a CAS. They sort of make sense, and sort of make engineers happy – but that's not good enough for Real Math.

I will let someone else explain why computer algebra systems don't incorporate proof assistants.

Answer 2

A proof assistant is typically built around a trusted kernel which verified formal proofs in a given formal system. This code is designed to be a short as possible, since it must be completely trusted for the system as a whole to be.

The rest of the program is designed to help the user generate proofs which are then accepted by the kernel. Here the code can be arbitrarily long and complicated as bugs will, at worst, produce "proofs" which are rejected by the kernel, notifying the user that the result was not proved, and not lead the program to claim something was proved which wasn't.

A computer algebra system, on the other hand, typically contains a large number of different algorithms for different problems. Each algorithm used in a given calculation must be trusted if the calculation is to be, and so each algorithm should ideally have a proof of correctness, which might be either formal or informal.

So, to write a proof assistant, you could start with a kernel that is powerful enough to support everything you might want to do, check its correctness, and then writing code on top of it that makes it easier to produce proofs in specific situations, whereas to write a computer algebra system you would write code to implement some simple algebraic operations, check its correctness, write code to implement some more complicated ones, check them, and so on.

Answer 3

The other answers have already worked out the differences between CAS and proof assistants, but I think it's worthwhile to also to look at what's similar. Researchers in CAS also have a notion of theorem proving, which is explained in a recent paper by Sebastian Posur: Some mathematical objects are universal in the sense that if we can prove something for this specific object, it will hold for a larger class of objects as well. The paper gives an example with a specific Q-algebra which can be shown trivial using Gröbner bases. Since this implies that all Q-algebras satisfying a certain relation are trivial, the computation using Gröbner basis techniques have established a simple theorem.

On the other hand, one can embed methods from CAS into theorem provers.

There is nothing fundamental which keeps CAS and theorem provers apart, it is rather a difference in culture which has has led to both communities being largely distinct. Researchers in CAS are interested in devising new fast algorithms which can be used to solve problems of relevance for them and are content with checking correctness of the algorithms manually, whereas the theorem proving community is still working on the right logical foundation to formalize mathematics. IMO, it would be very fruitful if more exchange between both communities happened, especially since most modern theorem provers are built with constructive type theories allowing one to implement algorithms in the same language that is used to conduct mathematical arguments.