Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proof Ground 2021 Call for Participation

view this post on Zulip Email Gateway (Jun 18 2021 at 12:47):

From: Simon Wimmer <>

Call for Participation

Proof Ground 2021
Interactive Proving Contest
June 28, 2021

at ITP 2021
Interactive Theorem Proving
June 29 - July 2, 2021, (originally in) Rome, Italy, 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 [1] 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 [2].

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 competition itself will be run via the contest system,
while the workshop will provide a platform for discussion among the

The first edition of the workshop [3] has been held at ITP 2019 [4]. The
second edition [5] was affiliated with IJCAR 2020 [6].

Important Dates


Maximilian P. L. Haslbeck
Tobias Nipkow
Simon Wimmer


Last updated: Jan 27 2022 at 20:19 UTC