Advent of Proof

UPDATE: Advent of Proof 2023 has now concluded! Thank you all so much for participating, and helping to make this as large of a success as it was! And a large congratulations in particular to those who placed in the top 10. Well done!

TypeSig is proud to announce a new Advent of Code style competition, called Advent of Proof! Click here to join in!

Each day from the 1st of December to the 25th, we release a new theorem that you must formalise and prove using either Agda or Lean. Depending on how fast you solve it (from first opening the question), how many hints you used, and a secret third metric, you will score a glorious place on the leaderboard! The challenges are aimed at beginners/intermediates, with some basic experience with using Agda/Lean already.

You must have a Discord account to authenticate with the site. This is used for scoring and leaderboard purposes. We also have a discussion channel for the competition in our Discord server, so feel free to join in the discussion over there!

Good luck and have fun!