Create 2024-12-12-advent-of-proof-2024

_posts/2024-12-12-advent-of-proof-2024

@@ -0,0 +1,27 @@
+---
+layout: post
+title:  "Advent of Proof 2024 Edition!"
+author: amy
+date:   2024-14-12 15:46:00 +0100
+image: assets/images/post-headers/aop-2024.png
+categories: lean agda events
+featured: false
+---
+
+TypeSig is pleased to announce that Advent of Proof is returning this year! [Click here to join in!][aop]
+
+We are grateful to the academics who supplied problems for us this year, and will credit them individually at the beginning of each problem when they are published. We also thank Dr Liam O'Connor for supplying the web infrastructure from last year's version of the event.  
+
+Each day from the 12th 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][discord-site] 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][discord], so feel free to join in the discussion over there!
+
+Good luck and have fun!
+
+[aop]: https://adventofproof.typesig.pl/
+[discord-site]: https://discord.gg
+[discord]: {{site.social.discord}}