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 :-).
On October 4, 2019 11:20:21 AM PDT, Jim Kingdon <[email protected]> wrote: >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. > >On October 4, 2019 10:33:42 AM PDT, "David A. Wheeler" ><[email protected]> wrote: >>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 >> >>-- >>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/E1iGRSY-0004sp-TT%40rmmprod07.runbox. > >-- >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/7B19B6BB-7A89-432A-8E2C-DD81BC08170B%40panix.com. -- 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/FA65F771-B3D2-47B1-B5CA-EFBB7BBBB953%40panix.com.
