Advent of Metamath 2024

[savask]

Programmers have a nice tradition of solving a small puzzle or coding task on each day of advent, Advent of Code being one of the most famous examples. Last year I tried to propose a similar initiative for Metamath, namely Metamath Christmas challenge, where the task was to prove Ryley's theorem on sums of three cubes (which was successfully done by Igor, congrats to him!).

This year I suggest a new challenge, a set of 16 small problems about magmas:

https://gist.github.com/savask/f7a3b46663aa16e5dd48f8bfaba3e3e5

All of these tasks have elementary (and quite short) proofs, and one need not know any universal algebra in order to solve them, although some arguments might be tricky to find! The first task appeared on the Putnam exam, the fourth one is the famous Eckmann-Hilton argument, and the last one is a series of steps required to prove a result of Mendelsohn and Padmanabhan that one short identity characterizes boolean groups.

I hope fellow metamathers will find this set of problems interesting. Although I know the proofs of all the suggested tasks, I have not formalized them myself, so beware of possible problems in the statements (especially in the d-conditions). Of course, the first person to formalize some result can claim it for themselves and put it in their mathbox.

I also would like to thank Mario for looking through this problem set and giving several valuable suggestions on how to fix and improve some statements. Also I would like to thank Benoit, since his comment on the set.mm github repository about the Eckmann-Hilton argument gave me an idea to make this problem set.

[Thierry Arnoux]

On 01/12/2024 06:49, savask wrote:
> Programmers have a nice tradition of solving a small puzzle or coding

> task on each day of advent. This year I suggest a new challenge, a set

> of 16 small problems about magmas:
>
> https://gist.github.com/savask/f7a3b46663aa16e5dd48f8bfaba3e3e5

That's awesome, thanks for organizing this!

I'll post my progress here:

https://github.com/tirix/christmas24.mm

[savask]

> I'll post my progress here: ...

Nice that you liked it! I have a question: do you use some automation (tactics) to do substitutions into the identity, like deriving step 23 of your MPP file? Or you simply remember the movements by heart?

[Thierry Arnoux]

On 02/12/2024 13:29, savask wrote:
> I have a question: do you use some automation (tactics) to do
> substitutions into the identity, like deriving step 23 of your M<P

> file? Or you simply remember the movements by heart?

Recently I've been using Yamma. Unfortunately it does not have
auto-transformations like MMJ2, so there is no tactics for automatically
proving e.g. variable substitutions.

Most of the time I work backwards, from the formula I want to prove.
Yamma proposes a reduced list of theorems which could lead to that
result, and I choose from the list, partly from my memory.

Otherwise I'm either entering the formula and letting the tool find the
correct theorem to apply, or remembering the name of the theorem I want
to apply, and letting the tool build the resulting formula.

[Jorge Agra]

That auto-transformation we mention, is what? Do you mind explaining?

--
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 visit https://groups.google.com/d/msgid/metamath/c8811771-bd98-4d95-96b9-1839a1d73505%40gmx.net.

[Thierry Arnoux]

On 02/12/2024 17:52, Jorge Agra wrote:

That auto-transformation we mention, is what? Do you mind explaining?

For example MMJ2 is able to automatically expand this proof snippet from just the last step:

9::oveq1 |- ( b = Y -> ( b .o. ( X .o. Y ) ) = ( Y .o. ( X .o. Y ) ) )

10:9:oveq2d |- ( b = Y -> ( ( X .o. Y ) .o. ( b .o. ( X .o. Y ) ) ) = ( ( X .o. Y ) .o. ( Y .o. ( X .o. Y ) ) ) )

11::id |- ( b = Y -> b = Y )

!12:10,11:eqeq12d |- ( b = Y -> ( ( ( X .o. Y ) .o. ( b .o. ( X .o. Y ) ) ) = b <-> ( ( X .o. Y ) .o. ( Y .o. ( X .o. Y ) ) ) = Y ) )

All it needs is the exclamation mark before the label and once the Unify command is called (Ctrl-U), it will generate all 3 steps above.

Yamma does not have this and I manually fill in `eqeq12d` among a short list. Then it will automatically find `id` as it is a one-step proof. I have to choose `oveq1d` over a short list (the first theorem in the list is often the correct one), and finally it find `oveq1` automatically.

MMJ2's auto-transformation  is mentioned here: https://github.com/digama0/mmj2/blob/c8dd05548139c7003220caedde65a7abe44a00bf/CHGLOG.TXT#L47

[Igor Ieskov]

> That's awesome, thanks for organizing this!

I second that. Thank you Saveliy for continuing this initiative!

I also was able to prove abaeqb. Similarly to Thierry’s proof, my proof also introduced a disjoint condition for a and b, whereas the task has disjoints showing that a and b should be non-disjoint. I spent some time trying to find another proof which will not require this additional disjoint for a and b, but I could not find it. On the one hand, as I understand, requiring a and b to be disjoint, means that we cannot substitute the same set for a and b simultaneously. Please correct me if I am wrong. For example, with this new disjoint we will not be able to “apply” this theorem to the statement |- ( ph -> A. x e. B A. x e. B ( x .o. x ) e. B ). Also the original d-conditions look like it was made deliberately that a and b should not be disjoint. On the other hand, it was mentioned that “beware of possible problems in the statements (especially in the d-conditions)”. Saveliy, could you please comment on that (is it legal to add a disjoint for a and b and what was your intention)?

> do you use some automation (tactics) to do substitutions into the identity, like deriving step 23 of your MPP file? Or you simply remember the movements by heart?

> That auto-transformation we mention, is what? Do you mind explaining?

These are all good questions. I used mm-lamp, and it has some automation to prove such steps (no need to write any code, it is available out of the box). I want to record a video with some explanations on how I proved abaeqb. This is a good example for me to demonstrate automation capabilities of mm-lamp. Will it not break any rules of this initiative, if I show how to prove abaeqb?

[Mario Carneiro]

On Mon, Dec 2, 2024 at 8:35 PM Igor Ieskov <igori...@gmail.com> wrote:

I also was able to prove abaeqb. Similarly to Thierry’s proof, my proof also introduced a disjoint condition for a and b, whereas the task has disjoints showing that a and b should be non-disjoint. I spent some time trying to find another proof which will not require this additional disjoint for a and b, but I could not find it. On the one hand, as I understand, requiring a and b to be disjoint, means that we cannot substitute the same set for a and b simultaneously. Please correct me if I am wrong. For example, with this new disjoint we will not be able to “apply” this theorem to the statement |- ( ph -> A. x e. B A. x e. B ( x .o. x ) e. B ). Also the original d-conditions look like it was made deliberately that a and b should not be disjoint. On the other hand, it was mentioned that “beware of possible problems in the statements (especially in the d-conditions)”. Saveliy, could you please comment on that (is it legal to add a disjoint for a and b and what was your intention)?

This is a typo, the theorem requires a and b to be disjoint. (If they were not disjoint, then you could apply the theorem with the two variables being the same to prove a stronger version of the theorem where you only assume the function is closed on the diagonal, which is not sufficient to prove the conclusion.)

[Benoit]

> Also I would like to thank Benoit, since his comment on the set.mm github repository about the Eckmann-Hilton argument gave me an idea to make this problem set.

Thank you Savask !  I found back the comment: https://github.com/metamath/set.mm/pull/2985#issuecomment-1399550809  It was certainly easier to write "I would like this in set.mm" than to actually devise this problem set !

Benoit

[Glauco]

I'll post my progress here:

https://github.com/tirix/christmas24.mm

cool repo! :-)

If you ever have the chance to record a screencast of some proof development (audio isn’t necessary), I’d love to check it out. It would help me identify features I could add to Yamma. I’m currently working on some improvements, and seeing your workflow from a different perspective would be incredibly helpful.

 

[Gino Giotto]

I proved the third theorem.

${
  $( If multiplying two times from the left (and the right) is an identity
     mapping, then the operation is commutative. $)
  $d a b B $.  $d a b X $.  $d a b Y $.  $d a b .o. $.  $d a ph $.
  aabbaa.a $e |- ( ph -> A. a e. B A. b e. B ( a .o. b ) e. B ) $.
  aabbaa.b $e |- ( ph -> A. a e. B A. b e. B ( a .o. ( a .o. b ) ) = b ) $.
  aabbaa.c $e |- ( ph -> A. a e. B A. b e. B ( ( b .o. a ) .o. a ) = b ) $.
  aabbaa.d $e |- ( ph -> X e. B ) $.
  aabbaa.e $e |- ( ph -> Y e. B ) $.
  aabbaa $p |- ( ph -> ( X .o. Y ) = ( Y .o. X ) ) $=
    ( co wceq wral oveq2 id oveq1 rspc2vd mpd cv oveq12d eqeq1d eqcom bitrdi wa
    oveq1d eqeq12d eqidd wcel eleq1d oveq2d eqtrd ) ACDEMZUNCEMZCEMZDCEMAGUAZFU
    AZEMZUREMZUQNZGBOFBOZUNUPNZJAVCUQUQCEMZCEMZNZVAFGCUNBBBURCNZVAVEUQNVFVGUTVE
    UQVGUSVDURCEURCUQEPVGQUBUCVEUQUDUEUQUNNZUQUNVEUPVHQVHVDUOCEUQUNCERUGUHKAVGU
    FBUIZAURUQEMZBUJZGBOFBOUNBUJZHAVLCUQEMZBUJVKFGCDBBBVGVJVMBURCUQERUKUQDNZVMU
    NBUQDCEPUKKVILSTZSTAUODCEAUOUNUNDEMZEMZDACVPUNEAVBCVPNZJAVRUQUQDEMZDEMZNZVA
    FGDCBBBURDNZVAVTUQNWAWBUTVTUQWBUSVSURDEURDUQEPWBQUBUCVTUQUDUEUQCNZUQCVTVPWC
    QWCVSUNDEUQCDERUGUHLAWBUFBUIKSTULAURVJEMZUQNZGBOFBOVQDNZIAWFUNUNUQEMZEMZUQN
    WEFGUNDBBBURUNNZWDWHUQWIURUNVJWGEWIQURUNUQERUBUCVNWHVQUQDVNWGVPUNEUQDUNEPUL
    VNQUHVOAWIUFBUILSTUMUGUM $.
$}

[Glauco]

These are all good questions. I used mm-lamp, and it has some automation to prove such steps (no need to write any code, it is available out of the box). I want to record a video with some explanations on how I proved abaeqb. This is a good example for me to demonstrate automation capabilities of mm-lamp. Will it not break any rules of this initiative, if I show how to prove abaeqb?

I’d be really interested in seeing such a video

 

[savask]

> Saveliy, could you please comment on that (is it legal to add a disjoint for a and b and what was your intention)?

Yes, it is legal to add or remove disjoints if you need it for the proof. I don't have a very good intuition behind disjoint conditions, so it seems I missed some in the statements.

> I used mm-lamp, and it has some automation to prove such steps (no need to write any code, it is available out of the box). ... Will it not break any rules of this initiative, if I show how to prove abaeqb?

Sure, please share the video, it would be very interesting to take a look at mm-lamp automation.

[Gino Giotto]

I proved the fourth theorem. It seems one hypothesis is not needed.

This proof is way too long so probably I used a very inefficient approach.

