Major Metamath set.mm past events?

[David A. Wheeler]

What are some major Metamath set.mm past events?

At the very least I think they are:
* Each of the Metamath 100 proofs
* The definition of the decimal constructor df-dec , since that let us (finally) easily write longer integers in base 10.
* The definition of Tarskian geometry using extensible structures df-trkg ; there was previous work of course, but this work seems to have finally gotten geometry "over the hump".

If there are others, please post and/or email to me.

I plan to soon regenerate my Gource visualization of set.mm history (using newer avatars, an improved program for identifying events, and some set.mm history cleanups). As part of that, I intend to add notes when a "major event" happens.

However, that means I have to create a file with a list of such events :-).

Thanks!

--- David A. Wheeler

[Jim Kingdon]

The introduction of http://us2.metamath.org/mpeuni/df-c.html

The introduction of http://us2.metamath.org/mpeuni/df-pi.html

I'm not sure whether these are the exact right places to draw lines, and whether they coincide with Top 100 proofs anyway, but they are examples of being able to do "real" math as opposed to just logic.

[Jim Kingdon]

Oh and I suppose I should immodestly mention the addition of http://us2.metamath.org/mpeuni/taupi.html . But that's just me trying to keep up my https://tauday.com creds, everyone will make up their own mind about that one :-).

[David A. Wheeler]

On Fri, 04 Oct 2019 11:24:43 -0700, Jim Kingdon <kin...@panix.com> wrote:
> Oh and I suppose I should immodestly mention the addition of http://us2.metamath.org/mpeuni/taupi.html . But that's just me trying to keep up my https://tauday.com creds, everyone will make up their own mind about that one :-).

I see the advantages of tau, but I think I'll avoid claiming that as a key event :-).

> On October 4, 2019 11:20:21 AM PDT, Jim Kingdon <kin...@panix.com> wrote:
> >The introduction of http://us2.metamath.org/mpeuni/df-c.html
> >The introduction of http://us2.metamath.org/mpeuni/df-pi.html

Those are excellent examples.

df-c has a useful date. According to set.mm,
df-c was contributed by NM on 22-Feb-1996 as df-c $a |- CC = ( R. X. R. ) $.
That is consistent with the git repo; the first instance I can find is in commit
85655124fa08f87bb77112eb4035b48feb12c723
(stable release, archive name set.mm.1998-03-16-from-vax).

df-pi is trickier to date. Paul Chapman created a definition 23-Jan-2008,
but a previous and different definition of df-pi was created
(presumably by Norman Megill) between 2004-09-27 and 2007-04-29. Details below.
Suggestions on how to date the *first* instance of df-pi are welcome.

--- David A. Wheeler

============= DETAILS ====================




Here's what set.mm currently says about df-pi:

