These calculations have been carried out by José Grimm; see this report as well as this later paper. According to one version of the formalism in the original Bourbaki, Grimm gets $$16420314314806459564661629306079999627642979365493156625 \approx 1.6 \times 10^{55}$$ (see page 517 of the earlier report). The discrepancy with Solovay's number is probably due to some subtle difference of interpretation of some detail. Note that the English translation of Bourbaki introduces some "small" changes and Grimm gets a rather different value: $$5733067044017980337582376403672241161543539419681476659296689 \approx. 5.7 \times 10^{60}$$
Timothy Chow
- 82.6k
- 26
- 363
- 587