${
  $( The Eckmann-Hilton argument. If for two unital magmas, represented here by the operation ` .o. ` with unit ` E `
     and the operation ` .(x) ` with unit ` I ` , on the same base set ` B ` an identity ` ( ( a .(x) b ) .o. ( c .(x) d ) ) = ( ( a .o. c ) .(x) ( b .o. d ) ) `
     holds, then these magmas coincide and the operation is associative and commutative. $)
  $d a b c d e v B $.  $d a b c d e v E $.  $d a b c d e v I $.
  $d a b c d e v .o. $.  $d a b c d e v .(x) $.  $d a b c d e v ph $.
  eckmannhilton.a $e |- ( ph -> A. a e. B A. b e. B ( a .o. b ) e. B ) $.
  eckmannhilton.c $e |- ( ph -> A. a e. B ( ( a .o. E ) = a /\ ( E .o. a ) = a ) ) $.
  eckmannhilton.d $e |- ( ph -> A. a e. B ( ( a .(x) I ) = a /\ ( I .(x) a ) = a ) ) $.
  eckmannhilton.e $e |- ( ph -> ( E e. B /\ I e. B ) ) $.
  eckmannhilton.f $e |- ( ph -> A. a e. B A. b e. B A. c e. B A. d e. B ( ( a .(x) b ) .o. ( c .(x) d ) ) = ( ( a .o. c ) .(x) ( b .o. d ) ) ) $.

  iden $p |- ( ph -> E = I ) $=
    ( co wceq wral oveq2 eqeq12d cv wa r19.26 simpld wb id bitrdi adantl rspcdv
    wcel eqcom adantld syl5bi mpd syl6ib adantrd oveq12d oveq1d 2ralbidv oveq2d
    oveq1 simprd eqidd rspc2vd syld 3eqtrd ) ADDDFPZEECPZEAGUAZDFPZVIQZDVIFPZVI
    QZUBGBRZDVGQZLVNVKGBRZVMGBRZUBZAVOVKVMGBUCZAVQVOVPAVMVOGDBADBUJZEBUJZNUDZVI
    DQZVMVOUEAWCVMVGDQVOWCVLVGVIDVIDDFSWCUFZTVGDUKUGUHUIULUMUNAVGEDCPZDECPZFPZE
    DFPZDEFPZCPZVHADWEDWFFAVIECPZVIQZEVICPZVIQZUBGBRZDWEQZMWOWLGBRZWNGBRZUBZAWP
    WLWNGBUCZAWRWPWQAWRWEDQZWPAWNXAGDBWBWCWNXAUEAWCWMWEVIDVIDECSWDTUHUIWEDUKUOU
    LUMUNAWODWFQZMWOWSAXBWTAWQXBWRAWQWFDQZXBAWLXCGDBWBWCWLXCUEAWCWKWFVIDVIDECVA
    WDTUHUIWFDUKUOUPUMUNUQAVIHUAZCPZIUAZJUAZCPZFPZVIXFFPZXDXGFPZCPZQZJBRIBRZHBR
    GBRZWGWJQZOAXOWEXHFPZEXFFPZDXGFPZCPZQZJBRIBRZXPAYBEXDCPZXHFPZXRXKCPZQZJBRIB
    RXNGHEDBBBVIEQZXMYFIJBBYGXIYDXLYEYGXEYCXHFVIEXDCVAURYGXJXRXKCVIEXFFVAURTUSX
    DDQZYFYAIJBBYHYDXQYEXTYHYCWEXHFXDDECSURYHXKXSXRCXDDXGFVAUTTUSAVTWANVBZAYGUB
    BVCWBVDAXPWEDXGCPZFPZWHXSCPZQYAIJDEBBBXFDQZXQYKXTYLYMXHYJWEFXFDXGCVAUTYMXRW
    HXSCXFDEFSURTXGEQZYKWGYLWJYNYJWFWEFXGEDCSUTYNXSWIWHCXGEDFSUTTWBAYMUBBVCYIVD
    VEUNAWHEWIECAVNWHEQZLVNVRAYOVSAVPYOVQAVKYOGEBYIYGVKYOUEAYGVJWHVIEVIEDFVAYGU
    FZTUHUIUPUMUNAVNWIEQZLVNVRAYQVSAVQYQVPAVMYQGEBYIYGVMYQUEAYGVLWIVIEVIEDFSYPT
    UHUIULUMUNUQVFAWOVHEQZMWOWSAYRWTAWRYRWQAWNYRGEBYIYGWNYRUEAYGWMVHVIEVIEECSYP
    TUHUIULUMUNVF $.

  mcoinc $p |- ( ph -> A. a e. B A. b e. B ( a .o. b ) = ( a .(x) b ) ) $=
    ( co wceq wral wa ralimi cv wi syl r19.26 iden oveq2d eqeq1d biimpd ralimdv
    simpl adantrd syl5bi mpd sylanbrc ralrimivw ralcom sylib oveq1d adantld weq
    simpr oveq2 id eqeq12d anbi12d biimpri sylbir syl2anc simpll simprl oveq12d
    cbvralvw simplr simprr ralim 3syl ralbii sylbb anim2i 2ralbidv simprd eqidd
    wcel rspc2vd imp biimpi sylc ) AGUAZECPZEHUAZCPZFPZWHEFPZEWJFPZCPZQZHBRZWHW
    JFPZWHWJCPZQZHBRZUBZGBRZWQGBRZXAGBRAWIWHQZWMWHQZSZWKWJQZWNWJQZSZSZHBRZGBRZW
    PWTUBZHBRZGBRXCAXGHBRZGBRZXJHBRZGBRZXMAXGGBRZHBRXQAXTHBAXEGBRZXFGBRZXTAXEEW
    HCPZWHQZSZGBRZYAMYEXEGBXEYDUJTUCAWHDFPZWHQZDWHFPZWHQZSZGBRZYBLYLYHGBRZYJGBR
    ZSAYBYHYJGBUDAYMYBYNAYHXFGBAYHXFAYGWMWHADEWHFABCDEFGHIJKLMNOUEZUFUGUHUIUKUL
    UMXEXFGBUDUNUOXGHGBBUPUQAXRGBAYDEWHFPZWHQZSZGBRZXRAYDGBRZYQGBRZYSAYFYTMYEYD
    GBXEYDVATUCAYLUUALAYKYQGBAYJYQYHAYJYQAYIYPWHADEWHFYOURUGUHUSUIUMYDYQGBUDUNY
    RXJGHBGHUTZYDXHYQXIUUBYCWKWHWJWHWJECVBUUBVCZVDUUBYPWNWHWJWHWJEFVBUUCVDVEVLU
    QUOXQXSSXPXRSZGBRXMXPXRGBUDUUDXLGBXLUUDXGXJHBUDVFTVGVHXLXOGBXKXNHBXKWPWTXKW
    LWRWOWSXKWIWHWKWJFXEXFXJVIXGXHXIVJVKXKWMWHWNWJCXEXFXJVMXGXHXIVNVKVDUHTTXOXB
    GBWPWTHBVOTVPAWIEJUAZCPZFPZWMEUUEFPZCPZQZJBRZGBRZXDAAWSIUAZUUECPZFPZWHUUMFP
    ZWJUUEFPZCPZQZJBRZGBRZIBRZHBRZSZUULAAUUTIBRZHBRGBRZUVDAVCOUVFUVCAUVFUVEGBRZ
    HBRUVCUVEGHBBUPUVGUVBHBUUTGIBBUPVQVRVSVHAUVCUULAUULWIUUNFPZUUPUUHCPZQZJBRGB
    RUVAHIEEBBBWJEQZUUSUVJGJBBUVKUUOUVHUURUVIUVKWSWIUUNFWJEWHCVBURUVKUUQUUHUUPC
    UVKWJEUUEFUVKVCURUFVDVTUUMEQZUVJUUJGJBBUVLUVHUUGUVIUUIUVLUUNUUFWIFUVLUUMEUU
    ECUVLVCURUFUVLUUPWMUUHCUUMEWHFVBURVDVTADBWCEBWCNWAZAUVKSBWBUVMWDWEUCUUKWQGB
    UUKWQUUJWPJHBJHUTZUUGWLUUIWOUVNUUFWKWIFUUEWJECVBUFUVNUUHWNWMCUUEWJEFVBUFVDV
    LWFTUCWQXAGBVOWG $.

  eckmannhilton $p |- ( ph -> ( E = I /\ A. a e. B A. b e. B ( ( a .o. b ) = ( a .(x) b ) /\ ( a .o. b ) = ( b .o. a ) ) /\
                        A. a e. B A. b e. B A. c e. B ( ( a .o. b ) .o. c ) = ( a .o. ( b .o. c ) ) ) ) $=
( wceq co wral syl wi vv ve cv wa iden mcoinc id ralcom ralbii bitri biimpi
    oveq1 oveq1d eqeq12d ralbidv oveq2 oveq2d wcel simpr eqidd rspc2vd cbvralvw
    mpd weq jca ralimi a1i com12 ralrimiv r19.26 imp bicomi eqeq1d impd ralimdv
    biimpd com13 oveq12 wb eqcom eqeq2 ralim simpll simplr oveq12d rspcdv bitrd
    imim1i idd simpllr eleq12d cbvral2vw rsp imim2i simp2 3exp syld com45 com34
    ex com23 eqeq2d mpdd 3jca ) ADEPZGUCZHUCZFQZXFXGCQZPZXHXGXFFQZPZUDHBRZGBRZX
    HIUCZFQZXFXGXOFQZFQZPZIBRZHBRZGBRZABCDEFGHIJKLMNOUEZAXJHBRZXLHBRZUDZGBRZXNA
    YDGBRZYEGBRZUDZYGAYHYIABCDEFGHIJKLMNOUFZAAEXFCQZXGECQZFQZEXGFQZXFEFQZCQZPZH
    BRZGBRZUDYIAAYTAUGAEXGCQZXOECQZFQZEXOFQZXGEFQZCQZPZIBRZHBRZYTAXIXOJUCZCQZFQ
    ZXFXOFQZXGUUJFQZCQZPZIBRZHBRZJBRZGBRZUUIAUUPJBRZIBRZHBRZGBRZUUTOUVDUUTUVCUU
    SGBUVCUUQJBRZHBRUUSUVBUVEHBUUPIJBBUHUIUUQHJBBUHUJUIUKSAUUIUUAUUKFQZUUDUUNCQ
    ZPZIBRZHBRUURGJEEBBBXFEPZUUQUVIHBUVJUUPUVHIBUVJUULUVFUUOUVGUVJXIUUAUUKFXFEX
    GCULUMUVJUUMUUDUUNCXFEXOFULUMUNUOUOUUJEPZUVIUUHHBUVKUVHUUGIBUVKUVFUUCUVGUUF
    UVKUUKUUBUUAFUUJEXOCUPUQUVKUUNUUEUUDCUUJEXGFUPUQUNUOUOADBURZEBURZUDUVMNUVLU
    VMUSSZAUVJUDBUTUVNVAVCUUIYTUUIYLUUBFQZUUDYPCQZPZIBRZGBRYTUUHUVRHGBHGVDZUUGU
    VQIBUVSUUCUVOUUFUVPUVSUUAYLUUBFUVSXGXFECUVSUGZUQUMUVSUUEYPUUDCUVSXGXFEFUVTU
    MUQUNUOVBUVRYSGBUVQYRIHBIHVDZUVOYNUVPYQUWAUUBYMYLFUWAXOXGECUWAUGZUMUQUWAUUD
    YOYPCUWAXOXGEFUWBUQUMUNVBUIUJUKSVEAYTYIAYSYETZGBRZYTYITAYRXLTZHBRZGBRZUWDAY
    LXFPZYMXGPZUDZYQXKPZUDZHBRZGBRZUWGAUWJHBRZGBRZUWKHBRZGBRZUDZUWNAUWPUWRAUWHH
    BRZGBRZUWIHBRZGBRZUDZUWPAUXAUXCAUWHGBRZHBRZUXAAUXEHBXGBURZAUXEAUXETUXGAXFEC
    QZXFPZUWHUDZGBRZUXEMUXJUWHGBUXIUWHUSVFSVGVHVIUXFUXAUWHHGBBUHUKSAUXBGBXFBURZ
    AUXBAUXBTUXLAUXKUXBMUXKUXIGBRZUXEUDZUXBUXKUXNUXIUWHGBVJUKUXMUXEUXBUXEUXMUXB
    UXMUXBTUXEUXMUXBUXIUWIGHBGHVDZUXHYMXFXGUXOXFXGECUXOUGZUMUXPUNVBUKVGVHVKSSVG
    VHVIVEUXDUWPUXDUWTUXBUDZGBRZUWPUXRUXDUWTUXBGBVJVLUXQUWOGBUWOUXQUWHUWIHBVJVL
    UIUJUKSAYQXGXFCQZPZHBRZGBRZUWRAYOXGPZYPXFPZUDZHBRZGBRZUYBAUYCHBRZGBRZUYDHBR
    ZGBRZUDZUYGAUYIUYKAUYHGBUXLAUYHAUYHTUXLAEXFFQZXFPZGBRZUYHAXFDFQZXFPZDXFFQZX
    FPZUDZGBRZUYOLAUYTUYNGBAUYQUYSUYNUYQAUYSUYNTZAVUBTUYQAUYSUYNAUYRUYMXFADEXFF
    YCUMVMVPVGVHVNVOVCUYOUYHTAUYOUYHUYNUYCGHBUXOUYMYOXFXGXFXGEFUPUXPUNVBUKVGVCV
    GVHVIAUYDGBRZHBRZUYKAVUCHBUXGAVUCAVUCTZUXGAXEVUCYCXEAVUCVUEXEAVUAVUCLAUYTUY
    DGBAUYQUYSUYDUYSUYQAUYDUYQAUYDTTUYSAUYQUYDAUYQUYDAUYPYPXFADEXFFYCUQZVMVPVHV
    GVQVNVOVCVGVHVCVGVHVIVUDUYKUYDHGBBUHUKSVEUYLUYGUYGUYLUYGUYHUYJUDZGBRUYLUYFV
    UGGBUYCUYDHBVJUIUYHUYJGBVJUJVLUKSUYFUYAGBUYEUXTHBYOXGYPXFCVRVFVFSAUYAUWQTZG
    BRZUYBUWRTAUXTUWKTZHBRZGBRZVUIAYHVULYKYHUAUCZUBUCZFQZVUMVUNCQZPZUBBRZUABRZV
    ULYHVUSYHXFVUNFQZXFVUNCQZPZUBBRZGBRVUSYDVVCGBXJVVBHUBBHUBVDXHVUTXIVVAXGVUNX
    FFUPXGVUNXFCUPUNVBUIVVCVURGUABGUAVDZVVBVUQUBBVVDVUTVUOVVAVUPXFVUMVUNFULXFVU
    MVUNCULUNUOVBUJUKVUSXGVUNFQZXGVUNCQZPZUBBRZHBRZVULVUSVVIVURVVHUAHBUAHVDZVUQ
    VVGUBBVVJVUOVVEVUPVVFVUMXGVUNFULVUMXGVUNCULUNUOVBUKVVIXKUXSPZGBRZHBRZVULVVI
    VVMVVHVVLHBVVGVVKUBGBUBGVDZVVEXKVVFUXSVUNXFXGFUPVUNXFXGCUPUNVBUIUKVVMVVKHBR
    ZGBRZVULVVMVVPVVKHGBBUHUKVVOVUKGBVVKVUJHBVVKUXTUWKVVKUXSXKPZUXTUWKVSVVKVVQX
    KUXSVTUKUXSXKYQWASVPVFVFSSSSSVUKVUHGBUXTUWKHBWBVFSUYAUWQGBWBSVCVEUWSUWNUWNU
    WSUWNUWOUWQUDZGBRUWSUWMVVRGBUWJUWKHBVJUIUWOUWQGBVJUJVLUKSUWMUWFGBUWLUWEHBUW
    LYRXLUWLYNXHYQXKUWLYLXFYMXGFUWHUWIUWKWCUWHUWIUWKWDWEUWJUWKUSUNVPVFVFSUWFUWC
    GBYRXLHBWBVFSYSYEGBWBSVKSVEYJYGYGYJYDYEGBVJVLUKSYFXMGBYFXMXMYFXJXLHBVJVLUKV
    FSAUVDYBOAUVDXHUUJFQZXFUUNFQZPZJBRZHBRZGBRZYBAUVDXIEUUJCQZFQZYPUUNCQZPZJBRZ
    HBRZGBRZVWDAUVAHBRZGBRZIBRZVWKTUVDVWKTAVWMVWKIEBUVNAXOEPZVWMVWKVSZVWOVWPTAV
    WOVWLVWJGBVWOUVAVWIHBVWOUUPVWHJBVWOUULVWFUUOVWGVWOUUKVWEXIFVWOXOEUUJCVWOUGZ
    UMUQVWOUUMYPUUNCVWOXOEXFFVWQUQUMUNUOUOUOVGVKWFUVDVWNVWKUVDVWNUVDVWLIBRZGBRV
    WNUVCVWRGBUVAHIBBUHUIVWLGIBBUHUJUKWHSUVDAVWKVWDTZAVWSTUVDAVWJVWCTZGBRZVWSAV
    WIVWBTZHBRZGBRZVXAAVWHVWATZJBRZHBRZGBRZVXDAXIXHPZVWEUUJPZUDZVWGVVTPZUDZJBRZ
    HBRZGBRZVXHAVXKJBRZHBRZGBRZVXLJBRZHBRZGBRZUDZVXPAVXSVYBAVXIJBRZHBRZGBRZVXJJ
    BRZHBRZGBRZUDZVXSAVYFVYIAVXIHBRZGBRZJBRZVYFAVYLJBUUJBURZAVYLAVYLTVYNAYHVYLY
    KYDVYKGBXJVXIHBXJVXIXHXIVTUKVFVFSVGVHVIVYMVYFVYMVYKJBRZGBRVYFVYKJGBBUHVYOVY
    EGBVXIJHBBUHUIUJUKSAVYHGBUXLAVYHAVYHTUXLAVYGHBUXGAVYGAVYGTUXGAUXEVYGAUXKUXE
    MAUXJUWHGBUXJAUWHUXIUWHAUWHTZUWHVYPTUXIAUWHUWHAUWHWIVHVGVKVHVOVCUXEVYGUWHVX
    JGJBGJVDZYLVWEXFUUJXFUUJECUPVYQUGUNVBUKSVGVHVIVGVHVIVEVYJVXSVYJVYEVYHUDZGBR
    ZVXSVYSVYJVYEVYHGBVJVLVYSVYDVYGUDZHBRZGBRVXSVYRWUAGBWUAVYRVYDVYGHBVJVLUIWUA
    VXRGBVYTVXQHBVXQVYTVXIVXJJBVJVLUIUIUJUJUKSAXFUUNCQZVVTPZJBRZHBRZGBRZVYBAWUE
    GBAUXLWUEAUXLUDZWUDHBWUGUXGWUDWUGUXGUDZWUCJBWUGUXGVYNWUCTZAUXLUXGWUITZAYHUX
    LWUJTYKAUXLYHWUJAUXLUXGYHWUIAUXLUXGVYNYHWUCAUXLUXGVYNYHWUCTZTZTWUGUXGWULWUH
    VYNWUKWUHVYNUDZVUNVUMFQZVUNVUMCQZPZUABRUBBRZWUCTWUKWUMWUCXFVUMCQZXFVUMFQZPZ
    WUPUBUAXFUUNBBBVVNWUPWUOWUNPZWUTWUPWVAVSVVNWUNWUOVTVGVVNWUOWURWUNWUSVUNXFVU
    MCULVUNXFVUMFULUNWGVUMUUNPZWURWUBWUSVVTWVBVUMUUNXFCWVBUGZUQWVBVUMUUNXFFWVCU
    QUNAUXLUXGVYNWJWUMVVNUDBUTWUHVYNUUNBURZWUGUXGVYNWVDTZAUXLUXGWVETZAWVDJBRZHB
    RZUXLWVFTZAXHBURZHBRGBRZWVHKWVKWVHWVKVUMUUJFQZBURZJBRZUABRWVHWVJWVMVUMXGFQZ
    BURGHUAJBBVVDXHWVOBBXFVUMXGFULVVDBUTWKHJVDZWVOWVLBBXGUUJVUMFUPWVPBUTWKWLWVN
    WVGUAHBVVJWVMWVDJBVVJWVLUUNBBVUMXGUUJFULVVJBUTWKUOVBUJUKSAWVHWVFWVIWVHWVFTA
    WVHUXGWVGTWVFWVGHBWMWVGWVEUXGWVDJBWMWNSVGAWVFUXLWVFAWVFUXLWOWPWQVCVKVKVKVAY
    HWUQWUCYHWUQXJWUPVUNXGFQZVUNXGCQZPGHUBUABBGUBVDXHWVQXIWVRXFVUNXGFULXFVUNXGC
    ULUNHUAVDWVQWUNWVRWUOXGVUMVUNFUPXGVUMVUNCUPUNWLUKWHSWTWTWTWRWSXAVCVKVKVIWTV
    IWTVIAWUEVYATZGBRZWUFVYBTAXFYPPZGBRZWVTAVUAWWBLAUYQGBRZUYSGBRZUDZWWBTVUAWWB
    TAWWCWWDWWBWWDWWCAWWBWWCAWWBTTWWDAWWCWWBAUYQWWAGBAXFUYPPZWWATUYQWWATAWWFWWA
    AUYPYPXFVUFXBVPUYQWWFWWAUYQWWFUYPXFVTUKWHSVOVHVGVQVNVUAWWEWWBVUAWWEUYQUYSGB
    VJUKWHSVCWWAWVSGBWWAWUDVXTHBWWAWUCVXLJBWWAWUCVXLWWAWUBVWGVVTWWAXFYPUUNCWWAU
    GUMVMVPVOVOVFSWUEVYAGBWBSVCVEVYCVXPVYCVXRVYAUDZGBRZVXPWWHVYCVXRVYAGBVJVLWWH
    VXQVXTUDZHBRZGBRVXPWWGWWJGBWWJWWGVXQVXTHBVJVLUIWWJVXOGBWWIVXNHBVXNWWIVXKVXL
    JBVJVLUIUIUJUJUKSVXOVXGGBVXNVXFHBVXMVXEJBVXMVWHVWAVXMVWFVVSVWGVVTVXMXIXHVWE
    UUJFVXIVXJVXLWCVXIVXJVXLWDWEVXKVXLUSUNVPVFVFVFSVXGVXCGBVXFVXBHBVWHVWAJBWBVF
    VFSVXCVWTGBVWIVWBHBWBVFSVWJVWCGBWBSVGVHXCUVDVWDYBTZTAWWKUVDVWDYBVWCYAGBVWBX
    THBVWAXSJIBJIVDZVVSXPVVTXRWWLUUJXOXHFWWLUGZUQWWLUUNXQXFFWWLUUJXOXGFWWMUQUQU
    NVBUIUIUKVGVGXCVCXD $.
$}

