Skip to main content
MathOverflow

Return to Answer

amended the phrase "poorly written", since the question has been edited
Source Link
Todd Trimble
Todd Trimble
  • 53.3k
  • 6
  • 205
  • 322

This question is poorly written but since there's somethingThere are some interesting behindissues here, let meas I will elaborate. Let me first make a full quote of §4.2 "Bourbaki on formalization" from Thomas Hales' 2014 Bourbaki seminar "Developments in formal proofs" ((1)).

This question is poorly written but since there's something interesting behind, let me elaborate. Let me first make a full quote of §4.2 "Bourbaki on formalization" from Thomas Hales' 2014 Bourbaki seminar "Developments in formal proofs" ((1)).

There are some interesting issues here, as I will elaborate. Let me first make a full quote of §4.2 "Bourbaki on formalization" from Thomas Hales' 2014 Bourbaki seminar "Developments in formal proofs" ((1)).

fixed notation
Source Link
YCor
YCor
  • 63.9k
  • 5
  • 187
  • 286

To give an illustrating example, assume that I'm writing an exercise program in some language, computing $n\mapsto \sum_{k=1}^nf(k+a_n)$, where $a(n)$ is the $n$-the decimal of $\pi$, and $f(n)$ say is $\lfloor n^{3/2}\rfloor$, which I previously defined as functions in the same programming language (the only point with this choice is that $f$ is much faster to compute than $a$). If I do it crudely $$(j:=0; \quad \text{for } k=1..n\;\; j\to j+f(k+a_n);\quad \text{return }j)$$$$(j:=0; \quad \text{for } k=1..n\;\; j:= j+f(k+a_n);\quad \text{return }j)$$ then I will compute $a(n)$ $n$ times. If instead I write $$(j:=0;\quad a:=a(n); \quad \text{for } k=1..n\;\; j\to j+f(k+a);\quad \text{return }j)$$$$(j:=0;\quad a:=a(n); \quad \text{for } k=1..n\;\; j:= j+f(k+a);\quad \text{return }j)$$ I'll compute $a(n)$ only once and hence this will be far quicker, although at first sight this is the same "algorithm". If I roughly say what should be the principle of the proof, this aspect will not appear.

The point of Bourbaki, once they assume that formalizing proofs is not worth an explicit realization, was therefore not to make this realization any practical. The possible (likely) fact that the size of the resulting formal proof of $1+1=2$ is huge is therefore anecdotical: for instance, if $N$ is the already huge proof of $0+1=1$ (or any related prior result), it's very possible that the formal proof will contain identical copies of this proof $N$ times, resulting in something of size $N^2$$\ge N^2$. The conclusion is that the Bourbaki's formalization is highly unpractical— this conclusion was already Bourbaki's (yet based on a clear underestimate, which would appear today as efficient). Given that this formalization was written just to exist and without practical concern, this is not a big deal (although the paper advertized by the OP makes a lot of conclusions from this fact).

To give an illustrating example, assume that I'm writing an exercise program in some language, computing $n\mapsto \sum_{k=1}^nf(k+a_n)$, where $a(n)$ is the $n$-the decimal of $\pi$, and $f(n)$ say is $\lfloor n^{3/2}\rfloor$, which I previously defined as functions in the same programming language (the only point with this choice is that $f$ is much faster to compute than $a$). If I do it crudely $$(j:=0; \quad \text{for } k=1..n\;\; j\to j+f(k+a_n);\quad \text{return }j)$$ then I will compute $a(n)$ $n$ times. If instead I write $$(j:=0;\quad a:=a(n); \quad \text{for } k=1..n\;\; j\to j+f(k+a);\quad \text{return }j)$$ I'll compute $a(n)$ only once and hence this will be far quicker, although at first sight this is the same "algorithm". If I roughly say what should be the principle of the proof, this aspect will not appear.

