Hi David, I agree with Alexander that the paragraph "Unlike the Gource... improvements" can be removed (and the older video it mentions can be removed too, if youtube allows that).
Concerning the following paragraph, I would shorten it to something like: The initial "big bang" effect is due to the 519 theorems dated 5-Aug-1993, which is when Norman Megill first added a date stamp to metamath.exe. Actually, these theorems were proved over a period of a few months before that date. I.e.: I used "big bang" to be more dramatic than "exploding" and to suggest the birth of a (mathematical) universe; I removed "likely" and "in part", because these 519 theorems are the reason. I obtained 519 as the number of occurrences of " (Contributed by NM, 5-Aug-1993.) " in the current set.mm after setting line width to 9999. I think the paragraph "The section..." is not necessary, since it begins to explain what pertains to the Metamath website. So your link to it is sufficient (and necessary!). By the way: the big bang effect in the video appears to happen in Nov-1993 (and the video shows a few contributions before). So it appears that the visualization is not entirely faithful (I think it's not to worry about). For the record, by looking at occurrences as above, I found: Aug-1993: 625 (including 519 on 5-Aug-1993, the earliest date) Sep-1993: 20 Oct-1993: 0 Nov-1993: 0 Dec-1993: 28 (I searched the strings "-xxx-1993.) " so there is a slight chance very few of these occurrences are not real contributions because the occur some place else in the file.) And for the past century, by year: 1993: 673 1994: 574 1995: 617 1996: 339 1997: 159 1998: 213 1999: 809 2000: 142 Thanks again for the great video. Benoît -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/142b3519-0083-4495-9d47-0dad6a3f9fbf%40googlegroups.com.
