According to Adrian Mathias, Robert Solovay showed that Bourbaki's definition of the number 1, written out using the formalism in the 1970 edition of Théorie des Ensembles, requires
$$ 2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897 \approx 2.4 \cdot 10^{54}
$$
symbols ...
Certainly there are more economical definitions. I think, as a regular ZFC formula, the number 1 can be defined in a few lines. 0 is the empty set {}, and 1 is the set {0}. It should not take much longer as a first order formula. BTW I am not sure the tag "enumerative-combinatorics" is appropriate here.
You're talking to mathematicians on a research-level site, so I'm not sure it's necessary to rant about the meaning of $10^{54}$ in terms on number of lines/pages/ book whatsoever. Have you opened the book? It doesn't take $10^{17}$ seconds to see that it defines a cardinal as equivalence class of sets modulo bijection. Maybe having a little look is a good starting point before asking a research-level question: it at least gives some context (I don't claim this answers the question, assuming it has any mathematical substance).
It just reminded me about The Library of Babel(en.wikipedia.org/wiki/The_Library_of_Babel) by Borges. There is an estimate of its size (you can find on the Wikipedia page in Russian, for example) which says that the Library is 10^611 338 times bigger than the observable universe
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,338,752,092,897!
Some context in support of this question. Mathias's paper is one of series of polemics claiming mathematicians have neglected logic. In it, he claims to demonstrate empirically the "hopeless unwieldness" of the formalism Bourbaki adopts. To do that, he claims to show exactly how "cumbersome" it would be to define 1 using that formalism. Whether Mathias is right depends on whether Solovay's calculations are correct. Surely this is a research level question.
My understanding is that there is a certain number $N$ which can computed and is interpreted as the number of symbols in a complete formal proof (written according to some precise rules), used in some somewhat obsolete book, and a lot of noise according to what it implies that this number is $>10^{50}$ rather than just a few billions. Since Bourbaki's foundations are never used in the formal proof softwares developed in the last decades, all the surrounding claims are pointless speculations.
@Justaguy: The question is very badly formulated. The math content is almost none: the OP cannot estimate certain number and asks if anybody can help. Computing that number is mathematically trivial. The style of the question is awful.
To have less crackpotesque considerations on Bourbaki vs recent developments on formal proofs, including some discussion of Bourbaki, you can read Th. Hales's 2014 Bourbaki seminar. See e.g. the discussion in §4.2.
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.
A single 80gsm A5 sheet weighs about 2.5 grams (source: papersizes.org/weight-of-sheets.htm), even double sided we have to multiply the number of pages by 1.25 for adjustment. I'd suggest adding also a total of 20g for the cover and some extra pages around it. This makes an additional 1.02 adjustment per book. Sure, the order of magnitude is not very different, but I'm just saying.
@BenCrowell I don't claim that the computation of this number $N$ (as answered by Timothy Chow), nor asking about the result of this computation, is anything crackpotesque. I was referring to some speculative non-mathematical conclusions drawn from the result of this computation.
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.
@TimothyChow What I see wrong with the post is not the question (to which you posted a timely answer) but (1) a useless emphatic comment on the meaning of the number $10^{54}$ (2) a link to a paper with polemical contents.
For the question itself, Mark says it's trivial. It's a bit exaggerated: the non-trivial part (today) would be to set it up, while a software would immediately output the result. But it might have been considered as off-topic for this reason too.
I've refrained to vote close the question (my hope was that the OP would focus the post to the question and remove superfluous comparisons, maybe directly quote Solovay rather than quoting the polemical paper, and possibly give more factual context, but he unfortunately didn't.
As Todd pointed out, the "useless emphatic" comment was a quotation from the "paper with polemical contents." Attacking John Baez strikes me as a case of shooting the messenger. If the question itself is fine, and it arose from reading a paper, I don't see why it's objectionable to link to the paper in question. Admittedly there's no need to quote from the paper but I don't see anything so terrible about doing so.
Mathias' paper is highly polemical, including strong (anonymous but global) accusations. Linking to the paper without any warning, and even quoting some non-essential part of it, could arouse the suspicion that the OP doesn't see any problem with these allegations, or even wishes to advertise them. Not amending the post after the criticism in the comments somewhat corroborates this impression.
I came across Mathias's website and some of his papers about 20 years ago and first read the "Bourbaki's definition of the number 1" paper then. My impression from those who knew people who knew people etc is that Mathias definitely enjoyed being polemical, generally speaking. I wonder if JB or Todd would enjoy as much Mathias's pointed insistence that Mac Lane's ideas for doing categories without set theory were somehow misguided?
(All this said, I did not downvote JB's question nor vote to close it)
@YCor for a more sober commentary, perhaps the comment of Toby Bartels here johncarlosbaez.wordpress.com/2020/04/13/bigness-part-1 is worth reading; I don't think Toby was criticising John at all, but merely adding context
Discussion on question by John Baez: …
Discussion on question by John Baez: …