The point of Bourbaki, once they assume that formalizing proofs is not worth an explicit realization, was therefore not to make this realization any practical. The possible (likely) fact that the size of the resulting formal proof of $1+1=2$ is huge is therefore anecdotical: for instance, if $N$ is the already huge proof of $0+1=1$ (or any related prior result), it's very possible that the formal proof will contain identical copies of this proof $N$ times, resulting in something of size $N^2$. The conclusion is that the Bourbaki's formalization is highly unpractical— this conclusion was already Bourbaki's (yet based on a clear underestimate, which would appear today as efficient). Given that this formalization was written just to exist and without practical concern, this is not a big deal (although the paper advertized by the OP makes a lot of conclusions from this fact).

To give an illustrating example, assume that I'm writing an exercise program in some language, computing $n\mapsto \sum_{k=1}^nf(k+a_n)$, where $a(n)$ is the $n$-the decimal of $\pi$, and $f(n)$ say is $\lfloor n^{3/2}\rfloor$, which I previously defined as functions in the same programming language (the only point with this choice is that $f$ is much faster to compute than $a$). If I do it crudely $$(j:=0; \quad \text{for } k=1..n\;\; j:= j+f(k+a_n);\quad \text{return }j)$$ then I will compute $a(n)$ $n$ times. If instead I write $$(j:=0;\quad a:=a(n); \quad \text{for } k=1..n\;\; j:= j+f(k+a);\quad \text{return }j)$$ I'll compute $a(n)$ only once and hence this will be far quicker, although at first sight this is the same "algorithm". If I roughly say what should be the principle of the proof, this aspect will not appear.

The point of Bourbaki, once they assume that formalizing proofs is not worth an explicit realization, was therefore not to make this realization any practical. The possible (likely) fact that the size of the resulting formal proof of $1+1=2$ is huge is therefore anecdotical: for instance, if $N$ is the already huge proof of $0+1=1$ (or any related prior result), it's very possible that the formal proof will contain identical copies of this proof $N$ times, resulting in something of size $\ge N^2$. The conclusion is that the Bourbaki's formalization is highly unpractical— this conclusion was already Bourbaki's (yet based on a clear underestimate, which would appear today as efficient). Given that this formalization was written just to exist and without practical concern, this is not a big deal (although the paper advertized by the OP makes a lot of conclusions from this fact).

Source Link
YCor
YCor
  • 63.9k
  • 5
  • 187
  • 286

This question is poorly written but since there's something interesting behind, let me elaborate. Let me first make a full quote of §4.2 "Bourbaki on formalization" from Thomas Hales' 2014 Bourbaki seminar "Developments in formal proofs" ((1)).

Over the past generation, the mantle for Bourbaki-style mathematics has passed to the formal proof community, in the way it deliberates carefully on matters of notation and terminology, finds the appropriate level of generalization of concepts, and situates different branches of mathematics within a coherent framework. The opening quote claims that formalized mathematics is absolutely unrealizable. Bourbaki objected that formal proofs are too long ("la moindre démonstration . . . exigerait déjà des centaines de signes" [translation by YCor: "any proof... would require hundreds of signs")], that it would be a burden to forego the convenience of abuses of notation, and that they do not leave room for useful metamathematical arguments and abbreviations ((2)). Bourbaki is correct in the strict sense that no human artifact is absolutely trustworthy and that the standards of mathematics evolve in a historical process, according to available technology. Nevertheless, the technological barriers hindering formalization have fallen one after another. Today, computer verifications that check millions of inferences are routine. As Gonthier has convincingly shown in the Odd Order theorem project, many abuses of notation can actually be described by precise rules and implemented as algorithms, making the term abuse of notation really something of a misnomer, and allowing mathematicians to work formally with customary notation. Finally, the trend over the past decades has been to move more and more features out of the metatheory and into the theory by making use of features of higher-order logic and reflection. In particular, it is now standard to treat abbreviations and definitions as part of the logic itself rather than metatheory.

So Bourbaki's point (at that time, namely in the few years before 1970) was that writing formal proofs, although precisely defined, is a hopeless task. For this reason, Bourbaki made no effort of efficiency.