[savask]

> I proved the fourth theorem. It seems one hypothesis is not needed.

That's impressive, it didn't cross my mind that one need not assume the second operation to be closed.

> This proof is way too long so probably I used a very inefficient approach.

I'm also surprised at the length, given that the proof I know (from wikipedia...) is quite short. In hindsight, I probably should have split the task into smaller subtasks anyway, maybe I will do so in a revised version of the problem set.

[Igor Ieskov]

> This is a typo, the theorem requires a and b to be disjoint. …

Got it. Thank you Mario.

Here is my video https://drive.google.com/file/d/1B_hiEfuP8KE3L_6uTnfdD7wkiLP15IIp/view?usp=sharing

A couple of comments to the video.

The volume may spike suddenly, so don't listen at high volume.

At 13:15, I didn't manage to clearly explain the difference between how matching and unification work in mm-lamp. Matching can replace all kinds of variables but it can do that in the top expression only. Unification can replace variables in both expressions but it can replace meta-variables only.

[Glauco]

Here is my video https://drive.google.com/file/d/1B_hiEfuP8KE3L_6uTnfdD7wkiLP15IIp/view?usp=sharing

Thank you, Igor, it is a really interesting video.

Glauco 

[Gino Giotto]

I proved the fift theorem. Again, apparently one hypothesis is not needed, the set B is not required to be not empty.

${
  $( Lemma for mendpadm. Multiplication is surjective. $)
  $d x y B $.  $d x y .o. $.  $d x y z ph $.
  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.
  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.
  mendpadmlem1 $p |- ( ph -> A. z e. B E. x e. B E. y e. B  ( x .o. y ) = z ) $=
    ( cv co wceq wrex wcel wa wral wi mpd adantr simpr weq simplr rsp wn pm2.21
    com24 oveq12 simpl oveq2d oveq12d eqeq1d biimpd ex a1i com14 imp41 rspcimdv
    syl5 cmgm pm3.22 anidms mgmcl 3expb syl2an 3expia biimprd adantll rspcimedv
    ja sylan ralrimiva ) ABLZCLZGMZDLZNZCEOZBEOZDEAVQEPZQZVQVQGMZVQWCGMZGMZVQNZ
    VTWBVPVNVQVOGMZGMZGMZVQNZDERZCERZBERZWFAWMWAKUAWBWLWFBVQEAWAUBWBBDUCZQZWKWF
    CVQEAWAWNUDWKWAWJSZWOCDUCZQWFWJDEUEAWAWNWQWPWFSZWAWNWQWRSSSAWPWNWQWAWFWAWJW
    NWQWAWFSSSWAUFWAWQWNWFWAWQWNWFSSUGUHWAWNWQWJWFWNWQWJWFSZSSWAWNWQWSWNWQQZWJW
    FWTWIWEVQWTVPWCWHWDGVNVQVOVQGUIWTVNVQWGWCGWNWQUJWTVOVQVQGWNWQUBUKULULUMUNUO
    UPUQVKUQUPURUTUSUSTWBVSWFBWCEAFVAPZWAWAQZWCEPZWAJWAXBWAWAVBVCXAWAWAXCEFVQVQ
    GHIVDVEVFZWBVNWCNZQVRWFCWDEWBWDEPZXEWBXCXFXDAXAWAXCXFSJXAWAXCXFEFVQWCGHIVDV
    GVLTUAXEVOWDNZWFVRSWBXEXGQZVRWFXHVPWEVQVNWCVOWDGUIUMVHVIVJVJTVM $.
$}

[savask]

> Here is my video ...

It was very interesting, thanks. For me the highlight of the video was the "proving bottom-up" dialog, which can search for proofs of large depth automatically. Metamath.exe also has one (the "improve" command), and mmj2 doesn't, as far as I'm aware, so in a sense metamath-lamp has partly surpassed mmj2 in functionality.

There was an interesting part near the end where the proof search couldn't figure out that A e. CC is implied by A e. RR, since the latter statement has the same length and hence isn't picked up by the "Less" search heuristic. I think mmj2's transformation script can circumvent such issues in special cases, so there's potential for improving the search maybe by adding special tactics for set.mm which narrow down the search with specific theorems banned/allowed.

> I proved the fifth theorem. Again, apparently one hypothesis is not needed, the set B is not required to be not empty.

Nice! You shouldn't require nonemptyness until lemma 7, which postulates the existence of unity. I think it's a bit unfortunate that we allow empty magmas, since algebraic structures are usually assumed to be based on nonempty sets; this makes the theory more uniform.

[Igor Ieskov]

> Thank you, Igor, it is a really interesting video.

Thanks, Glauco! Yamma’s feature of proposing a list of theorems is also very useful. I want to add such a feature to mm-lamp in the future.

> there's potential for improving the search maybe by adding special tactics for set.mm which narrow down the search with specific theorems banned/allowed.

Thanks for the feedback! Current implementation of the bottom-up prover allows to provide a list of theorems to use. Also it is possible to narrow down usage of some theorems to some specific scenarios. For example, to allow usage of syl only when the first hypothesis is of the form of |- ( ph -> X e. A ) and the conclusion is |- ( ph -> Y = ( X ^ N ) ). With appropriately collected list of theorems to use and such rules for narrowing down usage of some theorems, the bottom-up prover becomes very fast, so I don’t even need to specify statement length restriction. But all of these are available in macros only. I also have a few more ideas to try, for example, making bottom-up prover parameters dynamic, so they depend on what is needed to prove. Currently I am working on a few other improvements which will affect macros API. After that I will start documenting the macros feature.

[Gino Giotto]

Sixth theorem proved:

