I, like many people, am a keen user of mathematical software such as Mathematica and Maple. However, I have become increasingly frustrated by the many cases where such software simply gives you the wrong answer without warning. This can occur when performing all sorts of operations from simple sums to optimization amongst many other examples.
I have been wondering what could be done about this serious problem. What is needed is some way to allow the user to verify the correctness of an answer that is given so that they have some confidence in what they are being told. If you were to get a solution from a math colleague she/he might just sit down and show you their working. However this is not feasible for a computer to do in most cases. Could the computer instead give you a simple and easily checkable witness of the correctness of their answer? Checking may have to be done by computer but hopefully checking the checking algorithm will be much easier than checking the algorithm to produce the witness in the first place. When would this be feasible and how exactly could this be formalized
So in summary, my question is the following.
Could it be possible at least in theory for mathematical software to provide a short checkable proof along with the answer you have asked for?
A trivial case where we can do this immediately is for factorization of integers of course or many of the classic NP-complete problems (e.g. Hamiltonian circuit etc.).