On Saturday, July 9, 2022 at 4:05:20 PM UTC+2 Benoit wrote:
> * As you said, there should still be some pondering before adding a
> theorem, even with a high score. A possibility is that a theorem appears
> in this list because a proof pattern occurs often. It could be that this
> proof pattern can be shortened in other ways, but if the theorem in the
> list is added, the resulting shortened proofs will not allow this kind of
> proof inspection. Of course it's not specific to the present list: the
> more lemmas are used in a proof, the more difficult a global minimization
> is. It's not necessarily bad, and there's always a balance to find.
> Actually, I would generally prefer more reused lemmas, making for an often
> clearer proof, over a shorter but more cryptic proof. I guess this has
> similarities with using a high-level language versus completely optimized
> but obscure assembly code.
>
Yes, I can confirm that Benoît's concerns are right: I reconstructed the
followig theorem for list no. 34 ["2re","2pos","pm3.2i"] (no. 48 is nearly
the same) as I announced:
2posre $p |- ( 2 e. RR /\ 0 < 2 ) $=
( c2 cr wcel cc0 clt wbr 2re 2pos pm3.2i ) ABCDAEFGHI $.
But this is only the expanded form of ~2rp, and looking at proofs using `2
e. RR` and `0 < 2` (i.e., ~2re and ~2pos), such proofs can be shortened
more elegantly making use of `2 e. RR*`. For example, the proof of ~amgm2
can be shortened by using ~lemuldiv2d instead of ~lemuldiv2 (this must have
been done manually, minimize_with did not shorten anything). Since ~2pos is
not needed/used anymore, a new theorem ~2posre would not help to shorten
this proof further. Furthermore, using ~lemuldiv2d better fits to our
preferred "deduction style". Therefore, I will not add ~2posre to set.mm
(but will contribute the shortened proofs of ~amgm2 and a few others with
my next PR).
--
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/1b38399f-fbed-4672-89e8-1dbc180dd389n%40googlegroups.com.
