> The ability to generate proofs is quite different from > the ability to work backward from a conjecture still in > need of proof.
You obviously didn't get the import of Godel's Lost Letter. Or, you have actually proved P != NP yourself. Congrats, enjoy your new found fame and riches - when's the big announcement?
But, while you are still slumming here - could you spell out for us slumdogs exactly what is that difference Kirby? If you mean that mathematicians don't work by simply listing out proof in such a sequence, I'm afraid there's no prize for that. But its certainly not clear that they don't work by *some* algorithm, hidden from us though it may be by that damned black box.
Regardless, there are many logical consequences to the simple fact that the proofs of a formal system are enumerable, your observations notwithstanding.