On Sun, 6 Oct 2019 06:28:48 -0700 (PDT), Benoit <[email protected]> wrote:
> 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). I'll move the text so it's much further down, and probably remove it later. But some viewers might see both, & I think it's important to explain the difference. > 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", .. I used mostly your new text, but I kept "in part" because the visualization "looks ahead" to later actions to create it. I think the delay you mentioned is caused by the same issue; Gource tries to "bring in" symbols like people & then use them, but that algorithm doesn't work well at the beginning because everything appears at once. Your analogy to the big bang is quite apt. > 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!). The Metamath website explains much more of course, but I think it's important to give a quick here specifically on "what they are currently seeing". But I agree that the website link is the most important, since that gives people a chance to learn more :-). --- David A. Wheeler -- 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/E1iH8Nq-00038j-HI%40rmmprod07.runbox.
