I think the sentence "Unlike the Gource visualization through 2019-09-26, this visualization shows initial contributions AND modifications, fixes some attributions, adds captions, and has various visual improvements. "
can/should be removed. Instead, some more words should be said about the captions, for example "The captions at the bottom-left note some events. These includes besides others creating a major section, joining of a new contributor or proving a "top 100" mathematical theorem <http://web.archive.org/web/20080105074243/http://personal.stevens.edu/~nkahl/Top100Theorems.html> " Alexander On Sunday, October 6, 2019 at 12:13:42 AM UTC+2, David A. Wheeler wrote: > > On Sat, 5 Oct 2019 09:03:45 -0700 (PDT), Benoit <[email protected] > <javascript:>> wrote: > ... > > Finally, maybe you could put some of the information you gave here in > the > > youtube description of the video. > > Fair enough. > > Below is the descriptive text for the video. I can edit it after the > video is made public, but best to be accurate in the first place. > > If anyone has any recommendations, let me know. We can't answer every > question, but if someone stumbles upon this, we can provide some > information and a hyperlink for more. > > --- David A. Wheeler > > ================================================ > > > This is a view of the contributions to the Metamath set.mm (Metamath > Proof Explorer (MPE)) database using Gource through 2019-09-26. This view > was created by David A. Wheeler. Music by audionautix.com - "Threshold" > by Jason Shaw, CC-BY-3.0 Unported. This video is released under the > Creative Commons CC-BY-3.0 Unported license. > > In this visualization, contributions are shown over time (the increasing > date is shown at the top center). Tiny circles are assertions (most are > proven, the near-white ones are axioms or definitions), note that there are > more and more over time. The "flashes" from people to the assertions are > initial contributions or modifications of some kind. The major areas (each > with a different color) represent the top headings of set.mm, with > branches inside the major areas representing level 2 headings. > > Unlike the Gource visualization through 2019-09-26, this visualization > shows initial contributions AND modifications, fixes some attributions, > adds captions, and has various visual improvements. > > The initial "exploding" effect is likely due in part because of the over > 500 theorems dated 5-Aug-1993, which is when Norman Megill first added a > date stamp to metamath.exe. Of course these were not done in one day but > are the result of off and on effort in his spare time during earlier > months, before he kept track of dates. Norman does not think it is possible > to recover those missing early dates. > > The section "CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY" formally defines > the logic system we use in set.mm. In particular, it defines symbols for > declaring truthful statements, along with rules for deriving truthful > statements from other truthful statements. But that's not enough; we need > something to talk *about*. The section "ZF (ZERMELO-FRAENKEL) SET THEORY" > allows us to assert properties of arbitrary mathematical objects called > "sets." The section "REAL AND COMPLEX NUMBERS" derives the basics of real > and complex numbers; in it we first construct real and complex numbers > ("prove that numbers exist"), axiomatize them, derive their basic > properties, and define important operations and subsets. > > While set.mm is the largest Metamath database, there are other databases > such as iset.mm (which uses intuitionistic logic). > > For more information on set.mm (Metamath Proof Explorer (MPE)), see its > home page at http://us.metamath.org/mpeuni/mmset.html -- 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/a4b08785-829a-4c17-9ae2-9e54ab592720%40googlegroups.com.
