|Perl: the Markov chain saw|
Granted, my logic was based on some fast and loose equivalences. Questionable hardly describes it. Isomorphism is not equality, otherwise it would be called equality. I don't have the time or the desire (or perhaps even the ability) to generate a valid, rigorous proof. I was trying to illustrate the thought process which lead me to see the original statement as an outgrowth of, rather than orthogonal to, the CHI.
A perfect system will never happen. Even given a perfect program, perfectly compiled to run on perfect hardware, an imperfect person will provide input and interpret the output. And here we go, Garbage In, Garbage Out. Oops.
But a set of automated tools can help people catch errors. My compilers help me catch errors in my code, and so I am more productive. That's why I use strict and warnings. Those extra picky heuristics catch whole classes of errors for me, and save me endless hours debugging. Any time I spend working on PHP is a strong reminder that a these checks are helpful. A decent, interactive "proof compiler" and an additional "debugger" could be very handy things.
I haven't kept up on my math, but back when I was taking all those credit hours, I found that the best way to screw up a proof (besides beer) was to miss an assumption. The next best way was to fail to see the "right" transformation needed to get things into the "right" shape. Interactive computer assistance could help in the second case, by rapidly sifting a number of potential transformations, until something clicks for the human operator. But there is no guarantee that this will find anything fruitful. I wonder if this kind of tool would serve to enhance the problem with hidden assumptions.
I don't know a cure for the missed assumption. And I'm not sure how to use a computer's strengths to find one. Fortunately there are people who are smarter, better educated, and more dedicated than me working on these things.
Your description of the proof as a system sounds an awful lot like a Turing machine. :) Proofs are recorded in sets of symbols that are systematically manipulated to demonstrate an assertion. (Are proofs completely embodied by these symbolic forms, or is something lost in the ecoding?) As such they should be amenable to automated verification. It seems to me that the problem really lies in a way of creating a proof description language that is flexible and expressive enough to encompass useful research work (not just lame undergraduate homework proofs 'Prove that the infinite series BLAH converges, or diverges'). And yet still structured enough to yield to computation easily.
While I like your metaphor of the mathematician as the program, the system seems to be really a non-deterministic Turing machine. I interpret the corpus of proven statements as the rule set, the current set of symbols embody the state, and the verifier is the lowly head. The proof is really just the trace of the program as the NDTM ran through its paces. A verifier must merely demonstrate that only legal moves were made at each state transition. ( Hmm, this formulation leads me to believe that writing a proof with a computer is equivalent to the halting problem. But don't ask me to prove it. )
Just as I am not the bag of water and assorted chemicals madly fermenting in my chair, I am the process of fermentation, the proof is the process of calculation.
Now I've really wandered off topic. So I'll bring it back on track and summarize. Perfect verification is impossible. We can use our computers to improve our ability to catch a certain (unspecified) set of errors in our mathematical reasoning. The question is, is that set of errors disjoint from the set of errors that we are already good at catching? Or more simply, is automated validation useful?
Thank you for engaging me in this thought provoking discussion.