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 -- 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/c071d2a1-2bfd-47cc-8306-19df45647895%40googlegroups.com.
