[Virginia-American]

I don't know if it has a name; it's a consequence of there being an infinite number of theorems. I don't see how it follows that there are some that require an infinite proof.

Dr S: can you add anything?

[Doctor Stochastic]

It's been a long time since I looked at length of proofs. There's a long discussion of this (and lots of other things) here. I think that a proof using a Turing machine (and this covers all models of computation so far proposed) requires that the machine stop. There is an enumeration of all proofs though. Even if all proofs were finite, there would be infinitely many proofs in a system.

One can of course talk about infinte objects using only finitary means. For example, mathematical induction is only a schema for infinitely steps. Transcendental induction is also possible.

I'll look around on Google and in some texts and maybe have something to post later.

I still don't know how to pronounce adele. I found three spellings in different encyclopaedias: adele, adéle, and adèle; not helpful.

[LibWhacker]

I don't see how it follows that there are some that require an infinite proof.

The reasoning is similar to the proof that the number of primes is infinite. You start by assuming that there is some largest prime and show that that leads to a contradiction. We can do the same thing here . . . Assume that there is some "largest proof," and you'll see this leads to an immediate contradiction.