On 08/31/2003 02:28 PM, RAUBER, JOEL wrote:
> As an aside, IYHO
>
> Is the four color map proof an example of an answerable problem,
> albeit with inefficient algorithm?
Yes!
(At least for now. It's a moving target. Somebody
could come up with a short proof tomorrow.)
More generally, this is a wonderful example of
idea #3:
1) We know there exist some results that are true
and have short proofs.
2) Gödel tells us there exist some results that are
true but no proof is possible.
3) It wouldn't be too surprising to find that there
exist some results that are true but for which
the proof is "almost" impossible, i.e. very very
long.
Feynman once hypothesized something resembling
opposite of idea #3: he challenged his friends
that any arithmetic question they could pose in
a few words, he could answer quickly. He lost
when somebody asked him for something like the
ones-place digit in the decimal representation
of the tangent of 10^10^10. (I forget the exact
details.)