I'm really intersted by this. I'll look at it when I can (in some
months) as I am overwhelmed right now.
But this is definetely on my to look at list because this will be really
useful for my project.
Many thanks for the link.
Best regards,
Olivier
Le 26/03/2020 à 17:23, 'Stanislas Polu' via Metamath a écrit :
Hi!
At OpenAI we've been exploring the use of deep learning for formal
math for the past couple months. We've worked a lot with Metamath
whose simplicity makes it very amenable to deep learning.
Today, I submitted a PR containing a sample of proofs that were found
by our models and that are substantially shorter than their human
curated counterparts:
https://github.com/metamath/set.mm/pull/1547
We're very curious to hear from the community on whether this is
useful. Additionally, if the authors of the original proofs shortened
by this PR have qualitative feedback on the proposed versions, we'd be
keen on hearing from them as well, obviously.
As mentioned in the PR the models were run on a sample of ~1k proofs
from set.mm so we could probably get 45 times as many shorter proofs
if there is interest for it!
Looking forward to your feedback and comments.
-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/adfb3b21-9e80-b9da-b1d5-137757671a5b%40gmail.com.
