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.
For the Coq proof assistant there are several libraries to help with that. One matching your request quite well is Coquelicot (https://gitlab.inria.fr/coquelicot/coquelicot). The Coquelicot team made an exercise and participated in the French baccalauréat - I would say comparable more to a college than a high school math exam - and finished proofs for a good part of the exercises. The proofs can be found in the examples here (https://gitlab.inria.fr/coquelicot/coquelicot/-/tree/master/examples). I thought about translating the exercises and solutions to English.
But this was quite a few years ago and meanwhile there are very powerful tools for specific applications. E.g. there is coq-interval (https://gitlab.inria.fr/coqinterval/interval) which fully automatically does Coq proofs of rather complicated inequalities, say that a high order polynomial matches a sine function in a certain interval with a certain maximum deviation. It does this by Taylor decomposition and computing upper bounds for the residual. It can also do error proofs for a wide range of numerical integrals. A new feature added recently is the ability to do proven correct plots.
A tool for proving in Coq the error between infinite precision real and floating point computations is Gappa (https://gitlab.inria.fr/gappa/gappa).
Another very interesting Coq development is CoRN (https://github.com/coq-community/corn), a formalization of constructive reals in Coq. Constructive Reals are true real numbers which do compute. Essentially a constructive real number is an algorithm to compute a number to any desired precision together with a proof that this algorithm converges. One can prove that such numbers fulfill all usual properties of real numbers. An interesting side effect of constructive reals is that they need only LPO as axiom, while in classical reals the existence of the real numbers itself is an axiom. Any computation you do in CoRN, say pi>3, is automatically proven correct.
All these tools are included in Coq Platform, a common distribution of the Coq proof assistant.
There is more and this is steadily increasing. I would say it is not that far in the future that we have a usable proven correct CAS.