${
  $( Lemma for mendpadm. Multiplication is surjective. $)

  $d x y z a b c B $.  $d x y z a b c .o. $.  $d x z ph $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.
  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( Lemma for mendpadm. Multiplication by ` x ` from the left is surjective. $)
  mendpadmlem2 $p |- ( ph -> A. z e. B A. x e. B E. y e. B  ( x .o. y ) = z ) $=
    ( va vc co wceq wi wral oveq1 eqeq1d oveq2d vb cv wcel wrex wal wa cmgm w3a
    simp1 mgmcl 3com23 simp3 syl3anc syld3an3 3exp syl imp31 ad2antrr weq oveq2
    oveq12d eqeq12d cbvral3vw sylib com23 simplr rspc3v mpd simpr oveq1d rspcev
    id mpbid syl2anc ex alrimiv df-ral imbi2i albii sylbbr ) ADUBZEUCZBUBZEUCZW
    CCUBZGNZWAOZCEUDZPZBUEZPZDUEZWHBEQZDEQZAWKDAWBWJAWBUFZWIBWOWDWHWOWDUFZWCWAG
    NZWAWCWQGNZGNZGNZEUCZWCWTGNZWAOZWHAWBWDXAAFUGUCZWBWDXAPPJXDWBWDXAXDWBWDUHZX
    DWQEUCZWSEUCZXAXDWBWDUIZXDWDWBXFEFWCWAGHIUJZUKZXDWBWDWREUCZXGXEXDWDXFXKXHXD
    WBWDULXJEFWCWQGHIUJUMZEFWAWRGHIUJUNEFWQWSGHIUJUMUOUPUQWPWQWRGNZWTGNZWAOZXCW
    PLUBZUAUBZGNZXPMUBZXQGNZGNZGNZXSOZMEQUAEQLEQZXOWPWFWCWAWEGNZGNZGNZWAOZDEQCE
    QBEQZYDAYIWBWDKURYHYCXPWEGNZXPYEGNZGNZWAOXRXPWAXQGNZGNZGNZWAOBCDLUAMEEEBLUS
    ZYGYLWAYPWFYJYFYKGWCXPWEGRWCXPYEGRVASCUAUSZYLYOWAYQYJXRYKYNGWEXQXPGUTYQYEYM
    XPGWEXQWAGUTTVASDMUSZYOYBWAXSYRYNYAXRGYRYMXTXPGWAXSXQGRTTYRVLVBVCVDZWPXFXKW
    BYDXOPAWBWDXFAXDWBWDXFPPJXDWDWBXFXDWDWBXFXIUOVEUPUQAWBWDXKAXDWBWDXKPPJXDWBW
    DXKXLUOUPUQAWBWDVFZYCXOWQXQGNZWQXTGNZGNZXSOXMWQXSWRGNZGNZGNZXSOLUAMWQWRWAEE
    EXPWQOZYBUUCXSUUGXRUUAYAUUBGXPWQXQGRXPWQXTGRVASXQWROZUUCUUFXSUUHUUAXMUUBUUE
    GXQWRWQGUTUUHXTUUDWQGXQWRXSGUTTVASMDUSZUUFXNXSWAUUIUUEWTXMGUUIUUDWSWQGXSWAW
    RGRTTUUIVLVBVGUMVHWPXNXBWAWPXMWCWTGWPYDXMWCOZYSWPWDWBWDYDUUJPWOWDVIZYTUUKYC
    UUJWCXQGNZWCXTGNZGNZXSOWQWCXSWAGNZGNZGNZXSOLUAMWCWAWCEEELBUSZYBUUNXSUURXRUU
    LYAUUMGXPWCXQGRXPWCXTGRVASUADUSZUUNUUQXSUUSUULWQUUMUUPGXQWAWCGUTUUSXTUUOWCG
    XQWAXSGUTTVASMBUSZUUQXMXSWCUUTUUPWRWQGUUTUUOWQWCGXSWCWAGRTTUUTVLVBVGUMVHVJS
    VMWGXCCWTEWEWTOWFXBWAWEWTWCGUTSVKVNVOVPVOVPWNWBWMPZDUEWLWMDEVQUVAWKDWMWJWBW
    HBEVQVRVSVTUP $.
$}

As a side note, Tirix is now close to completing the proof of the Eckmann-Hilton argument, and although his version is better organized than mine, it still looks pretty long. I guess now we can say that the short proof on Wikipedia doesn't convey a good idea about the amount of work needed to accomplish that task.

[Gino Giotto]

Seventh theorem proved:

${
  $d x y z a b c B $.  $d x y z a b c .o. $.  $d y z ph $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.
  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( Lemma for mendpadm. Multiplication by ` y ` from the right is surjective. $)
  mendpadmlem3 $p |- ( ph -> A. z e. B A. y e. B E. x e. B ( x .o. y ) = z ) $=
    ( va vb vc co wceq wral oveq1 eqeq1d oveq2d cv wcel wrex wi wal weq oveq12d
    wa oveq2 id eqeq12d cbvral3vw sylib ad2antrr cmgm simplr mgmcl simpr rspc3v
    syl3anc mpd biimpd rspcev syl6an ex alrimiv df-ral imbi2i albii sylbbr syl
    ) ADUAZEUBZCUAZEUBZBUAZVNGOZVLPZBEUCZUDZCUEZUDZDUEZVSCEQZDEQZAWBDAVMWAAVMUH
    ZVTCWFVOVSWFVOUHZVLVLGOZVNVLGOZGOZWHVLWIGOZGOZGOZVLPZVSWGLUAZMUAZGOZWONUAZW
    PGOZGOZGOZWRPZNEQMEQLEQZWNAXCVMVOAVQVPVLVNGOZGOZGOZVLPZDEQCEQBEQXCKXGXBWOVN
    GOZWOXDGOZGOZVLPWQWOVLWPGOZGOZGOZVLPBCDLMNEEEBLUFZXFXJVLXNVQXHXEXIGVPWOVNGR
    VPWOXDGRUGSCMUFZXJXMVLXOXHWQXIXLGVNWPWOGUIXOXDXKWOGVNWPVLGUITUGSDNUFZXMXAVL
    WRXPXLWTWQGXPXKWSWOGVLWRWPGRTTXPUJUKULUMUNZWGWHEUBZWIEUBZVMXCWNUDWGFUOUBZVM
    VMXRAXTVMVOJUNZAVMVOUPZYBEFVLVLGHIUQUTZWGXTVOVMXSYAWFVOURZYBEFVNVLGHIUQUTZY
    BXBWNWHWPGOZWHWSGOZGOZWRPWJWHWRWIGOZGOZGOZWRPLMNWHWIVLEEEWOWHPZXAYHWRYLWQYF
    WTYGGWOWHWPGRWOWHWSGRUGSWPWIPZYHYKWRYMYFWJYGYJGWPWIWHGUIYMWSYIWHGWPWIWRGUIT
    UGSNDUFZYKWMWRVLYNYJWLWJGYNYIWKWHGWRVLWIGRTTYNUJUKUSUTVAWGWJEUBZWNWJVNGOZVL
    PZVSWGXTXRXSYOYAYCYEEFWHWIGHIUQUTWGWNYQWGWMYPVLWGWLVNWJGWGXCWLVNPZXQWGVMVMV
    OXCYRUDYBYBYDXBYRXKVLWSGOZGOZWRPWHVLWRVLGOZGOZGOZWRPLMNVLVLVNEEELDUFZXAYTWR
    UUDWQXKWTYSGWOVLWPGRWOVLWSGRUGSMDUFZYTUUCWRUUEXKWHYSUUBGWPVLVLGUIUUEWSUUAVL
    GWPVLWRGUITUGSNCUFZUUCWLWRVNUUFUUBWKWHGUUFUUAWIVLGWRVNVLGRTTUUFUJUKUSUTVATS
    VBVRYQBWJEVPWJPVQYPVLVPWJVNGRSVCVDVAVEVFVEVFWEVMWDUDZDUEWCWDDEVGUUGWBDWDWAV
    MVSCEVGVHVIVJVK $.
$}

[Gino Giotto]

I proved the eighth theorem without DV conditions on ph. The price to pay is the addition of more dummy variables and making the proof a bit longer:

${
  $d x y z a b c u v B $.  $d x y z a b c u v .o. $.  $d u v ph $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.
  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( Lemma for mendpadm.  The identity ` x .o. ( y .o. x ) = y ` holds. $)
  mendpadmlem4 $p |- ( ph -> A. x e. B A. y e. B ( x .o. ( y .o. x ) ) = y ) $=
    ( vu vc co wceq wral wcel oveq1 oveq12d oveq2d vv va vb cv wi wal wa eqeq1d
    weq oveq2 eqeq12d cbvral3vw sylib ad2antrr cmgm simplr mgmcl syl3anc rspc3v
    id simpr mpd 3eqtr3d ex alrimiv df-ral imbi2i albii sylbbr syl cbvral2vw )
    ALUDZUAUDZVLGNZGNZVMOZUAEPZLEPZBUDZCUDZVSGNZGNZVTOZCEPBEPAVLEQZVMEQZVPUEZUA
    UFZUEZLUFZVRAWHLAWDWGAWDUGZWFUAWJWEVPWJWEUGZVLVLGNZVOGNZWLVLVOGNZGNZGNZWMWP
    GNZGNZWMVOVMWKUBUDZUCUDZGNZWSMUDZWTGNZGNZGNZXBOZMEPUCEPUBEPZWRWMOZAXGWDWEAV
    SVTGNZVSDUDZVTGNZGNZGNZXJOZDEPCEPBEPZXGKXNXFWSVTGNZWSXKGNZGNZXJOXAWSXJWTGNZ
    GNZGNZXJOBCDUBUCMEEEBUBUIZXMXRXJYBXIXPXLXQGVSWSVTGRVSWSXKGRSUHCUCUIZXRYAXJY
    CXPXAXQXTGVTWTWSGUJYCXKXSWSGVTWTXJGUJTSUHDMUIZYAXEXJXBYDXTXDXAGYDXSXCWSGXJX
    BWTGRTTYDUTUKULZUMUNZWKWMEQZWOEQZYGXGXHUEWKFUOQZWLEQZVOEQZYGAYIWDWEJUNZWKYI
    WDWDYJYLAWDWEUPZYMEFVLVLGHIUQURZWKYIWDVNEQZYKYLYMWKYIWEWDYOYLWJWEVAZYMEFVMV
    LGHIUQUREFVLVNGHIUQURZEFWLVOGHIUQURZWKYIYJWNEQZYHYLYNWKYIWDYKYSYLYMYQEFVLVO
    GHIUQUREFWLWNGHIUQURYRXFXHWMWTGNZWMXCGNZGNZXBOWPWMXBWOGNZGNZGNZXBOUBUCMWMWO
    WMEEEWSWMOZXEUUBXBUUFXAYTXDUUAGWSWMWTGRWSWMXCGRSUHWTWOOZUUBUUEXBUUGYTWPUUAU
    UDGWTWOWMGUJUUGXCUUCWMGWTWOXBGUJTSUHXBWMOZUUEWRXBWMUUHUUDWQWPGUUHUUCWPWMGXB
    WMWOGRTTUUHUTUKUSURVBWKWPVLWQVNGWKXGWPVLOZYFWKYJYKWDXGUUIUEYNYQYMXFUUIWLWTG
    NZWLXCGNZGNZXBOWMWLXBVOGNZGNZGNZXBOUBUCMWLVOVLEEEWSWLOZXEUULXBUUPXAUUJXDUUK
    GWSWLWTGRWSWLXCGRSUHWTVOOZUULUUOXBUUQUUJWMUUKUUNGWTVOWLGUJUUQXCUUMWLGWTVOXB
    GUJTSUHMLUIZUUOWPXBVLUURUUNWOWMGUURUUMWNWLGXBVLVOGRTTUURUTUKUSURZVBWKWMVMWP
    VLGWKXGWMVMOZYFWKWDWDWEXGUUTUEYMYMYPXFUUTVLWTGNZVLXCGNZGNZXBOWLVLXBVLGNZGNZ
    GNZXBOUBUCMVLVLVMEEEUBLUIZXEUVCXBUVGXAUVAXDUVBGWSVLWTGRWSVLXCGRSUHUCLUIZUVC
    UVFXBUVHUVAWLUVBUVEGWTVLVLGUJUVHXCUVDVLGWTVLXBGUJTSUHMUAUIZUVFWMXBVMUVIUVEV
    OWLGUVIUVDVNVLGXBVMVLGRTTUVIUTUKUSURVBZWKXGUUIWKXOXGAXOWDWEKUNYEUMUUSVBSSUV
    JVCVDVEVDVEVRWDVQUEZLUFWIVQLEVFUVKWHLVQWGWDVPUAEVFVGVHVIVJVPWCVSVMVSGNZGNZV
    MOLUABCEELBUIZVOUVMVMUVNVLVSVNUVLGUVNUTVLVSVMGUJSUHUACUIZUVMWBVMVTUVOUVLWAV
    SGVMVTVSGRTUVOUTUKVKUM $.
$}

[savask]

> As a side note, Tirix is now close to completing the proof of the Eckmann-Hilton argument, and although his version is better organized than mine, it still looks pretty long. I guess now we can say that the short proof on Wikipedia doesn't convey a good idea about the amount of work needed to accomplish that task.

Yes, I'm surprised that this is the case, probably shows the lack of intuition on my side. When I showed the problem set to Mario, he suggested rewriting some statements with class variables, i.e. instead of "A. a e. B A. b e. B ( a .o. b ) = ( b .o. a)" one can introduce "X e. B" and "Y e. B" as hypotheses and write "( X .o. Y ) = ( Y .o. X )". In the end I did that only for a couple of first problems, since I wasn't sure how these additional hypotheses work with scoping etc. Thierry is using that technique in his repository, yet it seems the overall proof length is also large.

I plan to add another 3 "bonus" tasks near the end of next week, asking to prove the Mendelsohn-Padmanabhan identity in a boolean group (so we get a full characterization). Again, this is trivial mathematically but I'm not quite sure it will be trivial in metamath, although we have all the required definitions like group exponent (gEx) ready.

[Gino Giotto]

Ninth theorem proved:

