This is an unofficial reimagining of the Archive of Formal Proofs
Lifting the Exponentby Jakub Kądziołka
Solution to the xkcd Blue Eyes puzzleby Jakub Kądziołka