I don't doubt the fact that open-source style "peer-review" wouldn't really work as a method for formally verifying algorithms. But in the end, computations *can* be checked. We can look at the algorithm being used, the source code specifically, and we can actually reason about it. The time we need to reason, we can. The only thing we can currently do is get a result from Mathematica, and then attempt to show its correctness by other means.

- did anyone, anywhere, actually suggest that Mathematica output ought to be elevated to "assumed truth"?

I recently read a paper on closed forms of some transcendental summation identities -- and it was formally published -- and it contained something along the lines of "this Maple code proves the identity because it uses Zeilberger's algorithm". While we can certainly say Zeilberger's algorithm is formally correct, we can't say anything about Maple's internals or even if Maple is indeed using the algorithm. Yet, the Maple result was brought to "truth" status.

Mathematica's, Maple's, and Matlab's convenience to the scientific world makes most people feel okay with giving up a little bit (or seemingly little!) freedom. As explained in Jordi's and my post, the convenience of having a calculation done in a second with the general notion that the result is probably correct makes people give up rigor. I would argue that we, as humans, are naturally lazy. We choose the path of least resistance. If Mathematica gives the same result as a formal proof, but Mathematica does it in 1/2 second, then most people would just choose Mathematica and get on with their work.

This is hazardous. Right now the scientific community still has a certain lack of tolerance for non-scientific work. Thirty or forty or so years ago, any proof by computer would have been deemed rejected by a mathematician (recall the famous controversy of the four-color problem). Their acceptance is becoming widespread, and computer proofs are becoming more acceptable, and unfortunately mathematicians have a lack of knowledge about computer science and programming in general that they can't be bothered with software details or even debates like this one. With Wolfram continually polishing Mathematica, making it look more like a shiny gem of automated mathematics, I think people will just start to accept it. This is of course speculation, but that's what happened with computers 30 years ago too.