Building Metamath Automation Framework

[Abhishek Chugh]

Dear Metamath Community,

In the course of a conversation with Mario and David, I came to understand that the community is quite supportive of automation efforts in Metamath and a concerted effort could be quite productive. With the OpenAI folks developing excellent tools for Metamath, this is possibly the best time to forge foundations for a general automation framework.

Thus, I am organizing a project to help develop better automation for Metamath. I hope several members of the community will be able to contribute to this project in one way or another. To kickstart the discussions, I will post a simple proposal in a couple of days. It will be similar in spirit to the Metmamath automation I have developed for Sophize. 

In the meantime, please help us understand your interests, technical familiarity, and expectations by filling in the following simple survey:

https://docs.google.com/forms/d/e/1FAIpQLSfTjuVg-kMj8N2YeWo6O4jOH17EytisLR_pXby6fl3oTxd81A/viewform?usp=sf_link

-Abhishek

[Abhishek Chugh]

FRIENDLY REMINDER: We are almost ready to begin our discussions. Please fill in the survey so that we can get started without delays.

https://docs.google.com/forms/d/e/1FAIpQLSfTjuVg-kMj8N2YeWo6O4jOH17EytisLR_pXby6fl3oTxd81A/viewform?usp=sf_link

[Abhishek Chugh]

Hi all,

The project is now up. Please start contributing here:

https://sophize.org/s/metamath/J_automation

A little info about the interface:

The interface crystallizes Profs. Terry Tao and Timothy Gowers vision for large scale online collaborations. We have implemented all features they wanted (see this and this) and more. Make sure you can find the index of pages at the top of the page (see clip). Check the help page for more info.

[Abhishek Chugh]

Hey folks, there hasn't been any activity on the project. Are you facing technical issues accessing the content or contributing to it?

From the survey, I understand that the community is interested in this work. But, did the content/format in the project not meet the expectations? Let me know if you guys would like to see some changes.

[Jon P]

Hey. 

I just wanted to say that I think it's awesome you want to work on a new tool and maybe recruit people to a team, that's great, more work on mm is lovely to see.

For me personally I'm afraid I don't have any energy for contributing at the moment. I wonder if maybe you are running in the same issue with other people, there is a general sense of enthusiasm for the project and also people's lives are busy, we've all got a lot of covid stress I'm sure and so I think it can be a challenge to convince people to commit actual resources. Discussion is easy, real work is much harder and I can understand why people are hesitant to commit to a new thing.

Good luck with it, I hope you find the right people to work with.

Jon

[Abhishek Chugh]

Thanks for the message, Jon. It is always nice to hear the thoughts of members of the community.

Mario and David also warned me to not look for time any commitments early-on. So, I tried to make the project so that folks can make small contributions. But, I think that the different pages of the project may have led people to think that its a lot of work to even get started.

So let me focus on just one fun, simple, and very useful proposal. The goal here is to create a spec in plain-text or metamath language for storing automation info. No code, no prerequisites, just looking for simple ideas. Once we get the spec, OpenAI folks can make quite an impact by using their AI techniques to fill in the automation info.  Details are here.

Even with this, I think you are right Jon about people being busy and COVID obviously makes things harder. So, I am not getting my hopes up too high. But, I think people will find it fun to come up with an automation spec.

Abhishek