Merry Christmas to everyone! Advent of metamath has ended - both Gino <https://github.com/GinoGiotto/set.mm/tree/christmas> and Thierry <https://github.com/tirix/christmas24.mm> 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! -- 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/98e5664b-d78f-452d-8f03-afdbee401f60n%40googlegroups.com.
