Discussion on question by John Baez: Bourbaki's definition of the number 1

@YCor That's some contrived reasoning you have there.

It seems like Bourbaki inadvertently gave a much more concise definition of the number 2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,33‌​8,752,092,897!

Clearly Solovay is not a crackpot, and yet I don't understand from the context available here or in the Mathias paper why Solovay would have cared enough, even as a recreational exercise, to calculate this. Clearly if you have definitions written in terms of other definitions, to depth $n$, then direct substitution of the strings of symbols gives a string whose length increases exponentially with $n$. This is elementary, and computing a specific example, in a specific mathematical system, would seem to be of no interest.

I'm going to move comments to chat. Honestly, I'm finding some of the language used in comments pretty abusive (such as saying that the OP is "ranting" when in fact he's quoting someone, or saying the style of the question is "awful"). Let's tone it down, please.