Thanks Jim. You have a sharp eye for detail. I have updated the correction in the subtitles for future viewers.
I would also like to understand how the community feels about automated proof generation. From what I read in some academic papers - lack of automation seems to be an often highlighted shortcoming of Metamath compared to other proof verifiers/assistants. I am not 100% sure this theoretically makes Metamath prover "Poincaré Principle" compliant, but all calculations can be very easily automated. We can certainly build a Wolfram Alpha-type interface where results have fully formal Metamath proofs! The proof generating machines are hosted on a server I have dedicated for Metamath. The code extends on MMJ2. The core code for automatically generating proofs like "|- ; 1 6 e. NN" is in these 23 lines <https://github.com/Sophize/METAMATH_SERVER/blob/master/src/main/java/org/sophize/metamath/server/machines/NNClosureMachine.java#L93>. I will do a video or write detailed documentation for the community so that they can easily write more automation like this. I am also looking for some help with improving the automation architecture. Specifically, how to automatically figure out what substitutions are needed on a metamath theorem to produce a given statement in MMJ2. We may be able to then produce proof machines using just text files! Also a few other things like running a verifier on the resulting proof before sending it out to the webpage. Can someone lend me a hand with this work? Thanks, Abhishek On Tuesday, July 14, 2020 at 3:09:28 AM UTC+5:30 [email protected] wrote: > This does look interesting, for example as a tool for comparing set.mm > and iset.mm. > > One nitpick: the voiceover in Exploring the Metamath dataset in place > refers to _V as the universal set, but universal class is more correct, > because it is a proper class. > > > On July 13, 2020 10:35:24 AM PDT, Abhishek Chugh <[email protected]> > wrote: >> >> *TL;DR: Sophize is a modern online knowledge platform. We have >> incorporated the Metamath dataset. Watch this 3 min video >> <https://youtu.be/RgvSk8wO6GY> if in a hurry.* >> >> Hello, >> >> I would like to introduce the Metamath community to *Sophize >> <https://sophize.org/docs/tour/intro>* - a non-profit platform sharing >> and developing and sharing knowledge. The long-term goal of Sophize is >> to let people know of the rational truth that is derived from their chosen >> beliefs. You can pick your beliefs from places like Principia Mathematica, >> Einstein's book on relativity, the European constitution, or even the >> Talmud. Sophize will let you know what is true but also point out any >> inconsistencies in your understanding of the World. To do this it is going >> to utilize sound arguments (machine verifiable in the best case) that can >> be reused in as many belief systems as possible. >> >> Currently, we are focused on incorporating Mathematical knowledge from >> various sources. Thanks to the elegant simplicity of the Metamath language >> it is the first formal system that we incorporated into the platform. >> >> There is a lot I would like to share and discuss with you. But let me >> begin with a brief overview of the major features of the platform. The >> following videos will help you understand what we offer specifically to the >> Metamath community. >> >> - *Data Organization Model <https://youtu.be/1oS5K-qak68>* -The data >> organization model that brings to life Sophize's vision of revealing >> rational truth to its users - tailored to their beliefs. For mathematics, >> this model helps you look at rigorous proofs from different foundations. >> >> >> - Proof Generating Machines <https://youtu.be/5J_b8VnnL4k> - Helps to >> provide proof for the infinite possible propositions. Metamath has proofs >> of "2+2=4" but what if I needed proof of '343+789=1132'. >> >> >> - *Smart Articles <https://youtu.be/MODMQj67pPo>* - Informal texts - >> like books and research papers - are easier to read and understand (for >> their intended audiences). Formal databases - like Mizar, Metamath, Lean >> - >> are fully detailed and their proofs are beyond reproach. Smart articles >> are >> intended to bring the best of these two worlds together - to help users >> easily understand the content and also scrutinize every last detail when >> they need to. >> >> >> - Exploring the Metamath dataset <https://youtu.be/j0ZE-K3REcI> - >> This video will help in getting familiarized with the user interface we >> are >> developing. >> >> Please make sure to turn on the captions (subtitles) to make it easier to >> follow the videos. Also, check the description to see live links of the >> pages in the videos. >> >> The platform is in the early stages of development. We are looking for >> your help and feedback to create an open and inclusive state-of-the-art >> Mathematical library. >> >> Thanks, >> Abhishek Chugh >> >> -- 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/7e7697f8-b3df-4360-990d-a4a6630d7590n%40googlegroups.com.
