OpenAI Proof Assistant for Metamath

[Stanislas Polu]

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

[David A. Wheeler]

This looks very cool, thanks for posting about it here!

I understand that the system has to be trained on a particular version of set.mm. It seems to me that it would not be that difficult to create a difference file that identified new theorems, and perhaps new definitions, that could be fed into this tool. Then it could automatically work on current versions of set.mm even though it had been trained on older versions.

Thoughts?
--- David A.Wheeler

[Stanislas Polu]

> I understand that the system has to be trained on a particular version of set.mm. It seems to me that it would not be that difficult to create a difference file that identified new theorems, and perhaps new definitions, that could be fed into this tool. Then it could automatically work on current versions of set.mm even though it had been trained on older versions.

Totally, I think ideally we let you specify a commit on set.mm or, if
there is usage, bite the bullet and simply make the tool stateful and
let you upload your own .mm files to work from.

This would solve the "underlying kernel versioning" problem entirely.
As far as training is concerned, it would be a bit more involved to
adaptively train on diffs of set.mm but not completely out of reach.

-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 metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/30A4B5BD-CE3E-45B6-A2B1-836F071A4EA4%40dwheeler.com.

[David Starner]

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 prosf...@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 metamath+u...@googlegroups.com.

> 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)

[David A. Wheeler]

>If you are interested in getting access, just send me an email and
>I’ll happily get you all set-up.

I'm definitely interested in access! My email is
dwheeler AT dwheeler DOT com.


--- David A.Wheeler

[Stanislas Polu]

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 prosf...@gmail.com.

Good point. To anybody else looking to contact me, my email is sp...@openai.com.

Best,

-stan

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj7w2o2nLqdf9BrEwEgjV1Sj1QDbWXb5VUMsYQaChxavLA%40mail.gmail.com.

[Stanislas Polu]

(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

[Thierry Arnoux]

Hi all,

This is to highlight that I've used Stan's OpenAI based assistant to prove ~ gsummptres.
Once I had manually filled-in the initial (less-trivial)  first step, I found the tool's suggestions were quite good.

Even though we usually don't include this kind of information, I've made a note in the comments about the fact that I've used OpenAI's prover, as I don't know if anyone else has published any other theorem proven with that tool.

BR,
_
Thierry

[Stanislas Polu]

This is great to hear! I think this is indeed the first proof published designed with assistance of our tool. Thanks for the shoutout in your comment \o/

-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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7bae784d-6ebe-b29e-d7db-3fa5f7144fc4%40gmx.net.

[Jon P]

Hi Thierry,

That's is very nice progress! I have been playing around with the tool and I like it, it seems to have an obsession with eqtri however that also seems to work out quite often so it's probably right to think highly of it. I have done all the practice problems and I'm searching for some theorems I might be able to prove with it. 

One thing I noticed doing Filip's practice problems is that the 4th problem of his is much more difficult than the others and I have not yet been able to solve it using suggestions from the tool. I found this a bit surprising. My solutions are here if anyone is also trying the practice problems. I don't know if anyone else has found anything similar.

[Stanislas Polu]

Hi Jon!

I think eqtri is at least a plausible way to go here.

I think something along these lines could get you there? I entered the first eqtri manually here as the model fails to make useful progress early on.

https://mmproofassistant.azurewebsites.net/#eJydV9uSojAQ/ZUUT1qDbiDIxap9UJ92q+YLZueB6xjuEmBE13/fgEIiIqvWVE2FDNPndJ/TnXAUcO5GRFgehX1i+Dqy8rB+yKvUFZZCaFpuKIhCamZunAvLuAhDUSC5Sf+p2RCiapZmSeLRl7BDn1kUUQgT08Hxl7D0zJC4J1EIHB8rhl6WHITjEjvDaY6TeBRoskniPMNWkbsOsCoggsXsdxHOZCjD+bSFZwgUjqQoN5xQ5eG2VZrkW5dgMoq2Au4cbDZtWBbp/FpBKyYkqRvXMKUXbO1gGzsczFdijtdtAlbgJ5DAjz9/wJquZDC9qZgo2EkYmilxnW6nocMQB+iQnSWnplkYz2e97mXdRRqAcQ0j0mB2cJ+HqXN/o1lPad6oBWPxBsB2FQmlg6fkr4BNAAL7OcWcUtQJrTR9qMFreK2FZwgD8FIi6Xak7hEHn5t2jm0O+kaVlsHHB/g7A+m2+U3A52e9mNQbtfh0ZwqOx/pxefHE6dRsELpxtsbpVHuj6cWlkEZoLuOWN6PW502NaYYFpQrnECqqApGsaCoyVGUBNZpUluulISsL/b5tb6Kz9qA8H/crgxooLgpI6GF5O9I+d3k05XmcB4Ma4CFj0yPld/Q1KnI/lWuR67qs60VNbHORetWsqaKrRuGzuhu6bpVe0/UEaGDWupM1SP1zpb67o0OwFZ9RHhNfliUVSoZiIEPXDaggmqznB3YWBAtppOj96Lz49+k+rgbjMKCGgwMf+gmBLxAcqeVTtmUcBgjGBYx3qPTgqF36Ifp2aebt2TDdcsOWE7r/Rjdq4qtucqzA7DI9O1tpV1a6Sfzac5ydSGGZjpPhzlIsrRFLIU2XEISSpC00SUe6Suth+8VeSv1oNyJYP3hbDa07dx5UhoENWWcfJS4OUvUFJgO1e5IaQx90tR99RxgaL1CTnmbSgQ0w0SzV+TYNXL1UpIEyvVFrtSfqgwQZhwGCpozzA4qxNdpf/RDPjuORVPiGuryEen/cXDrv3nxmOYw0k6Ip9FyWJWgodE7LqkKTVzwjLHFcpiPq9IM/pM5tKo/LxUgNyAUr4oXlYT82r//LGL3mI4Z9Q+xUK1MlBYX5uPo2YR8K4vXtnrvz8ldS/n7IX/T4mwl/N+DPJv6g4w8Evr/4icaPEL6JebPzteSF4WvBrjuf4qV3fsVp0V2Tmw+39/fz4+kfOGw5mQ==

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/50a189c7-3f29-40ef-bd32-ee6246c2eceeo%40googlegroups.com.

[Stanislas Polu]

Hi Jon,

Here's a proof for the A=1 part. The other part should be similar. It's a bit tedious and you need to hint the model on a few eqtrd. I also had to hint `mvlladdd` to it by doing a search for it.

Hope it helps!

-stan

[Stanislas Polu]

Also note that our models are still not very good at these kinds of
expression manipulations / basic algebra (there are not many of them
in set.mm).

But we're working hard at making them much better at it. Will keep you
posted when we update the underlying model in that direction.

Best,

-stan

[Jon P]

Wow this is really cool, thanks Stan. Also thanks for letting me use the tool, my friends are all suitably impressed :)

[Aleksandras Maliuginas]

Hi, is it still alive? Where to get access to try this tool? 

[Jon P]

So the last I heard they had shut down the tool itself due to lack of use and I think the team inside openAI has moved on to working on Lean. I think they are contactable on Lean's Zulip chat: https://leanprover.zulipchat.com/