On the 23rd of April 2014, the first ever live theorem-proving competition was held at FP-SYD, with predictably great results.
The six contestants, fueled by nothing by alcoholic beverages and armed only with their favorite Coq environment and a handful of basic tactics, set out to prove a set of challenging lemmas in elimination rounds of five minutes or less.
Commentary/sledging was provided helpfully by our commentary team, including Boey Maun Suang, Thomas Sewell and Erik de Castro Lopo (as well as our contestants on the sidelines).
The final rankings were:
- Amos Robinson
- Liam O’Connor (me!)
- Tony Sloane
- Dom De Re and Eric Willigers (tied)
- Ben Lippmeier
Amos took home the chicken trophy, and a good time was had by all. It’s a remarkably fun event, both for those watching (many of whom were not familiar with Coq or theorem proving), and for those participating (I found it quite exhilirating!).
Many thanks go to Ben Lippmeier who organised basically everything and calibrated each lemma for difficulty, and to Atlassian for hosting FP-SYD.