Second Annual FP-Syd Coq Fight


Last night was the second annual FP-Syd Coq Fight, the only competitive theorem proving event in the world! Here are some notes and a recording of the final round live stream. Posted by Thomas Sutton on June 24, 2015

The FP-Syd Coq Fight is an annual event in which Coq users demonstrate their prowess in competitive theorem proving. Each bout sees two competitors race to prove a lemma before their opponent and before the timer runs out.

It didn’t even occur to me that we might broadcast this prestigious sporting event live on the Internet until near the end of the event, so here is a recording of my Periscope live stream of the semi-final and final bouts.

This is the second time FP-Syd has had a Coq Fight and it again was far more enjoyable than the phrase “competitive theorem proving” might suggest. Indeed, there’s even been some suggestion that there could be a far less prestigious “minor leagues” Coq Fight at ICFP 2015 in Vancouver later this year.

If this sounds like fun keep your twitter client tuned to the #coqfight hashtag on Twitter.

This post was published on June 24, 2015 and last modified on December 4, 2019. It is tagged with: events, fp-syd, coq, theorem proving, competition, video.