Another possibility is that there is a formal proof of feasible length, but no feasible search will ever turn it up. (Well, unless P = NP).
This reminds me of people who argue that, because P != NP, we will never prove this. (The key to the argument, IIRC, is that any proof of this fact will have very high algorithmic complexity.) I'm not sure how to find this argument now. (There is something like it one of Doron Zeilberger's April Fools opinions.)
the fact that people are able to prove astonishing things about 3-manifolds without running into contradictions I regard as very weak evidence in favor of ZF
Yes, these results should be formalisable in higher-order arithmetic (indeed _n_th order for n a single-digit number). It is the set theorists' work with large cardinals and the like that provides the only real evidence for the consistency of such a high-powered system as ZF.
Update: Discussion has moved on to a new thread.
The hiatus is over with today's publication of chapter 73, and the previous thread is approaching the 500-comment threshold, so let's start a new Harry Potter and the Methods of Rationality discussion thread. This is the place to discuss Eliezer Yudkowsky's Harry Potter fanfic and anything related to it.
The first 5 discussion threads are on the main page under the harry_potter tag. Threads 6 and on (including this one) are in the discussion section using its separate tag system. Also: one, two, three, four, five, six, seven. The fanfiction.net author page is the central location for information about updates and links to HPMOR-related goodies, and AdeleneDawner has kept an archive of Author's Notes.
As a reminder, it's often useful to start your comment by indicating which chapter you are commenting on.
Spoiler Warning: this thread is full of spoilers. With few exceptions, spoilers for MOR and canon are fair game to post, without warning or rot13. More specifically: