[ahmedfromtunis]

That's exactly the kind of situation I had in mind when I wrote that.

Goodstein’s theory would take more symbols than there are atoms in the observable universe to write down in "classic" maths. To "fix" this, mathematicians had to use a "new" way of thinking about infinity known as transfinite induction.

I think if we're smart enough to detect(?) a proof, we'll find a way to express it in a finite manner.