Solutions to Proof Ground 2019

As a side event of ITP 2019, the interactive theorem proving competition Proof Ground took place. I joined up with my former colleague Peter ‘The Machine’ Lammich to form the team Sledgehammer Squad, and we ended up solving all the tasks and winning the competition.

Here you can find polished versions of our solutions. The original solutions were optimised for speed, not legibility, maintainability, or beauty (especially Peter's 😄). For the download here, I spent a little bit of effort to refine them some more to match the style that would be appropriate for the Isabelle distribution or the Archive of Formal Proofs.

Problem descriptions: here and here.

Our solutions: Download (.tar.gz, 4.4 KiB)