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/2d234a16-f767-407c-a538-323605cc0292o%40googlegroups.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/037DCCDA-E8FE-464D-BE53-4E2202E5AEC0%40panix.com.
