Infinitely long proofs

It's actually vastly easier to view proofs as trees in this context, so I'll do that.

Generally, an "infinitely long proof" is more accurately a well-founded infinitely-branching tree (or something morally equivalent) - the idea being that we're working in some infinitary logic (or some logic of similar nature) where the basic deductive steps might involve infinitely many hypotheses. "Well-founded" means that the tree has no infinite paths, that is, no infinite regress: a node is "justified" by its immediate successors, with the root being the conclusion of the proof.

Now the point is that there is a notion associated to a well-founded tree which serves as a decent proxy for proof length - namely, the rank of the tree. Given a well-founded tree $T$, there is a unique function $\nu$ from the nodes of $T$ to the ordinals such that for each node $\alpha$ we have $$\nu(\alpha)=\sup\{\nu(\beta)+1: \alpha\prec \beta\}$$ (we take the supremum of the emptyset to be $0$, which means that $\nu(\alpha)=0$ for every terminal node $\alpha$). When we speak of the "length" of a proof in an infinitary system, this is what we (usually) mean. There are well-founded trees of arbitrary ordinal rank - while we generally are interested in at-most-countably-branching trees, which always have rank $<\omega_1$, we're not a priori limited to such.

As for their application, they show up in the study of infinitary logic in several ways (and Barwise's book has a good section on them) but they're also used to study classical first-order logic by replacing a complicated finitary system by an infinitary system which nonetheless has some better features; this happens with reasonable frequency in ordinal analysis, see e.g. here).

For starters, you could prove Peano's Fifth Axiom, a.k.a. the Axiom of Induction.