Re: [Metamath] Advent of Metamath 2024

['David A. Wheeler' via Metamath]

> 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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion visit 
https://groups.google.com/d/msgid/metamath/B5463E30-3042-4D89-A998-1AD029B74F38%40dwheeler.com.