This Workshop brings together researchers of the ITP community to discuss and compete in “proving contests”.
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 prototype contest system is currently used for teaching and hosting proving contests in Isabelle. While support for Coq and Lean is under development, we welcome the development of backends for any other Proof Assistant.
The workshop will be organized around an onsite contest, supplemented with informal presentations and discussions.
The workshop is part of ITP 2019.
Proof Ground 2019 is over! The winning teams are:
For the discussions, participation is open for anybody interested. We invite users and developer of all Proof Assistants to join in a discussion on how proving contests
For the contest, teams of up to two people are allowed. Physical presence on site is required. We will at least provide automatic grading for Coq, Isabelle, and Lean. But participants that use other proof assistants can compete as well.
Submission deadline: August 9, 2019
Workshop and Competition: September 13, 2019
During the Workshop we want to
present the idea of “proving contests”, the status quo of a prototype system to support such contests and a tutorial on how to use it;
conduct a contest using the prototype (solutions can be submitted in Coq/Isabelle/Lean and more) and have fun solving interesting problems and formalizing their solutions in our favourite ITP;
present the results of the contest, award prizes and discuss participants’ solutions;
discuss further ideas on the requirements and prospects of proving contests with the participants and community.
| Time | What? |
|---|---|
| 09:00-10:00 | Intro & competition system tutorial |
| 10:00-10:30 | Coffe break |
| 10:30-12:30 | Competition I |
| 12:30-14:00 | Lunch |
| 14:00-15:30 | Competition II |
| 15:30-16:00 | Coffee break |
| 16:00-17:30 | Results & plenary discussion |
All times are given for the PDT time zone.
In order to conduct an interesting and stimulating contest during the workshop 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.
Submissions can be made via email to wimmers [at] in [dot] tum [dot] de by the date indicated above.