Return to Question

According to a polemical article by Adrian Mathias, Robert Solovay showed that Bourbaki's definition of the number 1, written out using the formalism in the 1970 edition of Théorie des Ensembles, requires

2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897 $\approx$ 2.4 $\cdot$ 10⁵⁴

symbols and

871,880,233,733,949,069,946,182,804,910,912,227,472,430,953,034,182,177 $\approx$ 8.7 $\cdot$ 10⁵³

connective links used in their treatment of bound variables. Mathias notes that at 80 symbols per line, 50 lines per page, 1,000 pages per book, this definition would fill up 6 $\cdot$ 10⁴⁷ books. (If each book weighed a kilogram, these books would be about 200,000 times the mass of the Milky Way.)

My question: can anyone verify Solovay's calculation?

Solovay originally did this calculation using a program in Lisp. I asked him if he still had it, but it seems he does not. He has asked Mathias, and if it turns up I'll let people know.

(I conjecture that Bourbaki's proof of 1+1=2, written on paper, would not fit inside the observable Universe.)

According to a polemical article by Adrian Mathias, Robert Solovay showed that Bourbaki's definition of the number 1, written out using the formalism in the 1970 edition of Théorie des Ensembles, requires

2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897 $\approx$ 2.4 $\cdot$ 10⁵⁴

symbols and

871,880,233,733,949,069,946,182,804,910,912,227,472,430,953,034,182,177 $\approx$ 8.7 $\cdot$ 10⁵³

connective links used in their treatment of bound variables. Mathias notes that at 80 symbols per line, 50 lines per page, 1,000 pages per book, this definition would fill up 6 $\cdot$ 10⁴⁷ books. (If each book weighed a kilogram, these books would be about 200,000 times the mass of the Milky Way.)

My question: can anyone verify Solovay's calculation?

Solovay originally did this calculation using a program in Lisp. I asked him if he still had it, but it seems he does not. He has asked Mathias, and if it turns up I'll let people know.

(I conjecture that Bourbaki's proof of 1+1=2, written on paper, would not fit inside the observable Universe.)

According to Adrian Mathias, Robert Solovay showed that Bourbaki's definition of the number 1, written out using the formalism in the 1970 edition of Théorie des Ensembles, requires $$ 2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897 \approx 2.4 \cdot 10^{54} $$ symbols and $$ 871,880,233,733,949,069,946,182,804,910,912,227,472,430,953,034,182,177 \approx 8.7 \cdot 10^{53} $$ connective links (used in their treatment of bound variables). Mathias notes that at 80 symbols per line, 50 lines per page, 1,000 pages per book, this definition would fill up 6 $\cdot$ 10⁴⁷ books. If each book weighed a kilogram, these books would weigh about 3 $\cdot$ 10¹⁷ times the mass of the Sun. That's about 200,000 times the mass of the Milky Way.

My question: can anyone verify Solovay's calculation?

Solovay originally did this calculation using a program in Lisp. I asked him if he still had it, but it seems he does not. He has asked Mathias, and if it turns up I'll let people know.

(I conjecture that Bourbaki's proof of 1+1=2, written on paper, would not fit inside the observable Universe.)

According to a polemical article by Adrian Mathias, Robert Solovay showed that Bourbaki's definition of the number 1, written out using the formalism in the 1970 edition of Théorie des Ensembles, requires

2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897 $\approx$ 2.4 $\cdot$ 10⁵⁴

symbols and

871,880,233,733,949,069,946,182,804,910,912,227,472,430,953,034,182,177 $\approx$ 8.7 $\cdot$ 10⁵³

connective links used in their treatment of bound variables. Mathias notes that at 80 symbols per line, 50 lines per page, 1,000 pages per book, this definition would fill up 6 $\cdot$ 10⁴⁷ books. (If each book weighed a kilogram, these books would be about 200,000 times the mass of the Milky Way.)

My question: can anyone verify Solovay's calculation?

Solovay originally did this calculation using a program in Lisp. I asked him if he still had it, but it seems he does not. He has asked Mathias, and if it turns up I'll let people know.

(I conjecture that Bourbaki's proof of 1+1=2, written on paper, would not fit inside the observable Universe.)