> There you go: (solution of Day 20) Thanks! I haven't been able to find this proof anywhere in the literature, so this might be a useful reference for some other people as well. There seems to be ongoing work on formalizing modal logics in HOL Light, in particular, they have an automatic prover for GL https://link.springer.com/article/10.1007/s10817-023-09677-z Maybe in the worst case one could try to extract the proof from this utility, though I'm not sure if it's possible.
> So far, I made almost all proofs by hand (in metamath.exe) without any help. ... I've been using metamath lamp to formalize the proofs, and I've been sometimes wondering if its proof searching utility is missing some short arguments. I haven't tried comparing it with metamath.exe's improve command, though. > Note: I believe ~puzzlelem requires ~ax-gl for its proof, even tho there was no "now you can use ~ax-gl again" in the comment. Yes, days 21 - 24 are "ax-gl free", and at day 25 you're allowed to use ax-gl 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/b6b66bbe-298a-405a-a59c-c997629513b9n%40googlegroups.com.
