A term of length 4 523 659 424 929

A. D. Mathias

pp. 75-86

in: Benedikt Lowe, Florian Rudolph (eds), Foundations of the formal sciences I, Synthese 133, 2002.

Abstract

Bourbaki suggest that their definition of the number 1 runs to some tens of thousands of symbols. We show that that is a considerable under-estimate, the true number of symbols being that in the title, not counting 1 179 618 517 981 links between symbols that are needed to disambiguate the whole expression.