Perhaps we should create some unshortened "simple examples"

[David A. Wheeler]

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

[Stanislas Polu]

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

> --
> 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/E1jrOwt-0006KM-Hk%40rmmprod06.runbox.

[David A. Wheeler]

On July 4, 2020 5:41:11 PM EDT, 'Stanislas Polu' via Metamath <meta...@googlegroups.com> wrote:
>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"?

Some chained uses of simp instead of specialized therems like simp333 would be a start I think.

To be honest, you might be best positioned to answer that question. Have you noticed any specializations that might eventually lead to never using general applications?

I don't think we need to start with a large section. Just add a section with a few examples, and then people can propose additions as we go.


--- David A.Wheeler