New Gource visualization of set.mm

[David A. Wheeler]

I have a new significantly-updated Gource visualization of set.mm's progress over time:
https://www.youtube.com/watch?v=y_eqBLFlXOs

This video is currently "unlisted" - I'd like to hear if this is okay before making it public.

Please take a look & if you see an issue, let me know!

The key changes are:
* Any contribution or modification counts as a "flash" from the user to the assertion
(this shows more of the actual activity than the previous visualization showed).
* A number of set.mm attributions were fixed. The older visualization made some
unintentional errors obvious, so we went back to fix them & we now use that
fixed data set.
* The major section labels are further away from the center, so they
are much more readable than before.
* Many more avatars - thanks to everyone who helped!
The avatars are smaller than desired, unfortunately; the latest version of Gource
doesn't let me control that. But they *are* there.
* Captions note some events. I gave up trying to include all Metamath 100
proofs; once we hit ~2014 that becomes far too busy.
No doubt people can disagree about which events are worth noting,
the point is to provide *some* context of what is going on.
* The Metamath logo is on the top right.

Enjoy!

--- David A. Wheeler

[Benoit]

Looks great !

Maybe moving the captions lower-left (instead of lower-center) would make both the captions and the graph more legible (the captions, because they would be left-aligned, and the graph, because it would be less obstructed by the captions).

It's a bit strange that at around 0:01, the image blows out of frame: we lose some information (even if some might like the "big bang effect" this gives).  Maybe Gource has an option "always-within-frame" to prevent this?

Some titles appearing in the video read "TEXT/Text"; maybe "/Text" could be removed, that is, only keep the title of the "Part", not of the "Chapter".  I think this would improve readability.

Finally, maybe you could put some of the information you gave here in the youtube description of the video.

Benoît

[David A. Wheeler]

On Sat, 5 Oct 2019 09:03:45 -0700 (PDT), Benoit <benoit...@gmail.com> wrote:
> Looks great !

Thanks!

> Maybe moving the captions lower-left (instead of lower-center) would make
> both the captions and the graph more legible (the captions, because they
> would be left-aligned, and the graph, because it would be less obstructed
> by the captions).

Good idea. It turns out that I can do that (it's a setting called caption-offset)
and doing that is indeed an improvement.

I'll regenerate the video in a bit.

> It's a bit strange that at around 0:01, the image blows out of frame: we
> lose some information (even if some might like the "big bang effect" this
> gives). Maybe Gource has an option "always-within-frame" to prevent this?

I don't see any way to change it, and I think it's fine anyway. It creates an
interesting "exploding" effect at the beginning.

> Some titles appearing in the video read "TEXT/Text"; maybe "/Text" could be
> removed, that is, only keep the title of the "Part", not of the "Chapter".
> I think this would improve readability.

Sadly, Gource doesn't have a way to control that. Or more accurately, it
has a way to prevent showing the second part, and I use that control, but
sometimes it ignores the control.

I'd have to wallow into the gource source code to change that, and I don't feel like it :-).

> Finally, maybe you could put some of the information you gave here in the
> youtube description of the video.

Definitely!

--- David A. Wheeler

[David A. Wheeler]

Another Gource visualization now available (but not yet publicly listed):

https://youtu.be/MWRbUu0sS_8

I moved the captions to the bottom-left and improved the video description, per comments from Benoit.

Any last comments? Shall we "ship" it to the public?

--- David A. Wheeler

[Norman Megill]

On Saturday, October 5, 2019 at 1:00:27 PM UTC-4, David A. Wheeler wrote:

On Sat, 5 Oct 2019 09:03:45 -0700 (PDT), Benoit wrote:
...

> It's a bit strange that at around 0:01, the image blows out of frame: we
> lose some information (even if some might like the "big bang effect" this
> gives).  Maybe Gource has an option "always-within-frame" to prevent this?

I don't see any way to change it, and I think it's fine anyway. It creates an
interesting "exploding" effect at the beginning.

 

The exploding effect is likely due to the 500+ theorems dated 5-Aug-1993, which is when I 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 my spare time during earlier months, before I kept track of dates.  I don't think it is possible to recover the missing dates.

However, the visual explosion is kind of neat in a way, symbolizing a spark inspiring the creation of Metamath, or something like that.  I think it was around that time when the Metamath language was more or less finalized and implemented in metamath.exe and the 500 proofs translated from an earlier version of the language.  So in a way that's about when they were "added" to set.mm.