${
  $d x y z a b v B $.  $d x y z a b v .o. $.  $d v ph $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.
  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( First part of ~ mendpadmlem5 $)
  mendpadmlem5a $p |- ( ph -> A. x e. B ( x .o. ( x .o. x ) ) = x ) $=
    ( vv va vb cv co wceq wral weq id wcel wa impac mendpadmlem4 adantr oveq12d
    idd oveq2 eqeq1d oveq1 oveq2d eqeq12d cbvral2vw sylib rspc2v sylc ralrimiva
    cbvralvw ) ALOZUSUSGPZGPZUSQZLERBOZVCVCGPZGPZVCQZBERAVBLEAUSEUAZUBZVGVGUBMO
    ZNOZVIGPZGPZVJQZNERMERZVBAVGVGAVGUGUCVHVCCOZVCGPZGPZVOQZCERBERZVNAVSVGABCDE
    FGHIJKUDUEVRVMVIVOVIGPZGPZVOQBCMNEEBMSZVQWAVOWBVCVIVPVTGWBTVCVIVOGUHUFUICNS
    ZWAVLVOVJWCVTVKVIGVOVJVIGUJUKWCTULUMUNVMVBUSVJUSGPZGPZVJQMNUSUSEEMLSZVLWEVJ
    WFVIUSVKWDGWFTVIUSVJGUHUFUINLSZWEVAVJUSWGWDUTUSGVJUSUSGUJUKWGTULUOUPUQVBVFL
    BELBSZVAVEUSVCWHUSVCUTVDGWHTZWHUSVCUSVCGWIWIUFUFWIULURUN $.

  $d a b ph $.
  $( Second part of ~ mendpadmlem5 $)
  mendpadmlem5b $p |- ( ph -> A. x e. B ( ( x .o. x ) .o. x ) = x ) $=
    ( vv va vb cv co wceq wral weq oveq12d wcel wa mendpadmlem4 adantr id oveq2
    eqeq1d oveq1 oveq2d eqeq12d cbvral2vw sylib cmgm w3a 3anim1i 3anidm23 mgmcl
    simplr simpr eqcomd mendpadmlem5a cbvralvw rspcdva ad2antrr eqtr3d rspcimdv
    syl rspcdv mpd ralrimiva sylibr ) ALOZVLGPZVLGPZVLQZLERBOZVPGPZVPGPZVPQZBER
    AVOLEAVLEUAZUBZMOZNOZWBGPZGPZWCQZNERZMERZVOWAVPCOZVPGPZGPZWIQZCERBERZWHAWMV
    TABCDEFGHIJKUCUDWLWFWBWIWBGPZGPZWIQBCMNEEBMSZWKWOWIWPVPWBWJWNGWPUEZVPWBWIGU
    FTUGCNSZWOWEWIWCWRWNWDWBGWIWCWBGUHUIWRUEUJUKULWAWGVOMVMEWAFUMUAZVTVTUNZVMEU
    AAVTWTAWSVTVTJUOUPEFVLVLGHIUQVGWAWBVMQZUBZWFVONVLEAVTXAURXBNLSZUBZWEVNWCVLX
    DWBVMWDVLGWAXAXCURZXDVLVMGPZWDVLXDVLWCVMWBGXDWCVLXBXCUSZUTXDWBVMXEUTTWAXFVL
    QZXAXCWAWBWBWBGPZGPZWBQZXHMEVLMLSZXJXFWBVLXLWBVLXIVMGXLUEZXLWBVLWBVLGXMXMTT
    XMUJWAVPVQGPZVPQZBERZXKMERAXPVTABCDEFGHIJKVAUDXOXKBMEWPXNXJVPWBWPVPWBVQXIGW
    QWPVPWBVPWBGWQWQTTWQUJVBULAVTUSVCVDVETXGUJVHVFVIVJVSVOBLEBLSZVRVNVPVLXQVQVM
    VPVLGXQVPVLVPVLGXQUEZXRTXRTXRUJVBVK $.

  $( Lemma for mendpadm. Multiplication of ` x ` by ` x .o. x ` gives ` x ` . $)
  mendpadmlem5 $p |- ( ph -> A. x e. B ( ( x .o. ( x .o. x ) ) = x /\ ( ( x .o. x ) .o. x ) = x ) ) $=
    ( cv co wceq wral wa mendpadmlem5a mendpadmlem5b r19.26 sylanbrc ) ABLZUAUA
    GMZGMUANZBEOUBUAGMUANZBEOUCUDPBEOABCDEFGHIJKQABCDEFGHIJKRUCUDBEST $.
$}

[Gino Giotto]

Tenth theorem proved:

${
  $d x y z a b c u v B $.  $d x y z a b c u v .o. $.  $d a u v ph $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.
  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( Lemma for mendpadm. Squares of all elements are equal to each other. $)
  mendpadmlem6 $p |- ( ph -> A. x e. B A. y e. B ( x .o. x ) = ( y .o. y ) ) $=
    ( vu vv va vb co wceq wral weq oveq2d vc cv wi wal wa mendpadmlem4 id oveq2
    wcel oveq12d eqeq1d oveq1 eqeq12d cbvral2vw sylib ad2antrr simpr eqidd cmgm
    simplr syl3anc rspc2vd mpd cbvral3vw rspc3v eqtr3d ex alrimiv df-ral imbi2i
    mgmcl albii sylbbr syl eqeq2d ) ALUBZVPGPZMUBZVRGPZQZMERZLERZBUBZWCGPZCUBZW
    EGPZQZCERBERAVPEUIZVREUIZVTUCZMUDZUCZLUDZWBAWLLAWHWKAWHUEZWJMWNWIVTWNWIUEZV
    RVQVRGPZGPZVQVSWONUBZOUBZWRGPZGPZWSQZOERNERZWQVQQZAXCWHWIAWCWEWCGPZGPZWEQZC
    ERBERXCABCDEFGHIJKUFXGXBWRWEWRGPZGPZWEQBCNOEEBNSZXFXIWEXJWCWRXEXHGXJUGWCWRW
    EGUHUJUKCOSZXIXAWEWSXKXHWTWRGWEWSWRGULTXKUGUMUNUOUPZWOXDVRWSVRGPZGPZWSQXBNO
    VRVQEEENMSZXAXNWSXOWRVRWTXMGXOUGWRVRWSGUHUJUKWSVQQZXNWQWSVQXPXMWPVRGWSVQVRG
    ULTXPUGUMWNWIUQZWOXOUEEURWOFUSUIZWHWHVQEUIAXRWHWIJUPAWHWIUTZXSEFVPVPGHIVKVA
    VBVCWOWPVRVRGWOVQVPVRVPGPZGPZGPZWPVRWOYAVRVQGWOXCYAVRQZXLWOYCVPWSVPGPZGPZWS
    QXBNOVPVREEENLSZXAYEWSYFWRVPWTYDGYFUGWRVPWSGUHUJUKOMSZYEYAWSVRYGYDXTVPGWSVR
    VPGULTYGUGUMXSWOYFUEEURXQVBVCTWOWRWSGPZWRUAUBZWSGPZGPZGPZYIQZUAEROERNERZYBV
    RQZAYNWHWIAWCWEGPZWCDUBZWEGPZGPZGPZYQQZDERCERBERYNKUUAYMWRWEGPZWRYRGPZGPZYQ
    QYHWRYQWSGPZGPZGPZYQQBCDNOUAEEEXJYTUUDYQXJYPUUBYSUUCGWCWRWEGULWCWRYRGULUJUK
    XKUUDUUGYQXKUUBYHUUCUUFGWEWSWRGUHXKYRUUEWRGWEWSYQGUHTUJUKDUASZUUGYLYQYIUUHU
    UFYKYHGUUHUUEYJWRGYQYIWSGULTTUUHUGUMVDUOUPWOWHWHWIYNYOUCXSXSXQYMYOVPWSGPZVP
    YJGPZGPZYIQVQVPYIVPGPZGPZGPZYIQNOUAVPVPVREEEYFYLUUKYIYFYHUUIYKUUJGWRVPWSGUL
    WRVPYJGULUJUKOLSZUUKUUNYIUUOUUIVQUUJUUMGWSVPVPGUHUUOYJUULVPGWSVPYIGUHTUJUKU
    AMSZUUNYBYIVRUUPUUMYAVQGUUPUULXTVPGYIVRVPGULTTUUPUGUMVEVAVCVFTVFVGVHVGVHWBW
    HWAUCZLUDWMWALEVIUUQWLLWAWKWHVTMEVIVJVLVMVNVTWGWDVSQLMBCEELBSZVQWDVSUURVPWC
    VPWCGUURUGZUUSUJUKMCSZVSWFWDUUTVRWEVRWEGUUTUGZUVAUJVOUNUO $.
$}

> Yes, I'm surprised that this is the case, probably shows the lack of intuition on my side. When I showed the problem set to Mario, he suggested rewriting some statements with class variables, i.e. instead of "A. a e. B A. b e. B ( a .o. b ) = ( b .o. a)" one can introduce "X e. B" and "Y e. B" as hypotheses and write "( X .o. Y ) = ( Y .o. X )". In the end I did that only for a couple of first problems, since I wasn't sure how these additional hypotheses work with scoping etc. Thierry is using that technique in his repository, yet it seems the overall proof length is also large.

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.

[David A. Wheeler]

> On Dec 1, 2024, at 12:49 AM, savask <sav...@yandex.ru> wrote:
>
> Programmers have a nice tradition of solving a small puzzle or coding task on each day of advent, Advent of Code being one of the most famous examples. ...

>
> This year I suggest a new challenge, a set of 16 small problems about magmas:
> https://gist.github.com/savask/f7a3b46663aa16e5dd48f8bfaba3e3e5

Thanks for organizing this!

> ... Of course, the first person to formalize some result can claim it for themselves and put it in their mathbox.

That sounds great as a starting point.

However, at least some of these problems seem general and/or interesting.
I hope that at least some of these theorems will eventually end up in the "main" area,
instead of in a mathbox. Once a theorem is in the main area, it's easier for other proofs
to build on it.

--- David A. Wheeler

[Gino Giotto]

I proved the eleventh theorem. As anticipated by Savask, this is the first one using nonemptyness.

