Symbolic calculations performed manually or by a computer algebra system may be faulty or hold only subject to certain assumptions. A classical example is `sqrt(x^2) == x`

which is not true in general but it does hold if `x`

is real and non-negative.

Are there examples where proof assistants/checkers such as Coq, Isabelle, HOL, Metamath, or others are used to certify correctness of symbolic calculations? In particular, I am interested in calculus and linear algebra examples such as solving definite or indefinite integrals, differential equations, and matrix equations.

**Update:**
To be more concrete, it would be interesting to know whether there are examples of undergraduate assignments in calculus and linear algebra that could be formally solved (possibly with the help of a proof assistant) such that the solution can be automatically verified by a proof checker. A very simple example assignment for Lean is here.