AGI research on metamath and grant proposals

[Jon P]

Hello everyone, hope this is a reasonable thing to post.

I saw this call for grant proposals the other day:

https://astralcodexten.substack.com/p/apply-for-an-acx-grant

and I wondered if metamath might be eligible as a thing to work on. Looking at the list of goals a couple are

* move forward innovative and potentially socially beneficial technologies and ideas, even if these are very speculative.

* help understand and prepare for potentially disruptive future events, like pandemics or the advent of AGI

and I also noticed it's not just for the grants on that page but it's possible for the proposals to be more widely submitted to people who want to give money.

And it was interesting to see metamath mentioned in this AGI safety discussion (it's quite long so ctrl+f for metamath is probably the easiest way to see what is said):

https://www.greaterwrong.com/posts/CpvyhFy9WvCNsifkY/discussion-with-eliezer-yudkowsky-on-agi-interventions

I think maybe there are people out there who would be interested in contributing money to help with building out the database or maybe with the community verifier etc. I think it might really help with pitching if the topics which people wanted to add might be things like: reasoning about Neural Networks (there are some theoretical properties listed here for instance https://en.wikipedia.org/wiki/Artificial_neural_network#Theoretical_properties ), reasoning about computer systems and complexity classes, reasoning about code or algorithms etc. I'm not sure how well these topics fit in to the ZFC database but I imagine there are some results which do which would be interesting to formalise.

I don't think I can help so much (though this is all interesting to me) so I don't think it would be for me exactly, but it might be possible to get some money to pay for maybe one of the regular contributors to go full time with metamath. That might speed up development a bit and maybe help with a snowball effect where more gets done which attracts more attention etc.

I have thought for a while that formal systems, as in agents which can reason about their own code, are one of the best avenues for making AI systems which can be formally controlled, and yeah I wanted to kind of post about that in case anyone else is interested too. If there were a section of the database which had formal results about Artificial Neural Networks in that might make a nice foundation for people wanting to research in that area.

For instance Mario I know you've done a lot of work in that direction with MM0 and maybe some help for you to develop that might be interesting.