(reposting here the announcement on coq-club)
We are happy to announce a new proving contest at Proving for Fun, an online platform where you can tackle proving challenges in your favorite proof assistant:
While the platform was initially targeted at the Isabelle proof assistant, this month’s contest features freshly implemented support for Coq! This means you can now submit your solutions in both Isabelle and Coq. The contest is open starting now until 9 August 2019.
This also serves as a warmup for the “Proof Ground” workshop , which will take place in September alongside the ITP conference in Portland. The goal of the workshop is to bring together researchers from the ITP community, to discuss and compete in a “proving contest”, and it will use the Proving for Fun platform. If you happen to have ideas for interesting tasks, please consider submitting them following our “Call for Problems”.
We believe our problems should be a stimulating fun summer activity! We encourage you to participate and give us feedback on the prototype system.
Max Haslbeck, Simon Wimmer, and Armaël Guéneau