Witnesses for mathematical software 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.).
The concept of "witnesses" or "checkable proofs" is not totally new: as mentioned in the comments, look for the concept of "certificate". Three examples came to mind, there are more (in the comments and elsewhere):


Kurt Mehlhorn described in 1999 a similar problem in computational geometry algorithms (e.g. minor errors in coordinates can yield big errors in the results of some algorithm), solved in a similar way in the library Leda, by insisting that each algorithm produces a "certificate" of its answer in addition of the answer itself.
Demaine, Lopez-Ortiz and Munro in 2000 used the concepts of certificates (they call them "proofs") to show adaptive lower bounds on the computation of the union and intersection (and difference, but this one is trivial) of sorted sets. Don't exclude their work because they did not use certiticates to protect against computing errors: they showed that even though the certificate can be linear in the size of the instance in the worst case, it is often shorter, and hence can be "checked" in sublinear time (given random access to the input as a sorted array or a B-Tree), and in particular in time less than required to compute such a certificate. 
I have been using the concept of certificates on various other problems since seeing Ian Munro presenting their implementation at Alenex 2001, and in particular for permutations (apologies for the shameless plug, another one is coming), where the certificate is shorter in the best case than in the worst or average case, which yields a compressed data structure for permutations. Here again, checking the certificate (i.e. the order) takes at most linear time, less than computing  it (i.e. sorting). 

The concept is not always usefull for error checking: there are problems where checking the certificate takes as much time as producing it (or simply producing the result). Two examples come to mind, one trivial and one complicated, Blum and Kannan (mentioned in the comments) give others.


The certificate for proving that an element is not in an unsorted array of $n$ elements is obtained in $n$ comparisons and checked in the same time.
The certificate for the convex hull in two and three dimensions, if the points are given in random order, takes as much bits to encode as comparisons to compute [FOCS 2009] (other shameless plug).



The library Leda is the most general effort (that I know of) toward making deterministic certificate-producing algorithms the norm in practice. Blum and Kannan's paper is the best effort I saw to make it the norm in theory, but they do show the limits of this approach. 

Hope it helps...