> The MM1 server is written in Rust and can likely be compiled to webassembly for web integration. Most likely the most convenient protocol would be either the LSP server (communicating on standard in/out) or through C bindings with MM1 being compiled into a dynamic library. If you already have a server that's even better (any language will do). All I need for the server is to be able to handle HTTP POST requests (in JSON format). Once that's done, we can have a sample proof generator up in less than a day. Hit me up whenever you want to do that.
With regard to an organized effort for Metamath automation, Metamath users can consider this an invitation for a design discussion. If we can get a few people to sign up, I will set things up. Cheers! On Tuesday, July 14, 2020 at 9:53:46 PM UTC+5:30 [email protected] wrote: > On Tue, Jul 14, 2020 at 11:20 AM Abhishek Chugh <[email protected]> wrote: > >> > I believe the only reason it is traditionally lacking, compared to >> other proof assistants, is lack of concerted effort in that direction. >> I see. From what I understand, Metamath is run mostly by volunteers as a >> hobby and perhaps you are the only one here whose involvement is directly >> related to their day job. I won't have the time to implement everything >> myself, but I wouldn't mind leading a design and a discussion around making >> better Metamath automation. We can bring together the OpenAI folks and any >> volunteers who want to participate from this group. >> > > I think you are right about that. (Even my "day job" is mostly Lean, not > metamath. I've managed to swing MM0 into a dissertation project so I have > more time to work on that specifically but I have some particular features > to prioritize there.) > > > 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. >> Now that I have integrated Metamath on the platform, MM1 should also be >> simple enough to integrate on the platform. Can you get the mm1 code to run >> on JVM or python environment? You would get all features I have mentioned >> in the post and dedicated webpages for the work you've done. Let me know if >> you are interested. >> > > The MM1 server is written in Rust and can likely be compiled to > webassembly for web integration. Most likely the most convenient protocol > would be either the LSP server (communicating on standard in/out) or > through C bindings with MM1 being compiled into a dynamic library. > > > 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. >> Yes, I am building on MMJ2's features. I will open an issue today. >> Automatically figuring out substitutions needed should be useful for the >> proof assistant too. >> > > Unification is definitely done by mmj2 in the course of its work, I'm just > not sure it exposes a very convenient or reusable API for programmatic use. > The core function doing unification for a proof step appears to be > https://github.com/digama0/mmj2/blob/fc5c2427d3d0e0f56c392ae2603ca362dfec3e02/src/mmj/pa/ProofUnifier.java#L896 > > (which calls methods on ProofTree that do the actual work). > > Mario > > >> -Abhishek >> On Tuesday, July 14, 2020 at 8:08:46 PM UTC+5:30 [email protected] wrote: >> >>> 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/2596967d-44e6-4135-9a67-f3140846f516n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/2596967d-44e6-4135-9a67-f3140846f516n%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/2e79426b-952d-4cf2-ab3b-0f0d35677f46n%40googlegroups.com.
