[Metamath] Re: Building Metamath Automation Framework

[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

On Tuesday, July 21, 2020 at 4:55:31 PM UTC+5:30 drjonp...@gmail.com wrote:

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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/f53dc171-4a8f-4223-ae36-86aebbd45993n%40googlegroups.com.

[Metamath] Re: Building Metamath Automation Framework

[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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/56d1d4f7-407e-43e1-9f5c-6fe50b16b111o%40googlegroups.com.

[Metamath] Re: Building Metamath Automation Framework

[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.
On Monday, July 20, 2020 at 5:43:36 PM UTC+5:30 Abhishek Chugh wrote:

> 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.
>
>
> On Saturday, July 18, 2020 at 10:26:16 AM UTC+5:30 Abhishek Chugh wrote:
>
>> 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
>>
>

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/80e442ea-a021-4061-9642-4b8c4a4a3db1n%40googlegroups.com.

[Metamath] Re: Building Metamath Automation Framework

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


On Saturday, July 18, 2020 at 10:26:16 AM UTC+5:30 Abhishek Chugh wrote:

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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/bf604187-b164-487e-a5f1-8b4f51b66572n%40googlegroups.com.

[Metamath] Building Metamath Automation Framework

[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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/97121fbb-ef4d-41da-bfe3-3c514477e7f9o%40googlegroups.com.

[Metamath] 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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/3cafc922-0eb4-4425-aeb5-654f6e81ca4bn%40googlegroups.com.

Re: [Metamath] Automation

[Giovanni Mascellani]

Hi,

Il 09/11/19 12:27, 'Filip Cernatescu' via Metamath ha scritto:
> Automatic prover for a+b,a-b,a×b,a/b, ab... it will be necessary?

Maybe not necessary, but I believe it would be good to have automated
provers for everything that can be automated. Unfortunately not any
problem arising in real number (or integer number) theories can be
decided automatically, but some can. Z3 can prove statements (and emit
related proofs) in a range of theories, also using real numbers, and
eventually I would like to be able to convert those to Metamath.

Giovanni.
-- 
Giovanni Mascellani 
Postdoc researcher - Université Libre de Bruxelles

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/cc9dbcc0-c89d-ef94-b1d9-daa78c35cc64%40gmail.com.


signature.asc
Description: OpenPGP digital signature