$( Define pi = 3.14159..., which is the smallest positive number whose sine
is zero. Definition of pi in [Gleason] p. 311. (We use the inverse of
less-than, " ` ``' < ` ", to turn supremum into infimum; currently we
don't have infimum defined separately.) (Contributed by Paul Chapman,
23-Jan-2008.) $)
df-pi $a |- _pi = sup ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , `' < ) $.


However, the first commit with *any* df-pi in the git repo is
commit ba18c14ef9713308a7efe1dfbc8049975f52f56a
(stable release, archive name set.mm.2007-04-29-grothprim) which says:

$( Define pi = 3.14159..., which is the smallest positive number whose sine
is zero. (Note that the argument " ` ``' < ` " turns supremum into
infimum; currently we don't have infimum defined separately.) $)
df-pi $a |- pi =
sup ( { x e. RR | ( 0 < x /\ ( sin ` x ) = 0 ) } , RR , `' < ) $.
$}

The previous commit c55adffeaab4685ce49f662c301a4b518b9438e6
(stable release, archive name set.mm.2004-09-27-card) does *not* have df-pi.

[Norman Megill]

On Friday, October 4, 2019 at 6:05:57 PM UTC-4, David A. Wheeler wrote:

Here's what set.mm currently says about df-pi:

    $( Define pi = 3.14159..., which is the smallest positive number whose sine
       is zero.  Definition of pi in [Gleason] p. 311.  (We use the inverse of
       less-than, " ` ``' < ` ", to turn supremum into infimum; currently we
       don't have infimum defined separately.)  (Contributed by Paul Chapman,
       23-Jan-2008.) $)
    df-pi $a |- _pi = sup ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , `' < ) $.


However, the first commit with *any* df-pi in the git repo is
commit ba18c14ef9713308a7efe1dfbc8049975f52f56a
(stable release, archive name set.mm.2007-04-29-grothprim) which says:

    $( Define pi = 3.14159..., which is the smallest positive number whose sine
       is zero.   (Note that the argument " ` ``' < ` " turns supremum into
       infimum; currently we don't have infimum defined separately.) $)
    df-pi $a |- pi =
          sup ( { x e. RR | ( 0 < x /\ ( sin ` x ) = 0 ) } , RR , `' < ) $.
  $}

The previous commit c55adffeaab4685ce49f662c301a4b518b9438e6
(stable release, archive name set.mm.2004-09-27-card) does *not* have df-pi.

I defined pi earlier, but I don't think there were any theorems using that definition, so it doesn't really count.  Use Paul's version.
 
Norm

[David A. Wheeler]

On October 4, 2019 9:32:33 PM EDT, Norman Megill <n...@alum.mit.edu> wrote:
>
>I defined pi earlier, but I don't think there were any theorems using
>that
>definition, so it doesn't really count. Use Paul's version.
>
>Norm

Instead of pi, let's use cos. That one has a much simpler history.

Definition df-cos defines the cosine function. (Contributed by NM, 14-Mar-2005.)



--- David A.Wheeler

[Jim Kingdon]

On October 4, 2019 3:05:55 PM PDT, "David A. Wheeler" <dwhe...@dwheeler.com> wrote:
>I see the advantages of tau, but I think I'll avoid claiming that as a
>key event :-).

Drat! I'll need to keep searching for converts elsewhere.

As for the idea of using the introduction of cosine (given the somewhat complicated history around pi), that seems good.

Oh and at the risk of making more work for you, any plans to do a similar visualization for iset.mm? It might be a bit hard to do it solely off "Contributed by" dates, though (given that the relevant date might be the date of a copy-paste from set.mm to iset.mm). On the plus side, the git history goes back pretty darn close to the beginning (I think it was when I wanted to start contributing that we put it in the main set.mm repo, there might have been some kind of branch or something before that but I'm not sure it led to a useful git history). Hmm, maybe the date from git and the authorship from the Contributed by line? I suppose these issues are reason enough to focus on set.mm for this for now.

[David A. Wheeler]

On October 5, 2019 1:08:12 AM EDT, Jim Kingdon <kin...@panix.com> wrote:

>Oh and at the risk of making more work for you, any plans to do a
>similar visualization for iset.mm?

I have definitely thought about it, but I think that will require a completely different approach.

For set.mm I use the dates within the current set.mm file. As you noted, for iset.mm that won't work, since those dates are often a copy-paste from set.mm (many predate iset.mm).

> On the plus
>side, the git history goes back pretty darn close to the beginning...

>Hmm, maybe the date from git and the authorship from the Contributed by
>line?

That is possible. I think it might be more accurate to credit both the contributed by person AND the git committer if they are different. The gource input format has, in each line, a timestamp, user, and "pathname" being changed. Multiple lines can have the same timestamp and "pathname".

However, that is such a different approach that I think new code would have to be written to compute it. It isn't just a tweak that can be added to the current code.

> I suppose these issues are reason enough to focus on set.mm for
>this for now.

My thoughts exactly.


--- David A.Wheeler