There's a difference in the kind of things that proof assistants like Coq can do and what computer algebra systems like Sage can do. One can still use CAS like

There's a difference in the kind of things that proof assistants like Coq can do and what computer algebra systems like Sage can do. One can still use CAS like Sage to prove things and not just do numerical computations, but it's a bit of a different approach