*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.

Reply via email to