On Sat, 5 Oct 2019 09:03:45 -0700 (PDT), Benoit <[email protected]> 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/E1iGsJ2-00066W-Ez%40rmmprod07.runbox.