Here is some history before 1993:

Around 1990 or 1991, inspired literally by Principia Mathematica, I worked out the proofs of its 193 propositional calculus theorems using the more modern ax-1 through ax-3.  I tried to find the shortest proofs possible directly from axioms, both by hand and with various simple computer search programs, and the result is at http://us.metamath.org/mmsolitaire/pmproofs.txt where there is an open challenge to find shorter proofs.  I found it quite satisfying to see these proofs verified almost instantly, with complete confidence, compared to the many tedious, error-prone hours it would take to check the published proofs by hand.

The idea of formalizing set theory and thus "all of mathematics" developed while I was taking George Boolos' set theory course in spring 1992.  For the homework, I worked out the proofs in great detail (to the point where it may have annoyed him) with a vague idea that someday they would be useful for formalization.

I located a hard-copy of set.mm's predecessor, dated Sep. 1992, called "st.mm" (for "set theory").  It used "$<letter>" keywords but with mostly different names and a different proof format.  While it states axioms and definitions through elementary set theory, it has only 2 proofs, ~ syl and ~ id.

Later in 1992-3 I added more propositional calculus proofs based partly on the pmproofs.txt work, and much of the early set theory was essentially the proofs I wrote down in Boolos' class.  I think I focused on set theory almost immediately, typically adding prop and pred calculus theorems only as they became needed.  (The complete collection of PM proofs was not added until around 2005.)

Norm

[Alexander van der Vekens]

Really great, it's a lot of fun seeing the universe of set.mm expanding...

About the captions: as the video-bar (start/stop, loudspeaker symbol, etc.) is also at the bottom, the text is often hidden behind this bar:

Could the captions be located at the top-left, maybe?

But this is not an important issue - I think the video can be published anyway.

Alexander

[David A. Wheeler]

On Sat, 5 Oct 2019 14:39:25 -0700 (PDT), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:
> Really great, it's a lot of fun seeing the universe of set.mm expanding...

I agree. It's even more obvious in this version, because when there were multiple events for a label it now shows all the events (contributed by, modified by, shortened by, etc.).

> About the captions: as the video-bar (start/stop, loudspeaker symbol, etc.)
> is also at the bottom, the text is often hidden behind this bar:

> Could the captions be located at the top-left, maybe?

Sadly, no. I can only control their horizontal positioning.

--- David A. Wheeler

[David A. Wheeler]

On Sat, 5 Oct 2019 09:03:45 -0700 (PDT), Benoit <benoit...@gmail.com> 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

[Alexander van der Vekens]

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"

Alexander

On Sunday, October 6, 2019 at 12:13:42 AM UTC+2, David A. Wheeler wrote:

[Benoit]

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

[David A. Wheeler]

On Sun, 6 Oct 2019 06:28:48 -0700 (PDT), Benoit <benoit...@gmail.com> 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

[David A. Wheeler]

Here's another revision of the Gource visualization - I think this is the last one:

https://youtu.be/XC1g8FmFcUU

This resolves a problem hinted at by Benoit, which I describe below.

--- David A. Wheeler

==============================

On Sun, 6 Oct 2019 06:28:48 -0700 (PDT), Benoit <benoit...@gmail.com> wrote:
> 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). ...

I double-checked things & discovered that Benoit very much had a point.
The gource animations take some time and that *partly* explains the lag,
but when I rechecked the settings I realized they produced a *big* lag.

Here's a quick explanation of what I fixed.
I wanted the visualization to be a short video, not a movie, so I use:
seconds-per-day=0.01

That's fine by itself, but I originally had this as a setting:
max-file-lag=1

This meant that a new file's display in the visualization could be delayed
by up to 100 days, and that was the problem. I set them to match:
max-file-lag=0.01
and regenerated the video. The "appearance" video takes time,
but it starts on time & I think it more accurately visualizes the data.

If you look at the video you'll see that every second is actually 50 days, not 100.
I generate the videos at 60 fps (the default), then encode them at 30 fps.
That way, I see the videos in half the time. I do this because every
time I tweak a configuration I need to regenerate it & see it;
double-speed generation makes my process faster.
I've seen a *lot* of versions of this video :-).