Introduction to Sophize

[Abhishek Chugh]

TL;DR: Sophize is a modern online knowledge platform. We have incorporated the Metamath dataset. Watch this 3 min video if in a hurry.

Hello,

I would like to introduce the Metamath community to Sophize - 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 -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 - 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 - 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 - 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

[Jim Kingdon]

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.

[Abhishek Chugh]

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

[Mario Carneiro]

On Tue, Jul 14, 2020 at 9:06 AM Abhishek Chugh <achu...@gmail.com> 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. 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 kin...@panix.com 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 <achu...@gmail.com> wrote:

TL;DR: Sophize is a modern online knowledge platform. We have incorporated the Metamath dataset. Watch this 3 min video if in a hurry.

Hello,

I would like to introduce the Metamath community to Sophize - 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 -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 - 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 - 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 - 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7e7697f8-b3df-4360-990d-a4a6630d7590n%40googlegroups.com.

[Abhishek Chugh]

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

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

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

-Abhishek

[Mario Carneiro]

On Tue, Jul 14, 2020 at 11:20 AM Abhishek Chugh <achu...@gmail.com> 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

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2596967d-44e6-4135-9a67-f3140846f516n%40googlegroups.com.

[Abhishek Chugh]

> 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!

[David A. Wheeler]

> >>> On Tue, Jul 14, 2020 at 9:06 AM Abhishek Chugh <achu...@gmail.com>
> >>> 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'm *very* supportive of automation for Metamath, and I think everyone else is too.
Almost all Metamath proof assistants have *some* automation built in to them.
In mmj2 there's support for defining automation using JavaScript.
Even the C Metamath implementation's proof assistant has some
very simple automation, e.g., IMPROVE.

The lack of automation really comes down to lack of funding. Until recently people
haven't been paid to develop improved automation for Metamath-based tools,
so the automation implemented in the past has been relatively modest.
This appears to be changing. I presume the OpenAI folks *are* paid, and they've
been developing tools to create Metamath-based proofs.

There is a major difference in how Metamath approaches automation, though.
In Metamath, automated tools are used to find the proof, but what is stored as
the proof is the *actual* exact sequence of axioms & previously-proven
theorems... not just "hints" to an automation system to let it rediscover the proof.

As noted in the Metamath book, in most other tools (like Coq and Isabelle):
> “proofs” are actually programs that guide the program to find a proof, and not
> the proof itself. For example, an Isabelle/HOL proof might apply a step apply
> (blast dest: rearrange reduction). The blast instruction applies an
> automatic tableux prover and returns if it found a sequence of proof steps
> that work... but the sequence is not considered part of the proof.

Put another way, these other tools only store an an *outline*
of a proof (as expressed by various tactics), not the
actual proven steps. This is understandably attractive, because
it's similar to how human proofs are expressed, and at first glance that
approach also seems more flexible (since perhaps rederivation won't be hard
if something small changes).

But the Metamath approach, while different, has some interesting advantages:

* It's easy to modify automation tactics, because doing so won't invalidate any proofs.
Every modification of a Coq or Isabelle tactic risks invalidating past proofs.
* Metamath proofs "stay proved". Many past Coq and Isabelle proofs no longer
work on today's systems, in part because notations and tactics are part of the
program which is changed over time. MPE includes proofs from decades ago,
because the proofs are not hiding in some program's implementation, it's all
spelled out in the database (including the proof itself).
* Metamath proofs are very fast to verify, a few seconds for the entire MPE.
This again helps Metamath proofs "stay proved", because we routinely check
*all* proofs on every change. It would take serious compute power to
recheck all Coq proofs.
* It's easy to have multiple verifiers. MPE is routinely checked by 5 independent
verifiers on every change, making it the formal database with the *strongest*
level of confidence.
* Metamath's approach is in some sense "purer", because absolutely every step
is *shown* to be proven by an axiom or previously-proven step.
Once you see it, it becomes increasingly compelling.

I think Metamath has advantages, and there's no reason more can't be automated.

I hope that helps.

--- David A. Wheeler

[Abhishek Chugh]

> I'm *very* supportive of automation for Metamath, and I think everyone else is too.

That's great! I am going to assume we can get >=5 people pitching in ideas/design and >=3 working on implementation (>10 hrs/week). In a couple of days, I will post a small questionnaire to understand what kind of features folks are looking for in the automation. Following that, I will help organize a design discussion.

> In Metamath, automated tools are used to find the proof, but what is stored as the proof is the *actual* exact sequence of axioms & previously-proven theorems... not just "hints" to an automation system to let it rediscover the proof.

My goal is to make every proof/argument available and scrutinize-able by my users. So, Metamath's property of storing actual proof along with the fact that the proofs can be read by casual readers (with some Math background) are the main reasons I was attracted to Metamath instead of other systems in the first place.

> I think Metamath has advantages, and there's no reason more can't be automated.

Let's automate more then!