Problem submissions for Advent Of Proof

Stream: general

[Alex Brodbelt]

Hi!

TypeSig is a University of Edinburgh student society with a focus on programming language theory and theorem provers. Our 300 members include undergraduates, Master's and PhD students. Last year, we hosted the Advent of Proof, with submissions from across the UK and even other countries. Daily challenges were released 1st-24th of December. The challenges were self-contained puzzles to be solved in Lean or Agda by filling in holes / sorry left by starter code. The topics were beginner-friendly/intermediate level, and ranged from logic puzzles to proving properties of lambda calculus. Check out last year's problems here: AoP2023 (Discord account required; no information processed or stored).

Last year's problems and the platform were kindly provided by Dr Liam O'Connor, and TypeSig is very grateful for his support. This year, we want to run the event again 12th-24th of December, but we need contributors to make it happen. Would you like to submit 1-2 problems? Contributors will be given credit on the Advent of Proof platform, our website and Discord community.

A problem submission includes:

• a brief text/graphic presentation
• a complete solution in Lean or Agda
• starter code with holes / sorry

If interested, please send an email to president@typesig.pl with the number of problems you'd like to contribute. We'll provide a form for file uploads. The event is set to start December 12, but submissions can come a few days later too.

Thank you for your interest! :octopus:

[Violeta Hernández]

Can we participate in the event, or is it exclusive for university students?

[Alex Brodbelt]

Everyone can participate!