Stream: General

Topic: Proof Ground 2020

view this post on Zulip maximilian p.l. haslbeck (May 12 2020 at 08:38):

Dear Isabelle enthusiasts,

we are organizing another edition of the proving competition workshop "Proof Ground", which will take place virtually.
Please notice our Call for Problems, and spread the word!

Call for Problems

Proof Ground 2020
Interactive Proving Contest
June 29, 2020

at IJCAR 2020
International Joint Conference on Automated Reasoning
June 29 - July 5, 2020, (originally in) Paris, France, now fully virtual

This workshop brings together researchers of the ITP community to compete in a "proving contest".

While programming contests (e.g. ACM ICPC, International Olympiad in Informatics) challenge large numbers of participants to solve algorithmic problems within a short time, we envision proving contests to entice proof engineers to formally prove small but interesting problems from mathematics or computer science.

A contest system is currently used for teaching and hosting proving contests in Coq, Isabelle, and Lean.

Proof Ground 2020 is part of the Paris Nord Summer of LoVe 2020, a joint event on LOgic and VErification at Université Paris 13, made of Petri Nets 2020, IJCAR 2020, FSCD 2020, and over 20 satellite events.

As the main conferences of Paris Nord Summer of LoVe will happen as virtual conferences due to the Covid-19 outbreak, Proof Ground will also take a purely virtual format.

The first edition of the workshop has been held at ITP 2019.

Important Dates

Call for Problems

In order to conduct a stimulating contest we solicit interesting tasks.

A contest typically lasts for two hours and consists of around five problems with varying difficulty.

A problem:

Submissions from (potential) competition participants are allowed.

Examples can be found at the current "Proving for Fun" contest system, e.g. here.

Submissions can be made via email to wimmers [at] in [dot] tum [dot] de by the date indicated above.


Maximilian P. L. Haslbeck
Tobias Nipkow
Simon Wimmer

view this post on Zulip maximilian p.l. haslbeck (Jun 18 2020 at 07:00):

The registration for the workshop is now open and it's free :
The competition will take place Monday June 29th, just before the Isabelle Workshop and IJCAR. For both participation is virtual and registration is free!

view this post on Zulip maximilian p.l. haslbeck (Jun 18 2020 at 07:00):

In the competition we will have two 1,5 hour contests, with some discussions and virtual coffee breaks in between. These will be organized with zoom. If you want to take part in those discussions, please do register for the workshop and specify your zoom account name. It is also possible to just participate in the online contest.

view this post on Zulip maximilian p.l. haslbeck (Jun 18 2020 at 07:01):

You can look at last year's problems here and here. You can prepare for the contest with these tasks and submit solutions in the AllTime contest.

Last updated: Dec 07 2023 at 08:19 UTC