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 <http://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 [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/beb9b41c-2f01-4b1b-94d1-734203474e44n%40googlegroups.com <https://groups.google.com/d/msgid/metamath/beb9b41c-2f01-4b1b-94d1-734203474e44n%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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/8ca7f971-06b3-424f-b03e-4fcaa8c33aad%40gmx.net.
