Hi! OpenAI has lately been exploring the use of deep learning for formal maths in the context of Metamath. As part of this project, we’ve built an online proof assistant to interact with our models and we’re excited to share it with the Metamath community.
Ideally, the proof assistant will help you be more productive building your Metamath proofs while helping us improve our model’s accuracy at the same time. But in any case, we hope you'll also just have fun using it! This is a very early-stage release, so we’re limiting access to the Metamath community for now to get an initial round of feedback. The spirit of the terms of use of the proof assistant is that: (i) what is produced with the proof assistant can be shared back to set.mm (under CC0 license). (ii) we can use your usage of the proof assistant to improve our models. Here’s a short video demonstrating how it works: https://vimeo.com/434053884/1e15e93ec6 We also wrote a tutorial for the proof assistant (also serving as a short introduction to Metamath for people without priori knowledge of it): https://cdn.openai.com/openai_proof_assistant_tutorial.pdf The proof assistant is based on a fixed version of set.mm (currently `fbf3931`). For anything but definitions, you can circumvent that limitation by reproving missing lemmas and linking them from your proofs as demonstrated in the tutorial. The set.mm version impacts the training of the model as well as the underlying kernel. In the future we hope to allow custom set.mm files to be loaded in the kernel even if the model won’t be trained on them directly, as well as to retrain our models periodically. While this is a limitation today, it also makes the proof assistant very simple to get started with for beginners as well as anyone simply interested in better understanding the capabilities of our models. The proof assistant is currently hosted at (subject to change): https://mmproofassistant.azurewebsites.net/ If you are interested in getting access, just send me an email and I’ll happily get you all set-up. Looking forward to your proofs, comments and feedback! -stan -- 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/CACZd_0y1UVbknTX2%3DrKgKE5GHpZ2d332h%3DkT8XspJ2%2B7EPyCcA%40mail.gmail.com.
