(Still scrambled when accessed from the web. You can find my email at the top of the tutorial[0])
-stan [0] https://cdn.openai.com/openai_proof_assistant_tutorial.pdf On Fri, Jul 3, 2020 at 8:16 AM Stanislas Polu <[email protected]> wrote: > > 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_0xPU7HRr5-ADmcOMbxLPPP-wR3iaUR1aDVX8%3D_iKBXOyQ%40mail.gmail.com.
