Thanks David, >From an ML perspective, this is obviously desirable. We'd be glad to help with that. Do you have a tentative set of theorems that would be particularly interesting to "un-minimize"?
-stan On Fri, Jul 3, 2020 at 6:54 PM David A. Wheeler <[email protected]> wrote: > > As we get more & more shortened proofs (thanks OpenAI!), > I think we should create some unshortened & unminimized > examples of "simple uses of theorems" within set.mm. > These would show how to use simple *general* theorems to get proofs > instead of always minimizing the number of steps. > > Why? Two reasons: > > 1. Examples for humans. For example, there are a lot of simp* theorems like > simp333, > but it's absurd for humans to learn them all. Just use simp (chained) > and then minimize. But if we don't show this in practice, humans won't see > how that works. See the notes in mmnatded.html. > > 2. Examples for ML training. If ML is *only* trained in very specific > uses of theorems, it won't have (m)any examples of "more general > approaches" > where specific cases don't work. Otherwise I fear the ML approaches may > get unnecessarily stuck because they would only have training data > on hyperspecific cases. > > In general I think we *should* prefer proofs with a shorter number of steps. > So far practically every shortened Metamath proof I've seen is no more > complicated, > and is often clearer, than its longer version. That's different from human > "short" proofs, > but I think that's because human short proofs often skip more steps, while by > definition all Metamath proofs *must* show all steps. > But I fear our general preference for short proofs will cause some > information loss, > and this seems like a simple way to counter that. > > I think we have mechanisms in place to make this easy. > They'd be marked with "(Proof modification is discouraged.)" so they'd stick > around. > We could put them in a section (perhaps named "Unminimized examples"?) > near the "Natural deduction examples" with names like "ex-...ALT" > and "(New usage is discouraged)" so they wouldn't be used in other proofs. > Perhaps they should have text like "(Unminimized example)" to hint that it'd > be useful for AI training sets. I don't think we need a horde of them, just a > few. > > --- David A. Wheeler > > -- > 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/E1jrOwt-0006KM-Hk%40rmmprod06.runbox. -- 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_0yuQfrx0BsVajr3_iDofF8umSdnkJOnp7HRUhF%2BCAf4bg%40mail.gmail.com.
