Thanks David, Let me reach out to you by email.
> 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]. Good point. To anybody else looking to contact me, my email is [email protected]. Best, -stan On Fri, Jul 3, 2020 at 1:08 AM David Starner <[email protected]> wrote: > > 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. -- 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_0z-CRvbOveEKyZF9tN2%2BsWRpqEHLHj_0hnJhEcMEfnEdw%40mail.gmail.com.
