From c0d745057fe42b1d40051c24fd723ac3e9feaed6 Mon Sep 17 00:00:00 2001
From: Amy Yin <76240283+yinamy@users.noreply.github.com>
Date: Thu, 12 Dec 2024 16:31:57 +0000
Subject: [PATCH] Create 2024-12-12-advent-of-proof-2024

---
 _posts/2024-12-12-advent-of-proof-2024 | 27 ++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 _posts/2024-12-12-advent-of-proof-2024

diff --git a/_posts/2024-12-12-advent-of-proof-2024 b/_posts/2024-12-12-advent-of-proof-2024
new file mode 100644
index 0000000..a67d24f
--- /dev/null
+++ b/_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}}