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.
