TypeSig Advent of Proof 2023
...
...

Welcome

Welcome to TypeSig's Advent of Proof 2023! This is an alternative to Advent of Code that ran between Dec 1st to Dec 25th 2023, where the focus is instead on proving theorems in proof assistants!

Ranking criteria

Entries were ranked on correctness, number of hints used, and a special third criteria: a subjective evaluation of proof style from our judges. In particular, proving unnecessary theorems, using unnecessarily complicated methods, or unnecessary axiomatic dependencies reduce performance in this criteria, and brief, clear, well structured constructive proofs do well in this criteria.

We further measured the time taken between first opening a problem and submission, for tie-breaking purposes!

The leaderboards from the active competition are visible on the right hand side. Each question also has an individual leaderboard.

Prover Setup

Lean users are encouraged to use the online Lean playground for their solutions to avoid mathlib incompatibility issues. In each problem, links to the playground will be provided with the template code pre-loaded. The template may also be downloaded.
Agda users will need a working installation of a recent version of Agda with a compatible standard library. A downloadable template file will be provided with each problem.

Click one of the question buttons above to view the questions. Submissions are now closed, but the questions may still be viewed.