${
  $d x y z a b u v B $.  $d x y z a b u v .o. $.  $d M u v $.  $d u v a b ph $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.

  mendpadm.c $e |- ( ph -> B =/= (/) ) $.

  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( Lemma for mendpadm. ` M ` has an identity element. $)
  mendpadmlem7 $p |- ( ph -> ( 0g ` M ) e. B ) $=
    ( vv vu vb co wceq wa wral oveq12d va c0g cfv eqid wrex wne wcel weq eleq1a
    cv c0 simpr anim1ci mendpadmlem6 id eqeq1d eqeq2d cbvral2vw ad2antrr rspc2v
    sylib sylc syl9r imp31 eqeq12d anbi12d mendpadmlem5 cbvralvw ralbii rspcdv2
    ex ancom ralrimiva wi r19.2zb biimpi cmgm w3a 3anim1i 3anidm23 mgmcl syl wb
    simpl eqcomd ad4ant24 rspcdv ralrimdva rspcimedv rexlimdva mpd mgmidcl ) AM
    EGNFFUBUCZHWMUDIAUAUJZWNGPZOUJZGPZWPQZWPWOGPZWPQZRZOESZUAEUEZNUJZMUJZGPZXEQ
    ZXEXDGPZXEQZRZMESZNEUEZAEUKUFZXBUAESZXCJAXBUAEAWNEUGZRZXAOEXPWPEUGZRZXEXEGP
    ZXEGPZXEQZXEXSGPZXEQZRZXAMWPEXRMOUHZRZYAWRYCWTYFXTWQXEWPYFXSWOXEWPGXPXQYEXS
    WOQZXQYEXEEUGZXPYGWPEXEUIXPYHYGXPYHRYHXORXDXDGPZWPWPGPZQZOESNESZYGXPXOYHAXO
    ULUMAYLXOYHABUJZYMGPZCUJZYOGPZQZCESBESYLABCDEFGHIKLUNYQYKYIYPQBCNOEEBNUHZYN
    YIYPYRYMXDYMXDGYRUOZYSTUPCOUHZYPYJYIYTYOWPYOWPGYTUOZUUATUQURVAUSYKYGXSYJQNO
    XEWNEENMUHZYIXSYJUUBXDXEXDXEGUUBUOZUUCTUPOUAUHZYJWOXSUUDWPWNWPWNGUUDUOZUUET
    UQUTVBVKVCVDZXRYEULZTUUGVEYFYBWSXEWPYFXEWPXSWOGUUGUUFTUUGVEVFXPXQULAYDMESZX
    OXQAYCYARZMESZUUHAYMYNGPZYMQZYNYMGPZYMQZRZBESUUJABCDEFGHIKLVGUUOUUIBMEBMUHZ
    UULYCUUNYAUUPUUKYBYMXEUUPYMXEYNXSGUUPUOZUUPYMXEYMXEGUUQUUQTZTUUQVEUUPUUMXTY
    MXEUUPYNXSYMXEGUURUUQTUUQVEVFVHVAUUIYDMEYCYAVLVIVAUSVJVMVMXMXNXCVNXBUAEVOVP
    VBAXBXLUAEXPXKXBNWOEXPFVQUGZXOXOVRZWOEUGAXOUUTAUUSXOXOKVSVTEFWNWNGHIWAWBXPX
    DWOQZRZXBXJMEUVBYHRXAXJOXEEUVBYHULUVAOMUHZXAXJWCXPYHUVAUVCRZWRXGWTXIUVDWQXF
    WPXEUVDWOXDWPXEGUVDXDWOUVAUVCWDWEZUVAUVCULZTUVFVEUVDWSXHWPXEUVDWPXEWOXDGUVF
    UVETUVFVEVFWFWGWHWIWJWKWL $.
$}

I found this one to be more challenging than the previous ones, not because of its length, but rather because there were a few steps that, when taken in the wrong direction, lead me to dead ends. Finding a strategy that worked all the way from the beginning to the end required some nontrivial consideration (it might very well be that you won't feel the same, this is my experience).

[Gino Giotto]

Twelfth theorem proved. Nonemptiness is not used.

I used  mendpadmlem5a (proved above) instead of  mendpadmlem5 to make the proof a little shorter.

${
  $d x y z a b c u v B $.  $d x y z a b c u v .o. $.  $d u v ph $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.

  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( First part of ~ mendpadmlem8 $)
  mendpadmlem8a $p |- ( ph -> A. x e. B A. y e. B ( x .o. ( x .o. y ) ) = y ) $=
    ( vu va co wceq wral weq id oveq12d oveq2d vv vb wcel mendpadmlem5a eqeq12d
    vc cv wa eqcom bitrdi rspcv mpan9 cbvralvw sylib simpr rspcdva mendpadmlem6
    adantr adantlr ad2antrr eqeq1d eqeq2d eqidd simpl rspc2vd adantll mpd eqtrd
    oveq1 oveq2 cbvral3vw simplr cmgm mgmcl syl3anc rspc3v ralrimiva cbvral2vw
    wi ) ALUGZVTUAUGZGNZGNZWAOZUAEPZLEPBUGZWFCUGZGNZGNZWGOZCEPBEPAWELEAVTEUCZUH
    ZWDUAEWLWAEUCZUHZWCVTVTVTGNZGNZVTWAWOGNZGNZGNZWAWNVTWPWBWRGWLVTWPOZWMAWFWFW
    FGNZGNZWFOZBEPZWKWTABCDEFGHIJKUDZXCWTBVTEBLQZXCWPVTOWTXFXBWPWFVTXFWFVTXAWOG
    XFRZXFWFVTWFVTGXGXGSSXGUEWPVTUIUJUKULURWNWAWQVTGWNWAWAWAWAGNZGNZWQAWMWAXIOZ
    WKAWMUHMUGZXKXKGNZGNZXKOZXJMEWAMUAQZXNXIWAOXJXOXMXIXKWAXOXKWAXLXHGXORZXOXKW
    AXKWAGXPXPSSXPUEXIWAUIUJAXNMEPZWMAXDXQXEXCXNBMEBMQZXBXMWFXKXRWFXKXAXLGXRRZX
    RWFXKWFXKGXSXSSSXSUEUMUNURAWMUOUPUSWNXHWOWAGWNXAWGWGGNZOZCEPBEPZXHWOOZAYBWK
    WMABCDEFGHIJKUQUTWKWMYBYCVSAWKWMUHZYCXHXTOYABCWAVTEEEBUAQZXAXHXTYEWFWAWFWAG
    YERZYFSVACLQZXTWOXHYGWGVTWGVTGYGRZYHSVBWKWMUOYDYEUHEVCWKWMVDVEVFVGTVHTSWNXK
    UBUGZGNZXKUFUGZYIGNZGNZGNZYKOZUFEPUBEPMEPZWSWAOZWNWHWFDUGZWGGNZGNZGNZYROZDE
    PCEPBEPZYPAUUCWKWMKUTUUBYOXKWGGNZXKYSGNZGNZYROYJXKYRYIGNZGNZGNZYROBCDMUBUFE
    EEXRUUAUUFYRXRWHUUDYTUUEGWFXKWGGVIWFXKYSGVISVACUBQZUUFUUIYRUUJUUDYJUUEUUHGW
    GYIXKGVJUUJYSUUGXKGWGYIYRGVJTSVADUFQZUUIYNYRYKUUKUUHYMYJGUUKUUGYLXKGYRYKYIG
    VITTUUKRUEVKUNWNWKWOEUCZWMYPYQVSAWKWMVLZWNFVMUCZWKWKUULAUUNWKWMJUTUUMUUMEFV
    TVTGHIVNVOWLWMUOYOYQVTYIGNZVTYLGNZGNZYKOWPVTYKWOGNZGNZGNZYKOMUBUFVTWOWAEEEM
    LQZYNUUQYKUVAYJUUOYMUUPGXKVTYIGVIXKVTYLGVISVAYIWOOZUUQUUTYKUVBUUOWPUUPUUSGY
    IWOVTGVJUVBYLUURVTGYIWOYKGVJTSVAUFUAQZUUTWSYKWAUVCUUSWRWPGUVCUURWQVTGYKWAWO
    GVITTUVCRUEVPVOVGVHVQVQWDWJWFWFWAGNZGNZWAOLUABCEELBQZWCUVEWAUVFVTWFWBUVDGUV
    FRVTWFWAGVISVAUACQZUVEWIWAWGUVGUVDWHWFGWAWGWFGVJTUVGRUEVRUN $.

  $( Second part of ~ mendpadmlem8 $)
  mendpadmlem8b $p |- ( ph -> A. x e. B A. y e. B ( ( x .o. y ) .o. y ) = x ) $=
    ( vu vv cv co wceq wral wcel weq id wa mendpadmlem8a ad2antrr oveq1 oveq12d
    wi eqeq1d oveq2 oveq2d eqeq12d rspc2v eqcom syl6ib adantll mpd mendpadmlem4
    simplr simpr mgmcl syl3anc syl2anc eqtrd ralrimiva oveq1d cbvral2vw sylib
    cmgm ) ALNZMNZGOZVIGOZVHPZMEQZLEQBNZCNZGOZVOGOZVNPZCEQBEQAVMLEAVHERZUAZVLME
    VTVIERZUAZVKVJVHVJGOZGOZVHWBVIWCVJGWBVNVPGOZVOPZCEQBEQZVIWCPZAWGVSWAABCDEFG
    HIJKUBUCVSWAWGWHUFAVSWAUAWGWCVIPZWHWFWIVHVHVOGOZGOZVOPBCVHVIEEBLSZWEWKVOWLV
    NVHVPWJGWLTVNVHVOGUDUEUGCMSZWKWCVOVIWMWJVJVHGVOVIVHGUHUIWMTUJUKWCVIULUMUNUO
    UIWBVNVOVNGOZGOZVOPZCEQBEQZWDVHPZAWQVSWAABCDEFGHIJKUPUCWBVJERZVSWQWRUFWBFVG
    RZVSWAWSAWTVSWAJUCAVSWAUQZVTWAUREFVHVIGHIUSUTXAWPWRVJVOVJGOZGOZVOPBCVJVHEEV
    NVJPZWOXCVOXDVNVJWNXBGXDTVNVJVOGUHUEUGCLSZXCWDVOVHXEXBWCVJGVOVHVJGUDUIXETUJ
    UKVAUOVBVCVCVLVRVNVIGOZVIGOZVNPLMBCEELBSZVKXGVHVNXHVJXFVIGVHVNVIGUDVDXHTUJM
    CSZXGVQVNXIXFVPVIVOGVIVOVNGUHXITUEUGVEVF $.

  $( Lemma for mendpadm. Multiplying two times from the left or right by the same element gives the original element. $)
  mendpadmlem8 $p |- ( ph -> A. x e. B A. y e. B ( ( x .o. ( x .o. y ) ) = y /\ ( ( x .o. y ) .o. y ) = x ) ) $=
    ( cv co wceq wral wa mendpadmlem8a mendpadmlem8b r19.26-2 sylanbrc ) ABLZUA
    CLZGMZGMUBNZCEOBEOUCUBGMUANZCEOBEOUDUEPCEOBEOABCDEFGHIJKQABCDEFGHIJKRUDUEBC
    EEST $.
$}

[savask]

> 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.

[Gino Giotto]

I removed some DV conditions from my previous proof of aabbaa to use it in mendpadmlem9. Proofs for  mendpadmlem10  and  mendpadmlem11  are also provided.

${
  $( If multiplying two times from the left (and the right) is an identity

     mapping, then the operation is commutative. $)
  $d a b u B $.  $d b u X $.  $d b u Y $.  $d a b u .o. $.  $d u ph $.

  aabbaa.a $e |- ( ph -> A. a e. B A. b e. B ( a .o. b ) e. B ) $.
  aabbaa.b $e |- ( ph -> A. a e. B A. b e. B ( a .o. ( a .o. b ) ) = b ) $.
  aabbaa.c $e |- ( ph -> A. a e. B A. b e. B ( ( b .o. a ) .o. a ) = b ) $.
  aabbaa.d $e |- ( ph -> X e. B ) $.
  aabbaa.e $e |- ( ph -> Y e. B ) $.

  aabbaa $p |- ( ph -> ( X .o. Y ) = ( Y .o. X ) ) $=
    ( vu co wceq wral oveq2 id oveq12d eqeq1d weq ralbidv cbvralvw sylib bitrdi
    cv eqcom oveq1 oveq1d eqeq12d wa eqidd wcel eleq1d rspc2vd mpd oveq2d eqtrd
    ) ACDENZUSCENZCENZDCENAGUFZMUFZENZVCENZVBOZGBPZMBPZUSVAOZAVBFUFZENZVJENZVBO
    ZGBPZFBPVHJVNVGFMBFMUAZVMVFGBVOVLVEVBVOVKVDVJVCEVJVCVBEQVORZSTUBUCUDZAVIVBV
    BCENZCENZOZVFMGCUSBBBVCCOZVFVSVBOVTWAVEVSVBWAVDVRVCCEVCCVBEQWARSTVSVBUGUEVB
    USOZVBUSVSVAWBRWBVRUTCEVBUSCEUHUIUJKAWAUKBULZAVCVBENZBUMZGBPZMBPZUSBUMZAVJV
    BENZBUMZGBPZFBPWGHWKWFFMBVOWJWEGBVOWIWDBVJVCVBEUHZUNUBUCUDAWHCVBENZBUMWEMGC
    DBBBWAWDWMBVCCVBEUHUNVBDOZWMUSBVBDCEQUNKWCLUOUPZUOUPAUTDCEAUTUSUSDENZENZDAC
    WPUSEAVHCWPOZVQAWRVBVBDENZDENZOZVFMGDCBBBVCDOZVFWTVBOXAXBVEWTVBXBVDWSVCDEVC
    DVBEQXBRSTWTVBUGUEVBCOZVBCWTWPXCRXCWSUSDEVBCDEUHUIUJLAXBUKBULKUOUPUQAVCWDEN
    ZVBOZGBPZMBPZWQDOZAVJWIENZVBOZGBPZFBPXGIXKXFFMBVOXJXEGBVOXIXDVBVOVJVCWIWDEV
    PWLSTUBUCUDAXHUSUSVBENZENZVBOXEMGUSDBBBVCUSOZXDXMVBXNVCUSWDXLEXNRVCUSVBEUHS
    TWNXMWQVBDWNXLWPUSEVBDUSEQUQWNRUJWOAXNUKBULLUOUPURUIUR $.
$}

${
  $d x y z a b c u v w B $.  $d x y z a b c u v w .o. $.  $d a b c u v w ph $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.
  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( Lemma for mendpadm. Multiplication is commutative. $)
  mendpadmlem9 $p |- ( ph -> A. x e. B A. y e. B ( x .o. y ) = ( y .o. x ) ) $=
    ( vu vb va cv co wceq wral wcel weq vv wa cmgm ad2antrr simpr mgmcl syl3anc
    simplr ralrimiva oveq1 eleq1d oveq2 cbvral2vw sylib mendpadmlem8a id eqeq1d
    oveq12d oveq2d eqeq12d mendpadmlem8b ralcom aabbaa ) ALOZUAOZGPZVEVDGPZQZU
    AERZLERBOZCOZGPZVKVJGPZQZCERBERAVILEAVDESZUBZVHUAEVPVEESZUBZEVDVEGCBAVMESZB
    ERCERZVOVQAMOZNOZGPZESZNERZMERVTAWEMEAWAESZUBZWDNEWGWBESZUBFUCSZWFWHWDAWIWF
    WHJUDAWFWHUHWGWHUEEFWAWBGHIUFUGUIUIWDVSVKWBGPZESMNCBEEMCTZWCWJEWAVKWBGUJZUK
    NBTZWJVMEWBVJVKGULZUKUMUNUDAVKVMGPZVJQZBERCERZVOVQAWAWCGPZWBQZNERMERZWQAVJV
    LGPZVKQZCERBERWTABCDEFGHIJKUOXBWSWAWAVKGPZGPZVKQBCMNEEBMTZXAXDVKXEVJWAVLXCG
    XEUPVJWAVKGUJURUQCNTZXDWRVKWBXFXCWCWAGVKWBWAGULUSXFUPUTUMUNWSWPVKWJGPZWBQMN
    CBEEWKWRXGWBWKWAVKWCWJGWKUPWLURUQWMXGWOWBVJWMWJVMVKGWNUSWMUPUTUMUNUDVRVLVKG
    PVJQZCERBERZXHBERCERAXIVOVQABCDEFGHIJKVAUDXHBCEEVBUNAVOVQUHVPVQUEVCUIUIVHVN
    VJVEGPZVEVJGPZQLUABCEELBTVFXJVGXKVDVJVEGUJVDVJVEGULUTUACTXJVLXKVMVEVKVJGULV
    EVKVJGUJUTUMUN $.

  $( Lemma for mendpadm. Multiplication is associative. $)
  mendpadmlem10 $p |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) $=
    ( va vb co wceq wral weq oveq2 oveq1 oveq2d vu vv wcel mendpadmlem4 oveq12d
    vw vc cv wa eqeq1d eqeq12d cbvral2vw sylib ad3antrrr simpllr eqidd ad2antrr
    id cmgm simplr simpr syl3anc adantr rspc2vd mpd mendpadmlem8b oveq1d rspc2v
    mgmcl wi adantll cbvral3vw rspc3v 3eqtr3rd eqtr3d ralrimiva ) AUAUHZUBUHZGN
    ZUFUHZGNZVQVRVTGNZGNZOZUFEPZUBEPZUAEPBUHZCUHZGNZDUHZGNZWGWHWJGNZGNZOZDEPCEP
    BEPAWFUAEAVQEUCZUIZWEUBEWPVREUCZUIZWDUFEWRVTEUCZUIZVQWAVQGNZGNZWAWCWTLUHZMU
    HZXCGNZGNZXDOZMEPLEPZXBWAOZAXHWOWQWSAWGWHWGGNZGNZWHOZCEPBEPXHABCDEFGHIJKUDX
    LXGXCWHXCGNZGNZWHOBCLMEEBLQZXKXNWHXOWGXCXJXMGXOURZWGXCWHGRUEUJCMQZXNXFWHXDX
    QXMXEXCGWHXDXCGSTXQURZUKULUMUNWTXIVQXDVQGNZGNZXDOXGLMVQWAEEELUAQZXFXTXDYAXC
    VQXEXSGYAURZXCVQXDGRUEUJXDWAOZXTXBXDWAYCXSXAVQGXDWAVQGSTYCURUKAWOWQWSUOWTYA
    UIEUPWTFUSUCZVSEUCZWSWAEUCAYDWOWQWSJUNZWRYEWSWRYDWOWQYEAYDWOWQJUQAWOWQUTWPW
    QVAEFVQVRGHIVIVBVCZWRWSVAZEFVSVTGHIVIVBVDVEWTXAWBVQGWTWAVSWBVTGNZGNZGNZWAVS
    VRGNZGNWBXAWTYJYLWAGWTYIVRVSGWTXCXDGNZXDGNZXCOZMEPLEPZYIVROZAYPWOWQWSAWIWHG
    NZWGOZCEPBEPYPABCDEFGHIJKVFYSYOXCWHGNZWHGNZXCOBCLMEEXOYRUUAWGXCXOWIYTWHGWGX
    CWHGSZVGXPUKXQUUAYNXCXQYTYMWHXDGWHXDXCGRZXRUEUJULUMUNZWQWSYPYQVJWPYOYQVRXDG
    NZXDGNZVROLMVRVTEELUBQZYNUUFXCVRUUGYMUUEXDGXCVRXDGSVGUUGURUKMUFQZUUFYIVRUUH
    UUEWBXDVTGXDVTVRGRUUHURUEUJVHVKVETTWTYMXCUGUHZXDGNZGNZGNZUUIOZUGEPMEPLEPZYK
    WBOZAUUNWOWQWSAWIWGWJWHGNZGNZGNZWJOZDEPCEPBEPUUNKUUSUUMYTXCUUPGNZGNZWJOYMXC
    WJXDGNZGNZGNZWJOBCDLMUGEEEXOUURUVAWJXOWIYTUUQUUTGUUBWGXCUUPGSUEUJXQUVAUVDWJ
    XQYTYMUUTUVCGUUCXQUUPUVBXCGWHXDWJGRTUEUJDUGQZUVDUULWJUUIUVEUVCUUKYMGUVEUVBU
    UJXCGWJUUIXDGSTTUVEURUKVLUMUNWTYEWSWBEUCZUUNUUOVJYGYHWTYDWQWSUVFYFWPWQWSUTY
    HEFVRVTGHIVIVBUUMUUOVSXDGNZVSUUJGNZGNZUUIOWAVSUUIVTGNZGNZGNZUUIOLMUGVSVTWBE
    EEXCVSOZUULUVIUUIUVMYMUVGUUKUVHGXCVSXDGSXCVSUUJGSUEUJUUHUVIUVLUUIUUHUVGWAUV
    HUVKGXDVTVSGRUUHUUJUVJVSGXDVTUUIGRTUEUJUUIWBOZUVLYKUUIWBUVNUVKYJWAGUVNUVJYI
    VSGUUIWBVTGSTTUVNURUKVMVBVEWTYLVQWAGWTYPYLVQOZUUDWRYPUVOVJZWSWOWQUVPAYOUVOV
    QXDGNZXDGNZVQOLMVQVREEYAYNUVRXCVQYAYMUVQXDGXCVQXDGSVGYBUKMUBQZUVRYLVQUVSUVQ
    VSXDVRGXDVRVQGRUVSURUEUJVHVKVCVETVNTVOVPVPVPWDWNWGVRGNZVTGNZWGWBGNZOWIVTGNZ
    WGWHVTGNZGNZOUAUBUFBCDEEEUABQZWAUWAWCUWBUWFVSUVTVTGVQWGVRGSVGVQWGWBGSUKUBCQ
    ZUWAUWCUWBUWEUWGUVTWIVTGVRWHWGGRVGUWGWBUWDWGGVRWHVTGSTUKUFDQZUWCWKUWEWMVTWJ
    WIGRUWHUWDWLWGGVTWJWHGRTUKVLUM $.

  $d a b c M $.
  mendpadm.c $e |- ( ph -> B =/= (/) ) $.
  $( Lemma for mendpadm. ` M ` is a group. $)
  mendpadmlem11 $p |- ( ph -> M e. Grp ) $=
    ( vb vu wceq wcel co wral eqeq12d oveq12d va vc c0g cfv cbs a1i cplusg cmgm
    mgmcl syl3an1 w3a mendpadmlem10 weq oveq1 oveq1d oveq2d rspc3v mendpadmlem7
    cv oveq2 mpan9 mendpadmlem5b id cbvralvw sylib wi simpr ax-1 eleq1a anabsi5
    wa im2anan9 3anim1i 3anidm23 syl mendpadmlem6 ad2antrr eqeq1d eqeq2d rspc2v
    ancoms adantll mpd rspccv eqtr3d mendpadmlem5a adantr grpidd rspcdv ex mpid
    imp simplll simpllr adantl 3jca 3ad2ant1 3adant1 rspcdv2 pm3.22 sylc isgrpd
    ) AUAMUBEGFUAUSZFUCUDZEFUEUDOZAHUFGFUGUDOZAIUFAFUHPZXCEPZMUSZEPZXCXIGQZEPJE
    FXCXIGHIUIUJABUSZCUSZGQZDUSZGQZXLXMXOGQZGQZOZDERCERBERXHXJUBUSZEPUKXKXTGQZX
    CXIXTGQZGQZOZABCDEFGHIJKULXSYDXCXMGQZXOGQZXCXQGQZOXKXOGQZXCXIXOGQZGQZOBCDXC
    XIXTEEEBUAUMZXPYFXRYGYKXNYEXOGXLXCXMGUNUOXLXCXQGUNSCMUMZYFYHYGYJYLYEXKXOGXM
    XIXCGUTUOYLXQYIXCGXMXIXOGUNUPSDUBUMZYHYAYJYCXOXTXKGUTYMYIYBXCGXOXTXIGUTUPSU
    QVAABCDEFGHILJKURAXHXDXCGQZXCOZAXHXIXIGQZXIGQZXIOZMERZYOAXLXLGQZXLGQZXLOZBE
    RZYSABCDEFGHIJKVBZUUBYRBMEBMUMZUUAYQXLXIUUEYTYPXLXIGUUEXLXIXLXIGUUEVCZUUFTU
    UFTUUFSVDVEAXHYSYOVFAXHVKZYRYOMXCEAXHVGZUUGMUAUMZVKZYQYNXIXCUUJYPXDXIXCGUUJ
    AXJVKZYPXDOUUGUUIUUKAUUGAXHUUIXJAUUGVHXCEXIVIVLVJUUKUAEGFYPXEUUKHUFXFUUKIUF
    UUKXGXJXJUKZYPEPAXJUULAXGXJXJJVMVNEFXIXIGHIUIVOUUKXHVKZXCXCGQZXCGQZYPXCGQXC
    UUMUUNYPXCGUUMYTXMXMGQZOZCERBERZUUNYPOZAUURXJXHABCDEFGHIJKVPZVQXJXHUURUUSVF
    ZAXHXJUVAUUQUUSUUNUUPOBCXCXIEEYKYTUUNUUPYKXLXCXLXCGYKVCZUVBTZVRYLUUPYPUUNYL
    XMXIXMXIGYLVCZUVDTVSVTWAWBWCZUOUUKXHUUOXCOZAUUCXJXHUVFVFZUUDUUCUVGVFXJUUBUV
    FBXCEYKUUAUUOXLXCYKYTUUNXLXCGUVCUVBTUVBSWDUFVAWLWEUUMXCUUNGQZXCYPGQXCUUMUUN
    YPXCGUVEUPUUKXHUVHXCOZAXHUVIVFZXJAXLYTGQZXLOZBERZUVJABCDEFGHIJKWFZUVLUVIBXC
    EYKUVKUVHXLXCYKXLXCYTUUNGUVBUVCTUVBSWDVOWGWLWEWHVOUUGUUIVGZTUVOSWIWJWKWLUUH
    UUGMEGFUUNXEUUGHUFXFUUGIUFUUGXGXHXHUKZUUNEPAXHUVPAXGXHXHJVMVNEFXCXCGHIUIVOU
    UGXJVKZNUSZUVRGQZUVRGQZUVROZUUNXIGQZXIONXIEUVQNMUMZVKZUVTUWBUVRXIUWDUVSUUNU
    VRXIGUWDAXHUVREPZUKZUVSUUNOZUWDAXHUWEAXHXJUWCWMAXHXJUWCWNUVQUWCUWEXJUWCUWEV
    FUUGXIEUVRVIWOWLWPZUWFUURUWGAXHUURUWEUUTWQZXHUWEUURUWGVFZAUWEXHUWJUUQUWGUVS
    UUPOBCUVRXCEEBNUMZYTUVSUUPUWKXLUVRXLUVRGUWKVCZUWLTZVRCUAUMZUUPUUNUVSUWNXMXC
    XMXCGUWNVCZUWOTVSVTZWAWRWCVOUVQUWCVGZTUWQSUUGXJVGZAUWANERZXHXJAUUCUWSUUDUUB
    UWABNEUWKUUAUVTXLUVRUWKYTUVSXLUVRGUWMUWLTUWLSVDVEVQWSUVQUVRUVSGQZUVROZXIUUN
    GQZXIONXIEUWDUWTUXBUVRXIUWDUVRXIUVSUUNGUWQUWDUWFUWGUWHUWFUWEXHVKZUURUWGXHUW
    EUXCAXHUWEWTWRUWIUWPXAVOTUWQSUWRAUXANERZXHXJAUVMUXDUVNUVLUXABNEUWKUVKUWTXLU
    VRUWKXLUVRYTUVSGUWLUWMTUWLSVDVEVQWSWHXB $.

$}

There is a bit of a conflict between proof length and amount of DV conditions. So far, I've been inclined to prefer fewer DV conditions at the cost of longer proofs, because theorems can be used more easily later, as in the example above. What version do people usually prefer?  

[Glauco]

>There is a bit of a conflict between proof length and amount of DV conditions.

>So far, I've been inclined to prefer fewer DV conditions at the cost of longer proofs, because theorems can be used more easily later, as in the example above.

>What version do people usually prefer?  

My vote, in general, is for fewer DV conditions, even at the cost of a longer proof.

I also prefer using nf* over cbv*, as it makes the intent clearer.

[Gino Giotto]

Last theorem of the original challenge proved:

${
  $d x y z a b B $.  $d x y z a b .o. $.  $d a b ph $.  $d M a b x $.

  mendpadm.a $e |- B = ( Base ` M ) $.
  mendpadm.b $e |- .o. = ( +g ` M ) $.

  mendpadm.c $e |- ( ph -> B =/= (/) ) $.

  mendpadm.d $e |- ( ph -> M e. Mgm ) $.
  mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z ) $.

  $( Boolean groups (i.e. abelian groups of exponent 2), can be defined by one identity.
     Here we use a short identity from a 1972 paper of N.S. Mendelsohn and R. Padmanabhan. $)
  mendpadm $p |- ( ph -> ( M e. Abel /\ A. x e. B ( x .o. x ) = ( 0g ` M ) ) ) $=
    ( vb va wcel co wceq wral weq oveq12d cabl cv c0g cfv cbs a1i mendpadmlem11
    cplusg wa wi wal mendpadmlem9 oveq1 oveq2 eqeq12d cbvral2vw r19.21bi df-ral
    sylib 19.21bi 3impia isabld eqid adantr simpr mgmcl syl3anc mendpadmlem6 id
    eqeq1d eqcom bitrdi rspc2v adantll oveq1d mendpadmlem5b rspcv mpan9 adantlr
    cmgm mpd eqtr3d oveq2d mendpadmlem5a ismgmid2 ralrimiva cbvralvw jca ) AFUA
    OBUBZWIGPZFUCUDZQZBERZAMNEGFEFUEUDQAHUFGFUHUDQAIUFABCDEFGHIKLJUGAMUBZEOZNUB
    ZEOZWNWPGPZWPWNGPZQZAWOUIZWQWTUJZNXAWTNERZXBNUKAXCMEAWICUBZGPZXDWIGPZQZCERB
    ERXCMERABCDEFGHIKLULXGWTWNXDGPZXDWNGPZQBCMNEEBMSZXEXHXFXIWIWNXDGUMWIWNXDGUN
    UOCNSXHWRXIWSXDWPWNGUNXDWPWNGUMUOUPUSUQWTNEURUSUTVAVBAWPWPGPZWKQZNERWMAXLNE
    AWQUIZMEGXKFWKHWKVCIXMFVTOZWQWQXKEOAXNWQKVDAWQVEZXOEFWPWPGHIVFVGXMWOUIZWNWN
    GPZWNGPZXKWNGPWNXPXQXKWNGXPWJXDXDGPZQZCERBERZXQXKQZXMYAWOAYAWQABCDEFGHIKLVH
    VDVDWQWOYAYBUJAXTYBXSXKQZBCWPWNEEBNSZXTXKXSQYCYDWJXKXSYDWIWPWIWPGYDVIZYETVJ
    XKXSVKVLCMSZXSXQXKYFXDWNXDWNGYFVIZYGTVJVMVNWAZVOAWOXRWNQZWQAWJWIGPZWIQZBERW
    OYIABCDEFGHIKLVPYKYIBWNEXJYJXRWIWNXJWJXQWIWNGXJWIWNWIWNGXJVIZYLTZYLTYLUOVQV
    RVSWBXPWNXQGPZWNXKGPWNXPXQXKWNGYHWCAWOYNWNQZWQAWIWJGPZWIQZBERWOYOABCDEFGHIK
    LWDYQYOBWNEXJYPYNWIWNXJWIWNWJXQGYLYMTYLUOVQVRVSWBWEWFXLWLNBENBSZXKWJWKYRWPW
    IWPWIGYRVIZYSTVJWGUSWH $.
