> 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 On Sunday, December 1, 2024 at 6:49:26 AM UTC+1 savask 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. Last year I tried to propose a similar initiative for Metamath, > namely Metamath Christmas challenge > <https://groups.google.com/g/metamath/c/91QTr-3TvN0>, 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 > <https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_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. > -- 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/cea595f7-3c6e-4740-9883-4e4de05b4700n%40googlegroups.com.
