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/8a70fab7-c3a2-400a-9a43-1a7b07abcf43n%40googlegroups.com.