$}

Every theorem of the original challenge now has a proof (either by me or Thierry).  

[Gino Giotto]

First four bonus theorems proved. Proofs are quite short.

${
  $d x y z a B $.  $d x y z a .o. $.  $d M a $.
  mendpadmbi.a $e |- B = ( Base ` M ) $.
  mendpadmbi.b $e |- .o. = ( +g ` M ) $.
  mendpadmbi.c $e |- B =/= (/) $.
  mendpadmbi.d $e |- M e. Mgm $.

  ${
    $d E x a $.
    $( Lemma for mendpadmbi. Mendelsohn-Padmanabhan identity implies that ` x .o. x ` is the group identity for all ` x ` . $)
    mendpadmbilem1.a $e |- E = ( 0g ` M ) $.
    mendpadmbilem1 $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z -> A. x e. B ( x .o. x ) = E ) $=
      ( va cv co wceq wral wcel a1i weq cabl c0g cfv c0 wne cmgm oveq12d eqeq1d
      oveq1 2ralbidv cbvralvw biimpi mendpadm id eqtr4di ralimi simpl2im sylib
      ) ANZBNZGOZUSCNZUTGOZGOZGOZVBPZCDQBDQZADQZMNZVIGOZEPZMDQZUSUSGOZEPZADQVHF
      UARVJFUBUCZPZMDQVLVHMBCDFGHIDUDUEVHJSFUFRVHKSVHVIUTGOZVIVCGOZGOZVBPZCDQBD
      QZMDQVGWAAMDAMTZVFVTBCDDWBVEVSVBWBVAVQVDVRGUSVIUTGUIUSVIVCGUIUGUHUJUKULUM
      VPVKMDVPVJVOEVPUNLUOUPUQVKVNMADMATZVJVMEWCVIUSVIUSGWCUNZWDUGUHUKUR $.

    $( Lemma for mendpadmbi. Mendelsohn-Padmanabhan identity implies that ` x ` to the power of ` 2 ` is the group identity for all ` x ` . $)
    mendpadmbilem2.a $e |- .x. = ( .g ` M ) $.
    mendpadmbilem2 $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z -> A. x e. B ( 2 .x. x ) = E ) $=
      ( cv co wceq wral c2 mendpadmbilem1 wcel mulg2 eqeq2 syl5ibcom ralimia
      syl ) AOZBOZHPUGCOZUHHPHPHPUIQCDRBDRADRUGUGHPZFQZADRSUGEPZFQZADRABCDFGHIJ
      KLMTUKUMADUGDUAULUJQUKUMDHEGUGINJUBUJFULUCUDUEUF $.
  $}

  $( Lemma for mendpadmbi. Mendelsohn-Padmanabhan identity implies that the group exponent is at most 2. $)
  mendpadmbilem3 $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z -> ( gEx ` M ) e. ( 1 ... 2 ) ) $=
    ( va cmgm wcel c2 cv co wceq wral cfv eqid cn cmg c0g cgex c1 cfz 2nn oveq1
    weq oveq12d eqeq1d 2ralbidv cbvralvw mendpadmbilem2 sylbi gexlem2 mp3an12i
    ) ELMNUAMAOZBOZFPZURCOZUSFPZFPZFPZVAQZCDRBDRZADRZNKOZEUBSZPEUCSZQKDRZEUDSZU
    ENUFPMJUGVGVHUSFPZVHVBFPZFPZVAQZCDRBDRZKDRVKVFVQAKDAKUIZVEVPBCDDVRVDVOVAVRU
    TVMVCVNFURVHUSFUHURVHVBFUHUJUKULUMKBCDVIVJEFGHIJVJTZVITZUNUOKVIVLENLDVJGVLT
    VTVSUPUQ $.

  $( Lemma for mendpadmbi. Mendelsohn-Padmanabhan identity implies that the group exponent divides 2. $)
  mendpadmbilem4 $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z -> ( gEx ` M ) || 2 ) $=
    ( cv co wceq wral c1 c2 wcel cdvds wbr id cgex cfv cfz mendpadmbilem3 elpri
    wo cpr fz12pr eleq2s cz 2z 1dvds ax-mp eqbrtrdi z2even jaoi 3syl ) AKZBKZFL
    URCKZUSFLFLFLUTMCDNBDNADNEUAUBZOPUCLZQVAOMZVAPMZUFZVAPRSZABCDEFGHIJUDVEVAOP
    UGVBVAOPUEUHUIVCVFVDVCVAOPRVCTPUJQOPRSUKPULUMUNVDVAPPRVDTUOUNUPUQ $.
