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.
