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. We welcome the development of backends for any other Proof Assistants.
Proof Ground 2021 is part of ITP 2021.
The workshop will be organized around an onsite contest, supplemented with informal presentations and discussions. As the main conferences has transitioned to an online format due to the COVID-19 pandemic, Proof Ground 2021 will also take a purely virtual format.
Two previous editions of the workshop have been held:
Submission deadline for problems: May 30, 2021
Workshop and Competition: June 28, 2021
During the Workshop we want to
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.
The contest phases will be organized through the competition system. Coffee breaks and discussions will be held virtually, via Zoom/Discord.
Due to its online nature, collaboration during the contest is discouraged. Participants should compete as individuals. We will at least provide automatic grading for Coq, Isabelle, and Lean, but participants that use other proof assistants can compete as well.
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
The contest phases will be organized through the competition system. Please register an account in advance. See below for more info.
Plenaries are happening on Zoom. You should already have received the link if you have registered for the workshop.
For coffee & lunch breaks, we consider to additionally use Discord (again). It requires no installation but registration. We will open to discussion during the first plenary whether to use Discord.
For further information/needs/difficulties (e.g. Zoom link), feel free to send us an email: wimmers [at] in [dot] tum [dot] de
This is a tentative schedule for the competition:
| Time | What? |
|---|---|
| 09:30-10:00 | Intro and Q&A |
| 10:00-10:20 | Meet Your Competitors |
| 10:20-10:30 | Competition Preparation |
| 10:30-12:30 | Competition I |
| 12:30-14:00 | Lunch/Open Discussion |
| 14:00-16:00 | Competition II |
| 16:00-16:30 | Coffee Break/Open Discussion |
| 16:30-17:30 | Results & Plenary Discussion |
All times refer to the CEST time zone.
The contest phases will be organized through the competition system. Please register an account in advance.
Our tasks have been prepared for the following systems:
opam packages:
coq 8.13.2coq-hammer-tactics 1.3.1+8.13coq-mathcomp-algebra 1.12.0coq-mathcomp-bigenough 1.0.0coq-mathcomp-fingroup 1.12.0coq-mathcomp-finmap 1.5.1coq-mathcomp-ssreflect 1.12.0coq-stdpp 1.5.0coq-tlc 20210316