[max_streese]

Could someone explain to me what the difference between a computer algebra system like Symbolics.jl and a theorem prover like Coq is?

Is that more in the nuances or is there a fundamental difference between these two (referring to the terms and not their specific implementations in Symbolics.jl and Coq respectively)?

Or is this question unreasonable to ask in the first place?

[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...

[hvocode]

Not unreasonable at all.

A rough way to think about a tool like Coq or Isabelle is that it provides a very simple core foundation built out of some mathematical logic and mechanisms for manipulating statements in that logic ("if P implies Q, then X"). Proofs end up being sequences of applications of rules that manipulate the statements until you reach some conclusion. People build up theories on top of this core (and other theories), which introduce new mathematical constructs and theorems/lemmas that represent their properties.

A computer algebra system (CAS) tends to have a more complex core because instead of only having some logic as its basis, it might know about higher level constructs like polynomials and such. This allows it to more easily operate on those constructs directly via specialized algorithms and heuristics without having to build up a huge foundation of theories that they live on top of.

That said, you could implement lots of things a CAS does in a theorem prover - it just would probably be pretty awkward to work with, and possibly quite slow. Similarly, lots of CAS tools (like Mathematica and Maple) provide features for doing proofs that are similar to theorem provers. One place I would expect those to differ though is that the small, simple core of a theorem prover allows people to careful verify it such that the theories atop it inherit the verification evidence of the core. I do not know if any such verification evidence exists when it comes to the large kernels that make up tools like Mathematica/Maple.