# Proof Ground 2021 - Call for Problems

**URL:** <https://discourse.rocq-prover.org/t/proof-ground-2021-call-for-problems/1259>\
**Category:** Announcements\
**Created:** [April 2, 2021, 8:43am UTC](https://discourse.rocq-prover.org/t/proof-ground-2021-call-for-problems/1259 "2021-04-02T08:43:10Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![maxhaslbeck](https://avatars.discourse-cdn.com/v4/letter/m/e95f7d/32.png) [@maxhaslbeck](https://discourse.rocq-prover.org/u/maxhaslbeck)\
**Post date:** [April 2, 2021, 8:43am UTC](https://discourse.rocq-prover.org/t/proof-ground-2021-call-for-problems/1259/1 "2021-04-02T08:43:10Z")

</div>

Dear Coq enthusiasts,

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

* * *

## Call for Problems

* * *

## Proof Ground 2021 Interactive Proving Contest June 28, 2021 [Proof Ground 2021](https://www21.in.tum.de/~wimmers/proofground/)

at ITP 2021  
Interactive Theorem Proving  
June 29 - July 2, 2021, (originally in) Rome, Italy, now fully virtual  
[https://easyconferences.eu/itp2021/](https://easyconferences.eu/itp2021/)

* * *

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](https://do.proof.in.tum.de) is currently used for  
teaching and hosting proving contests in Coq, Isabelle, and Lean.

Proof Ground 2021 is affiliated with the conference on [Interactive  
Theorem Proving 2021](https://easyconferences.eu/itp2021/).

As the main conference will happen as virtual conferences due to the  
ongoing Covid-19 pandemic, Proof Ground 2021 will also take a purely  
virtual format.

The [first edition](https://www21.in.tum.de/~wimmers/proofground2019/) of  
the workshop has been held at [ITP 2019](https://itp19.cecs.pdx.edu/).  
The [second edition](https://www21.in.tum.de/~wimmers/proofground2020/)  
was affiliated with [IJCAR 2020](https://ijcar2020.org/).

Important Dates

- Submission deadline: May 30, 2021

- Workshop and Competition: June 28, 2021

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:

- should contain an informal statement of the problem together with a  
template for the formal proof;

- should come with a reference solution (in any ITP);

- should be solvable (including formal proof) within 30 minutes;

- should be easy to state in any proof assistant, without requiring  
too much background library;

- could be from any part of mathematics, software verification, or  
your daily work with ITPs, and could also be a logic puzzle/riddle;

- could contain several subproblems which lead to partial points.

Submissions from (potential) competition participants are allowed.

Examples can be found at the current “Proving for Fun” contest system,  
e.g. [here](https://do.proof.in.tum.de/competitions/contest/6/).

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

Organizers

Maximilian P. L. Haslbeck  
Simon Wimmer  
Tobias Nipkow