Merry Christmas everybody. So, I compared the proofs Thierry and I worked on. To me, it looks clear that using class variables is better for proof length and simplicity, therefore, in the best interest of the database, I think Thierry's versions are the ones to be added.
He did not remove some hypotheses and DV conditions as I did (like removing the closure hypothesis in the Eckmann-Hilton argument), but I see no reason why this wouldn't be possible with his proofs as well. Removing hypotheses should come at no cost, while removing DVs might lengthen some proofs. So far, only one person expressed an opinion on this matter (favouring fewer DVs), so it might be worth collecting other thoughts. There is also a difference in axiom usage. Thierry's versions of *~* *mendpadmlem8*, *~**mendpadmlem9*, *~**mendpadmlem10* use *ax-pr* and *ax-sep*, while mine avoid them. Additionally, Thierry's versions of *~* *mendpadmbilem4*, *~**mendpadmbilem5*, *~**mendpadmbi* use *ax-pre-sup*, while I avoided it altogether. As a result, my version of the goal statement of the challenge (*~mendpadmbi*) has fewer DV conditions (saving *$d x M y z $.*) and uses one fewer axiom (*~**ax-pre-sup*). > Advent of metamath has ended - both Gino and Thierry finished formalizing all problems, including the bonus ones. I started from the third theorem *~aabbaa*, so only Thierry formalized all problems. I'd like to hear from Thierry, also regarding credits, whether he would be ok with Savask's proposals or not (I was the first to formalize every theorem from *~aabbaa *onward, but his versions are better suited for the shared database). -- 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 visit https://groups.google.com/d/msgid/metamath/73427ff3-25ac-48ec-bad2-39b6cf80e41en%40googlegroups.com.