To give an illustrating example, assume that I'm writing an exercise program in some language, computing $n\mapsto \sum_{k=1}^nf(k+a_n)$, where $a(n)$ is the $n$-the decimal of $\pi$, and $f(n)$ say is $\lfloor n^{3/2}\rfloor$, which I previously defined as functions in the same programming language (the only point with this choice is that $f$ is much faster to compute than $a$). If I do it crudely $$(j:=0; \quad \text{for } k=1..n\;\; j\to j+f(k+a_n);\quad \text{return }j)$$ then I will compute $a(n)$ $n$ times. If instead I write $$(j:=0;\quad a:=a(n); \quad \text{for } k=1..n\;\; j\to j+f(k+a);\quad \text{return }j)$$ I'll compute $a(n)$ only once and hence this will be far quicker, although at first sight this is the same "algorithm". If I roughly say what should be the principle of the proof, this aspect will not appear.

The point of Bourbaki, once they assume that formalizing proofs is not worth an explicit realization, was therefore not to make this realization any practical. The possible (likely) fact that the size of the resulting formal proof of $1+1=2$ is huge is therefore anecdotical: for instance, if $N$ is the already huge proof of $0+1=1$ (or any related prior result), it's very possible that the formal proof will contain identical copies of this proof $N$ times, resulting in something of size $N^2$. The conclusion is that the Bourbaki's formalization is highly unpractical— this conclusion was already Bourbaki's (yet based on a clear underestimate, which would appear today as efficient). Given that this formalization was written just to exist and without practical concern, this is not a big deal (although the paper advertized by the OP makes a lot of conclusions from this fact).

Most likely, the main ideas of Bourbaki's foundations could be formalized in a more efficient way (more efficient than highly inefficient is not too hard— should we bluster if $10^{54}$ is upgraded to $10^{20}$?), but I have no idea whether they could be formalized in a useful practical way. (There might also be good reasons that Bourbaki's foundations are not prone to efficient formalization; the estimate asked by OP is not a sufficient one, for the reason elaborated in the previous paragraph.) Given that Bourbaki's foundations have an interest which is now essentially reduced to historical (including for the aspects other than this exact formalization), and other foundations have been successfully formalized by others in the last 15 years, I'm not sure if anybody would spend energy on this.

At a historical level, one can wonder whether Bourbaki's 1970 belief that formal proofs are not to be written down, has had any counterproductive effect in the next few decades; this is hard to measure and the paper ((3)) linked by the OP speculates on this with no serious grounds. Let me make a quote from the conclusion of ((3)).

Bourbaki themselves took the first course: as remarked by Corry, they shied away from their own foundations. I expect that they came to the conclusion that logic is crazy — they had to conclude that to protect their sanity; but were they aware that the picture of logic they were giving to their disciples is merely a grotesque distortion and diminution of that subject ? Is it too fanciful to see here, in this choice of formalism, with its unintuitive treatment of quantifiers, the reason for the phenomenon (which many mathematicians in various European countries have drawn to my attention whilst beseeching me not to betray their identity, lest the all-powerful Bourbachistes take revenge by depriving them progressively of research grants, office facilities and ultimately of employment) that where the influence of Bourbaki is strong, support for logic is weak ? How does one get the message across, to those who have accepted the Bourbachiste gospel, that logicians are actually not interested in a formal system of such purposeless prolixity, still less do they advocate it as the proper intellectual framework for doing mathematics ?

In regard to the fact that Bourbaki invited Hales to talk on formal proofs, I found the "revenge" claim particularly crisp today! ((3)) was written earlier, but whether there was a ban in the 1990s against elaboration and study of formal proofs, I'll leave it to better witnesses of that time and subject.

((1)) Th. Hales. Developments in formal proofs

((2)) N. Bourbaki. Théorie des ensembles [Set theory], 1970.

((3)) A. Mathias. A term of length 4,523,659,424,929 (1999). Link