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.)

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.