Bourbaki's definition of the number 1 According to a polemical article by Adrian Mathias, Robert Solovay showed that Bourbaki's definition of the number 1, written out using the formalism in the 1970 edition of Thé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$ 1054
symbols and 
871,880,233,733,949,069,946,182,804,910,912,227,472,430,953,034,182,177 $\approx$ 8.7 $\cdot$ 1053
connective links used in their treatment of bound variables.   Mathias notes that at 80 symbols per line, 50 lines per page, 1,000 pages per book, this definition would fill up 6 $\cdot$ 1047 books.  (If each book weighed a kilogram, these books would be about 200,000 times the mass of the Milky Way.)
My question: can anyone verify Solovay's calculation?
Solovay originally did this calculation using a program in Lisp.   I asked him if he still had it, but it seems he does not.  He has asked Mathias, and if it turns up I'll let people know.
(I conjecture that Bourbaki's proof of 1+1=2, written on paper, would not fit inside the observable Universe.)
 A: There are some interesting issues here, as I will elaborate. Let me first make a full quote of §4.2 "Bourbaki on formalization" from Thomas Hales' 2014 Bourbaki seminar "Developments in formal proofs" ((1)). 

Over the past generation, the mantle for Bourbaki-style mathematics has passed to
  the formal proof community, in the way it deliberates carefully on matters of notation
  and terminology, finds the appropriate level of generalization of concepts, and situates
  different branches of mathematics within a coherent framework.
  The opening quote claims that formalized mathematics is absolutely unrealizable. Bourbaki objected that formal proofs are too long ("la moindre démonstration
  . . . exigerait déjà des centaines de signes" [translation by YCor: "any proof... would require hundreds of signs")], that it would be a burden to forego
  the convenience of abuses of notation, and that they do not leave room for useful
  metamathematical arguments and abbreviations ((2)).
  Bourbaki is correct in the strict sense that no human artifact is absolutely trustworthy
  and that the standards of mathematics evolve in a historical process, according to available technology. Nevertheless, the technological barriers hindering formalization have
  fallen one after another. Today, computer verifications that check millions of inferences
  are routine. As Gonthier has convincingly shown in the Odd Order theorem project,
  many abuses of notation can actually be described by precise rules and implemented
  as algorithms, making the term abuse of notation really something of a misnomer, and
  allowing mathematicians to work formally with customary notation. Finally, the trend
  over the past decades has been to move more and more features out of the metatheory
  and into the theory by making use of features of higher-order logic and reflection. In
  particular, it is now standard to treat abbreviations and definitions as part of the logic
  itself rather than metatheory.

So Bourbaki's point (at that time, namely in the few years before 1970) was that writing formal proofs, although precisely defined, is a hopeless task. For this reason, Bourbaki made no effort of efficiency.
To give an illustrating example, assume that I'm writing an exercise program in some language, computing $n\mapsto \sum_{k=1}^nf(k+a_n)$, where $a(n)$ is the $n$-the decimal of $\pi$, and $f(n)$ say is $\lfloor n^{3/2}\rfloor$, which I previously defined as functions in the same programming language (the only point with this choice is that $f$ is much faster to compute than $a$). If I do it crudely 
$$(j:=0; \quad \text{for } k=1..n\;\; j:= j+f(k+a_n);\quad \text{return }j)$$ then I will compute $a(n)$ $n$ times. If instead I write 
$$(j:=0;\quad a:=a(n); \quad \text{for } k=1..n\;\; j:= j+f(k+a);\quad \text{return }j)$$
I'll compute $a(n)$ only once and hence this will be far quicker, although at first sight this is the same "algorithm". If I roughly say what should be the principle of the proof, this aspect will not appear.
The point of Bourbaki, once they assume that formalizing proofs is not worth an explicit realization, was therefore not to make this realization any practical. The possible (likely) fact that the size of the resulting formal proof of $1+1=2$ is huge is therefore anecdotical: for instance, if $N$ is the already huge proof of $0+1=1$ (or any related prior result), it's very possible that the formal proof will contain identical copies of this proof $N$ times, resulting in something of size $\ge N^2$. The conclusion is that the Bourbaki's formalization is highly unpractical— this conclusion was already Bourbaki's (yet based on a clear underestimate, which would appear today as efficient). Given that this formalization was written just to exist and without practical concern, this is not a big deal (although the paper advertized by the OP makes a lot of conclusions from this fact).
Most likely, the main ideas of Bourbaki's foundations could be formalized in a more efficient way (more efficient than highly inefficient is not too hard— should we bluster if $10^{54}$ is upgraded to $10^{20}$?), but I have no idea whether they could be formalized in a useful practical way. (There might also be good reasons that Bourbaki's foundations are not prone to efficient formalization; the estimate asked by OP is not a sufficient one, for the reason elaborated in the previous paragraph.) Given that Bourbaki's foundations have an interest which is now essentially reduced to historical (including for the aspects other than this exact formalization), and other foundations have been successfully formalized by others in the last 15 years, I'm not sure if anybody would spend energy on this. 
At a historical level, one can wonder whether Bourbaki's 1970 belief that formal proofs are not to be written down, has had any counterproductive effect in the next few decades; this is hard to measure and the paper ((3)) linked by the OP speculates on this with no serious grounds. Let me make a quote from the conclusion of ((3)).

Bourbaki themselves took the first course: as remarked by Corry, they shied away from their own
  foundations. I expect that they came to the conclusion that logic is crazy — they had to conclude that
  to protect their sanity; but were they aware that the picture of logic they were giving to their disciples
  is merely a grotesque distortion and diminution of that subject ? Is it too fanciful to see here, in this
  choice of formalism, with its unintuitive treatment of quantifiers, the reason for the phenomenon (which
  many mathematicians in various European countries have drawn to my attention whilst beseeching me not
  to betray their identity, lest the all-powerful Bourbachistes take revenge by depriving them progressively
  of research grants, office facilities and ultimately of employment) that where the influence of Bourbaki is
  strong, support for logic is weak ? How does one get the message across, to those who have accepted
  the Bourbachiste gospel, that logicians are actually not interested in a formal system of such purposeless
  prolixity, still less do they advocate it as the proper intellectual framework for doing mathematics ?

In regard to the fact that Bourbaki invited Hales to talk on formal proofs, I found the "revenge" claim particularly crisp today! ((3)) was written earlier, but whether there was a ban in the 1990s against elaboration and study of formal proofs, I'll leave it to better witnesses of that time and subject.
((1)) Th. Hales. Developments in formal proofs
((2)) N. Bourbaki. Théorie des ensembles [Set theory], 1970.
((3)) A. Mathias. A term of length 4,523,659,424,929 (1999). Link
A: Mathias, Grimm, and some people who've contributed to this Q&A seem to take these numbers as evidence of the impracticality of working formally in Bourbaki's theory. YCor explicitly called it unpractical, and said that Bourbaki shared that belief, which may be true. In light of that, I think it's worth writing a bit about the premise that seems to underlie the question.
If you define $F_1=F_2=1,\; F_{n+2}=F_n+F_{n+1}$, and eliminate $F$ from the expression $F_{250}$ by substitution, you get a tree of about $1.6\times 10^{52}$ nodes, or a string of that many symbols in Bourbaki/Polish notation.
I don't think it follows that the definition is a bad one. It's hard to see how you could avoid the blowup without introducing complications that would interfere with the definition's intended use.
You could object that this isn't a comparable situation because $250>1$, but that scarcely matters. Bourbaki happened to put a bunch of structure underneath $1$, but even if $1$ is primitive in your proof system, as soon as you do anything remotely interesting with it, you will have the same problem. The mere statement of your upper bound in Ramsey theory, never mind the proof, will have over Graham's-number symbols in it.
There is a simple way to get a better measure of the complexity of $F_{250}$ without changing the definition: merge common subtrees. The result is a dag of 249 nodes, of which 248 are additions: one for $F_3$, one for $F_4$, $\ldots$
Here's what happens when you merge common subtrees of the expressions from Grimm page 514. (The one called M is Solovay's, and the one called SS is mentioned in Timothy Chow's answer.)




expression
tree size
tree links
dag size
dag links




SS
57330670440×1050
21634097377×1050
13153
876


SM
315628276×1050
114233082×1050
13015
876


S
171713×1050
64721×1050
8061
544


M
24098×1050
8718×1050
7971
544




I calculated these with a Python program that constructs the complete dags in memory and then collects statistics with and without duplication counts. The construction consumes a whopping several megabytes of RAM due to CPython's inefficient object representation, and takes a noticeable fraction of a second due to CPython being slow. If my code were published in a series of books, and each book weighed 1 kilogram, the total mass of all the books would be a few grams.
The dags are still much larger than the code that made them. The remaining bloat can be blamed on the definition of $\exists$, which uses its body twice in a way that precludes sharing, and on complicated constructions that can't be shared because they have children, particularly ordered pairs. These problems can be solved by introducing parametrized subtrees. One approach is to express the dag as a tree without duplication by introducing a "structural let" that assigns names to subtrees, and then permit the named subtrees to have holes whose values are specified at each use point. (Or you can keep the dag and add $\phi$ nodes – see Appel.) With this extra flexibility you can write any of these expressions in just a few hundred nodes.
I want to stress that these concise expressions are fully formally equivalent to the original strings. Not a single double negative has been eliminated. Given the concise formula and an index, you can compute the symbol at that index in the original string.
In this framework – which is just a small subset of what's available in a proof system like Coq – it hardly matters what's primitive. If Bourbaki's pairing operator $\supset$ isn't primitive, you can define it once at the top of the expression; the space cost is constant regardless of how many times it's used. If the expression is a proposition whose proof will be formally checked, the axioms of $\supset$ need to be proven and checked as theorems only once each, adding a constant startup time regardless of how many times they're used. These costs aren't fundamentally different from the costs of implementing $\supset$ as primitive. Only if you convert to the normal form will you see a difference, and there is no reason ever to do that. It's an abstraction violation.
To summarize:

*

*These gigantic normal forms show up in all formal systems, not just Bourbaki's.

*They aren't a good measure of practicality or anything else.

