Stream: General

Topic: Proving for Fun


view this post on Zulip maximilian p.l. haslbeck (Jul 31 2019 at 08:45):

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.

https://competition.isabelle.systems/competitions/contest/11/

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

Happy proving!

view this post on Zulip Hanna Lachnitt (Jul 31 2019 at 13:13):

Looks cool thanks for sharing the link :)

view this post on Zulip maximilian p.l. haslbeck (Aug 12 2019 at 13:31):

The "July 2019" contest at Proving for Fun is over now.
Congratulations to the winners and thanks to all the participants.
We hope you had some fun solving this month's problems and proving them formally.

We have set up a github repository with a summary of the contest, sample solutions and discussions about the problems. Feel free to participate in commenting any task in its issue and publishing your solution with a pull-request.

We specially want to thank the people who helped making the contest possible by creating the tasks and translating them to their proof assistant: Armaël Guéneau, Sebastiaan Joosten, Kevin Kappelmann, Simon Wimmer.

You still can submit your solutions for the tasks of the "July 2019" contest, they are now integrated into the "All Time" contest.

Tomorrow, Aug 13 at noon (MESZ) we start the "August 2019" contest which will be open until Sep 12 midnight. It also serves as a preparation for the contest happening at the Proof Ground workshop Sep 13 alongside the ITP conference in Portland.

view this post on Zulip maximilian p.l. haslbeck (Aug 13 2019 at 10:04):

August 2019 Contest is open for submissions now. Have fun :) !

view this post on Zulip maximilian p.l. haslbeck (Sep 13 2019 at 16:23):

Today we will have the Proof Ground workshop here in Portland. We will have two contests, one before lunch (10:30 - 12:30 (PDT)) and one after lunch (14:00 - 15:30 (PDT)). Feel free to participate from anywhere on earth and have fun by solving and mechanizing the tasks :).

view this post on Zulip maximilian p.l. haslbeck (Sep 13 2019 at 17:32):

The morning session is starting now. You can see the problems here and submit solutions: https://competition.isabelle.systems/competitions/contest/13/

view this post on Zulip maximilian p.l. haslbeck (Sep 13 2019 at 21:18):

The afternoon session has started. https://competition.isabelle.systems/competitions/contest/14/


Last updated: Aug 15 2022 at 02:13 UTC