Hi Stan, I had a look at the proofs - very impressive results! Especially because we had a global minimization recently, and your method found much shorter proofs nevertheless. I had a closer look at the proofs for the theorems I contributed (these are theorems I contributed in my first year working with Metamath, so I was lacking experience):
* opabbrex: reduction from 12 to 7 essential steps, using ~ssopab2 * 2eluzge0: reduction from 5 to 3 essential steps, using ~nn0uz * elfz0add: reduction from 16 to 10 essential steps, using ~uzaddcl * elfzmlbm: reduction from 33 to 16 essential steps, using ~lesub1dd Observations: * the number of essential steps was almost halved * the usage of only one theorem (indicated above) caused most of the shortening * the proofs are still comprehensible, even better to understand because they are shorter I would really appreciate if you continue your work to find more shortenings using OpenAI. Alexander On Thursday, March 26, 2020 at 5:24:02 PM UTC+1, Stanislas Polu wrote: > > 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/1c23b864-6b53-4ede-a2df-23851315e523%40googlegroups.com.
