Proof Ground

Interactive Proving Contests

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:

  1. Manuel Eberl and Peter Lammich (Isabelle/HOL)
  2. Floris van Doorn and Simon Hudon (Lean)
  3. Fabian Kunze (Coq)

Who Should Attend?

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.

Important Dates

Submission deadline: August 9, 2019

Workshop and Competition: September 13, 2019


During the Workshop we want to


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.

Call for Problems

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:

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