A quite popular tradition among software engineers is to solve one small programming task on each day of advent (for example, see Advent of Code). Last year we did the same thing but for formalizing small theorems about magmas in Metamath, and to a great success!

This year's new set of problems is about modal logics.

The problems deal with the provability logic GL which can be used to express some famous results like Godel's second theorem and its implications. Although it might seem like an involved topic requiring deep knowledge of logic and proof theory, one doesn't need to know any complex mathematics at all - all one needs is a good enough grasp on usual propositional proofs (let's say up to theorem wex in set.mm) and the rest is explained in the file.