I'd like access to this. Unfortunately, Google Groups obscures the original email address, so I don't see how to email you directly. My address is [email protected].
On Thu, Jul 2, 2020 at 1:26 AM 'Stanislas Polu' via Metamath <[email protected]> wrote: > > 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. -- The standard is written in English . If you have trouble understanding a particular section, read it again and again and again . . . Sit up straight. Eat your vegetables. Do not mumble. -- _Pascal_, ISO 7185 (1991) -- 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/CAMZ%3Dzj7w2o2nLqdf9BrEwEgjV1Sj1QDbWXb5VUMsYQaChxavLA%40mail.gmail.com.
