> I wonder how it looks on the other proof assistants. It seems an interesting example related to the topic of de Bruijn factors and the difficulty of proving theorems formally vs. informally.
My understanding is that a noticeable part of the metamath proof is taken by work with quantifiers, variables etc, and this is usually handled (semi-) automatically in other proof assistants. > I hope that at least some of these theorems will eventually end up in the "main" area, instead of in a mathbox. I would be happy if they did, but I think it's best to apply our usual rule here - theorems generally stay in mathboxes until someone else requires it. > Twelfth theorem proved. Since Gino is moving at an alarming pace, I have updated the problem set with 6 bonus problems, which ask to prove that that the Mendelsohn-Padmanabhan identity *characterizes* abelian groups of exponent 2. Essentially it's mendpadm + an argument showing that this identity holds in boolean groups. I didn't put these statements initially since I wasn't entirely sure if anyone was going to participate at all (I'm glad that I was wrong), but beware that new problems might be a bit more technical even though they are trivial from the mathematical standpoint. -- 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/dbc9c545-6078-4199-8f45-573460ba8096n%40googlegroups.com.
