There are quite a few famous gigantic numbers used in useful mathematical proofs, like Skewes's number, Graham's number, and the number $2 \uparrow \uparrow 10^{10^6}$ from Coward and Lackenby's 2011 result on determining the ambient isotropy of links. However, these numbers are all upper (or lower) bounds, which I think is not quite as interesting, because you can often make an upper bound higher by just doing less work.

What is the largest number to have appeared naturally in a useful mathematical proof that isn't just an upper or lower bound? Obviously the terms "naturally" and "useful" make this question somewhat subjective. Also, I'm not particularly interested in numbers defined in the form "the smallest number satisfying $X$ property", so I'd prefer a number where we can actually estimate its value to some degree of precision - e.g. we can roughly estimate how many iterated logarithms (or another slowly-growing function) would be required to bring it down to $o(1)$. (I think this requirement would rule out $\mathrm{TREE}(3)$.)

One possibility that occurs to me is $\sim 8 \times 10^{53}$, the cardinality of the monster group, but I bet there are larger ones.