[isabelle] Proving for Fun: Summer Edition

Dear Isabelle enthusiasts,

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.


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 [1], 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 stimulating as a fun summer activity! We
also encourage you to participate and give us feedback on the prototype

Happy proving,
Armaël Guéneau
Max Haslbeck
Simon Wimmer

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.