and John Conway answered:
> I don't think they should be. There is, of course, the philosophical
> question of whether the existence of a valid proof of something should
> really convince us of its truth. But one shouldn't confuse this with
> the question of whether a particular proof really is a valid one.
>
These questions remind me instead one of the most intriguing
philosophical issues of our century : Wittgenstein's "Rule Following". It
has been analyzed by some of the most authoritative modern philosophers of
science (as J.J Katz and S.Kripke) and its real nature is not completely
clear.
In fact, the original question is a complex network of short sentences
in Wittgenstein's "Philosophical Investigations" that somehow recall us that
any rule to be interpreted requires another rule, till built-in rules which
are 'opaque' to our conscience, and that for that reason every behaviour can
match with every rule (Please apologize this synthesis: at the moment I have
no copy of these books, and the topic in itself is really not easy for me).
Somehow the problem seems to me already known to Lewis Carroll (the Turtle
and Achilles, quoted in Hofstadter's "Goedel, Escher, Bach")
From this point of view the difference between a computer-based proof,
a community-of-scientists-based proof and an usual short-and-comprehensible
proof is simply the set of built-in primitives and their acceptance for us.
For usual short-and-comprehensible proofs they are our linguistic
semantic rules and our logic reasoning primitives.
For computer-based proofs they are the programming languages primitives
and our acceptance of the Church-Turing thesis.
For community-of-scientists-based proofs they are our linguistic
semantic rules and our trust in the community of the interested scientists.
Anyway the theme in my opinion is strictly philosophical.
Luigi Borzacchini