On Tue, Jul 14, 2020 at 9:06 AM Abhishek Chugh <[email protected]> wrote:
> 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! > I've always been very supportive of automation in regards to metamath proofs. I believe the only reason it is traditionally lacking, compared to other proof assistants, is lack of concerted effort in that direction. The fact that verifiers and proof assistants are decentralized also contributes to a lack of big automation since the work is more distributed. But I think the winds are changing, and there are now several projects that use some significant automation around metamath, like the OpenAI prover. My own pet project MM1 has been a reimagining of metamath in an environment with proper metaprogramming / tactic support, based on systems like the Lean theorem prover. > 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 will note that mmj2 actually already has automation capable of handling numerical calculation and closure proofs like these. I went for a JS-based macro language for implementing these kinds of tactics. See https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js#L117-L324 for the implementation of an arithmetic prover, not unlike the one you have implemented in pure java. MM1 also has an arithmetic prover (working in peano arithmetic, not set.mm) that is implemented in the MM1 metaprogramming language: https://github.com/digama0/mm0/blob/master/examples/peano_hex.mm1 , and I believe that this approach is a much better foundation for writing proof producing algorithms. > 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? > I take it that you are linking directly to mmj2? I'm not sure this is very well supported ATM. You can open an issue for this but I won't be able to get to it for a while. Mario > > 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 > <https://groups.google.com/d/msgid/metamath/7e7697f8-b3df-4360-990d-a4a6630d7590n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsJSkJhi4WK-Cp9iopaVd80wGQ%3DxyyEGyi_NUd_ZrZoaw%40mail.gmail.com.