$}

[savask]

> Last theorem of the original challenge proved:

Congratulations!

> First four bonus theorems proved. Proofs are quite short.

Yes, but the last two proofs are probably going to be a bit longer, since I didn't split them into chunks as small.

[Gino Giotto]

One theorem left:

${
  $d x y a b B $.  $d x y a b .o. $.  $d M a b $.

  mendpadmbi.a $e |- B = ( Base ` M ) $.
  mendpadmbi.b $e |- .o. = ( +g ` M ) $.

  $( Lemma for mendpadmbi. In a group of exponent dividing 2 we have ` x .o. x .o. y = y ` for all ` x ` and ` y ` . $)
  mendpadmbilem5a $p |- ( ( M e. Grp /\ ( gEx ` M ) || 2 ) -> A. x e. B A. y e. B ( x .o. ( x .o. y ) ) = y ) $=
    ( va vb wcel cfv c2 wa cv co wceq wral eqid 3ad2ant2 3eqtr3rd cgrp cgex wbr
    cdvds c0g cmg gexid adantl w3a 3anan32 gexdvdsi eqcomd sylbir eqtr3d adantr
    mulg2 oveq1d grplid ad4ant14 simplll simplr simpr grpass syl13anc ralrimiva
    weq id oveq1 oveq12d eqeq1d oveq2 oveq2d eqeq12d cbvral2vw sylib ) DUAJZDUB
    KZLUDUCZMZHNZVTINZEOZEOZWAPZICQZHCQANZWFBNZEOZEOZWGPZBCQACQVSWEHCVSVTCJZMZW
    DICWLWACJZMZDUEKZWAEOZVTVTEOZWAEOZWAWCWNWOWQWAEWLWOWQPWMWLVQVTDUFKZOZWOWQWK
    WTWOPVSVTWSVQDCWOFVQRZWSRZWORZUGZUHWLVPWKVRUIZWTWQPVPWKVRUJXELVTWSOZWOWQWTV
    TWSVQDLCWOFXAXBXCUKWKVPXFWQPVRCEWSDVTFXBGUPSWKVPWOWTPVRWKWTWOXDULSTUMUNUOUQ
    VPWMWPWAPVRWKCEDWAWOFGXCURUSWNVPWKWKWMWRWCPVPVRWKWMUTVSWKWMVAZXGWLWMVBCEDVT
    VTWAFGVCVDTVEVEWDWJWFWFWAEOZEOZWAPHIABCCHAVFZWCXIWAXJVTWFWBXHEXJVGVTWFWAEVH
    VIVJIBVFZXIWIWAWGXKXHWHWFEWAWGWFEVKVLXKVGVMVNVO $.

  $( Lemma for mendpadmbi. In an abelian group of exponent dividing 2 we have ` x .o. x .o. y = y ` for all ` x ` and ` y ` . $)
  mendpadmbilem5 $p |- ( ( M e. Abel /\ ( gEx ` M ) || 2 ) -> A. x e. B A. y e. B ( x .o. ( x .o. y ) ) = y ) $=
    ( cabl wcel cgrp cgex cfv c2 cdvds wbr cv co wceq wral ablgrp sylan
    mendpadmbilem5a ) DHIDJIDKLMNOAPZUCBPZEQEQUDRBCSACSDTABCDEFGUBUA $.
$}

[Gino Giotto]

Last theorem proved:

${
  $d x y z a b c B $.  $d x y z a b c .o. $.  $d M a b c $.

  mendpadmbi.a $e |- B = ( Base ` M ) $.
  mendpadmbi.b $e |- .o. = ( +g ` M ) $.

  mendpadmbi.c $e |- B =/= (/) $.
  mendpadmbi.d $e |- M e. Mgm $.

  $( Boolean groups are characterized by an identiy of N.S. Mendelsohn and R. Padmanabhan. $)
  mendpadmbi $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x .o. ( z .o. y ) ) ) = z <-> ( M e. Abel /\ ( gEx ` M ) || 2 ) ) $=
    ( va vb vc cv co wceq wral wcel oveq1 oveq2d cabl cgex cfv c2 cdvds wbr c0g
    wa wne a1i cmgm weq oveq12d eqeq1d 2ralbidv cbvralvw biimpi mendpadm simpld
    c0 mendpadmbilem4 jca cgrp wi simpl ablgrp grpass 3exp2 3syl mendpadmbilem5
    imp41 ad3antrrr mgmcl mp3an1 oveq2 eqeq12d rspc2v sylan adantlll mpd ablcom
    id ad5ant145 3eqtr3rd ralrimiva cbvral3vw sylib impbii ) ANZBNZFOZWICNZWJFO
    ZFOZFOZWLPZCDQBDQZADQZEUARZEUBUCUDUEUFZUHZWRWSWTWRWSKNZXBFOEUGUCPKDQWRKBCDE
    FGHDUTUIWRIUJEUKRZWRJUJWRXBWJFOZXBWMFOZFOZWLPZCDQBDQZKDQWQXHAKDAKULZWPXGBCD
    DXIWOXFWLXIWKXDWNXEFWIXBWJFSWIXBWMFSUMUNUOUPUQURUSABCDEFGHIJVAVBXAXBLNZFOZX
    BMNZXJFOZFOZFOZXLPZMDQZLDQZKDQWRXAXRKDXAXBDRZUHZXQLDXTXJDRZUHZXPMDYBXLDRZUH
    ZXKXKXLFOZFOZXKXBXJXLFOZFOZFOXLXOYDYEYHXKFXAXSYAYCYEYHPZXAWSEVCRZXSYAYCYIVD
    VDVDWSWTVEEVFYJXSYAYCYIDFEXBXJXLGHVGVHVIVKTYDWIWKFOZWJPZBDQADQZYFXLPZXAYMXS
    YAYCABDEFGHVJVLXSYAYCYMYNVDZXAXSYAUHXKDRZYCYOXCXSYAYPJDEXBXJFGHVMVNYLYNXKXK
    WJFOZFOZWJPABXKXLDDWIXKPZYKYRWJYSWIXKWKYQFYSWBWIXKWJFSUMUNBMULZYRYFWJXLYTYQ
    YEXKFWJXLXKFVOTYTWBVPVQVRVSVTYDYHXNXKFYDYGXMXBFWSYAYCYGXMPWTXSDFEXJXLGHWAWC
    TTWDWEWEWEXPWPWIXJFOZWIXMFOZFOZXLPWKWIXLWJFOZFOZFOZXLPKLMABCDDDKAULZXOUUCXL
    UUGXKUUAXNUUBFXBWIXJFSXBWIXMFSUMUNLBULZUUCUUFXLUUHUUAWKUUBUUEFXJWJWIFVOUUHX
    MUUDWIFXJWJXLFVOTUMUNMCULZUUFWOXLWLUUIUUEWNWKFUUIUUDWMWIFXLWLWJFSTTUUIWBVPW
    FWGWH $.
$}

I guess this is the end. Nice challenge, I enjoyed it.

[samiro.d...@rwth-aachen.de]

> Last theorem proved:

> [...]

> Nice challenge, I enjoyed it

Congratulations!  Despite being very busy with my own challenge I actually enjoyed watching this.

[Mario Carneiro]

Part 2 is, of course, making a version of this which is suitable for set.mm.

--
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 visit https://groups.google.com/d/msgid/metamath/27f7b052-78a8-4b02-b269-0e817bb9bb65n%40googlegroups.com.

[Gino Giotto]

>  Part 2 is, of course, making a version of this which is suitable for set.mm.

Sure. I committed all my proofs in my own fork of set.mm https://github.com/GinoGiotto/set.mm/tree/christmas. All verifiers are green https://github.com/GinoGiotto/set.mm/actions/runs/12335559653.

[Thierry Arnoux]

I've also been posting my progress here:

https://github.com/tirix/christmas24.mm/commits

https://github.com/tirix/christmas24.mm/blob/master/christmas24.mm

I limited myself to one theorem a day, so I should reach the last theorem of the original list around Christmas day.

Some of my proofs seem shorter, but I have not run the minimizer.

BR,
_
Thierry

On 15/12/2024 05:02, Gino Giotto wrote:

>  Part 2 is, of course, making a version of this which is suitable for set.mm.

Sure. I committed all my proofs in my own fork of set.mm https://github.com/GinoGiotto/set.mm/tree/christmas. All verifiers are green https://github.com/GinoGiotto/set.mm/actions/runs/12335559653.

--
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 visit https://groups.google.com/d/msgid/metamath/beb9b41c-2f01-4b1b-94d1-734203474e44n%40googlegroups.com.

[savask]

> I guess this is the end. Nice challenge, I enjoyed it.

Nice, glad you liked it.

I also agree with Mario that it would be nice to have this in set.mm, in a mathbox or elsewhere. Gino has been mostly using theorem formulations which I suggested (apart from some d-conditions and superfluous hypotheses), but I often like Thierry's treatment better, since he reformulates theorems in a way which make them easier to use or to prove. Maybe in the end you could combine both efforts, and push a "mixed" version into set.mm where some theorems are double-credited like "contributed by GG and TA" or "contributed by GA, revised by TA" etc, where one could select "the best" approach in each case.

[David A. Wheeler]

> On Dec 17, 2024, at 11:14 PM, savask <sav...@yandex.ru> wrote:
>
> > I guess this is the end. Nice challenge, I enjoyed it.
>
> Nice, glad you liked it.
>
> I also agree with Mario that it would be nice to have this in set.mm, in a mathbox or elsewhere.

I agree! I'd love to see this in the shared databases, at least in mathboxes.
As soon as they're ready, I'd really like to see at least some of these promoted
to the "main" section.

--- David A. Wheeler

[Gino Giotto]

If you're eager to have these theorems in the shared database I can commit my proofs first, but it might be more strategic to wait for Thierry to finish his work.

[savask]

Merry Christmas to everyone!

Advent of metamath has ended - both Gino and Thierry finished formalizing all problems, including the bonus ones. There has also been some contributions from Igor and icecream17 on github, so overall I think this year's challenge was a success.

In my opinion it would be nice to try to formalize a more "serious" result in a similar manner, maybe even a metamath 100 theorem - first we formalize the statements (without proofs), and then the proofs would be crowdsourced (I think that was the general idea of Thierry's blueprints project). Other proof assistants used this technique to a great benefit, and I think this year's advent showed that even our small metamath community can do the same.

Happy holidays to everyone once again!

[Gino Giotto]

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).

[Thierry Arnoux]

Hi all,

We could certainly include those proofs in set.mm, crediting both Gino and myself. I'll see if I can propose a PR. It will not be perfect at first, but they can be reworked to remove hypotheses, DV conditions and axiom dependencies.

BR,
_
Thierry

--
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 visit https://groups.google.com/d/msgid/metamath/73427ff3-25ac-48ec-bad2-39b6cf80e41en%40googlegroups.com.