Return to Answer

These calculations have been carried out by José Grimm; see [1] as well as [2]. According to one version of the formalism in the original Bourbaki, Grimm gets $$16420314314806459564661629306079999627642979365493156625 \approx 1.6 \times 10^{55}$$ (see page 517 of [1, version 10]). 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}$$ EDIT: As suggested in the comments, here are the full citations for Grimm's papers.

[1] José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2018, pp.826. inria-00440786v10. doi:10.6092/issn.1972-5787/4771

[2] Grimm, J. (2010). Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. Journal of Formalized Reasoning, 3(1), 79-126. doi:10.6092/issn.1972-5787/1899

These calculations have been carried out by José Grimm; see [1] as well as [2]. According to one version of the formalism in the original Bourbaki, Grimm gets $$16420314314806459564661629306079999627642979365493156625 \approx 1.6 \times 10^{55}$$ (see page 517 of [1, version 10]). 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}$$ EDIT: As suggested in the comments, here are the full citations for Grimm's papers.

[1] José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2018, pp.826. inria-00440786v10. doi:10.6092/issn.1972-5787/4771

[2] Grimm, J. (2010). Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. Journal of Formalized Reasoning, 3(1), 79-126. doi:10.6092/issn.1972-5787/1899

These calculations have been carried out by José Grimm; see [1] as well as [2]. According to one version of the formalism in the original Bourbaki, Grimm gets $$16420314314806459564661629306079999627642979365493156625 \approx 1.6 \times 10^{55}$$ (see page 517 of [1, version 10]). 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}$$ EDIT: As suggested in the comments, here are the full citations for Grimm's papers.

[1] José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2018, pp.826. inria-00440786v10

[2] Grimm, J. (2010). Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. Journal of Formalized Reasoning, 3(1), 79-126.

These calculations have been carried out by José Grimm; see [1] as well as [2]. According to one version of the formalism in the original Bourbaki, Grimm gets $$16420314314806459564661629306079999627642979365493156625 \approx 1.6 \times 10^{55}$$ (see page 517 of [1, version 10]). 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}$$ EDIT: As suggested in the comments, here are the full citations for Grimm's papers.

[1] José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2018, pp.826. inria-00440786v10. doi:10.6092/issn.1972-5787/4771

[2] Grimm, J. (2010). Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. Journal of Formalized Reasoning, 3(1), 79-126. doi:10.6092/issn.1972-5787/1899

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}$$

These calculations have been carried out by José Grimm; see [1] as well as [2]. According to one version of the formalism in the original Bourbaki, Grimm gets $$16420314314806459564661629306079999627642979365493156625 \approx 1.6 \times 10^{55}$$ (see page 517 of [1, version 10]). 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}$$ EDIT: As suggested in the comments, here are the full citations for Grimm's papers.

[1] José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2018, pp.826. inria-00440786v10

[2] Grimm, J. (2010). Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. Journal of Formalized Reasoning, 3(1), 79-126.