Bigness (Part 1)

The French mathematicians who went under the pseudonym Nicolas Bourbaki did a lot of good thingsbut not so much in the foundations of mathematics. In this paper, Adrian Mathias showed that their formalism was incredibly inefficient:

Adrian R. D. Mathias, A term of length 4,523,659,424,929, Synthese 133 (2002), 7586.

He proved that the definition of the number 1 in Bourbakis 1954 text on set theory requires 4,523,659,424,929 symbols and also 1,179,618,517,981 links connecting symbols, without...