Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Welcome!

Here at 'Proving for Fun' we host proving competitions and learning material for interactive theorem provers (ITPs) such as Isabelle.

This page briefly explains how to use the system and displays the current competitions. Particularly consider the Tutorial Competition when using the system for the first time, or when you want to learn more about Isabelle/HOL.

If you have any questions, feel free to contact us via email (details).

How to use the System

  • In order to compete in one of our competitions you first need to register.
  • On the right you find a list of the current and past competitions. By clicking on them you can view more details about them and see the list of problems. Further, you can view the problem statements, and—if the contest is still active—submit a solution.
  • For each contest you can also view the Leaderboard and see how you and your competitors perform.
  • When logged in, you can view all you submissions and their status by clicking 'Actions > Your submissions' in the navigation bar.

Problem Statements

Most problems that you will find here follow an overall structure. They contain:

  • A name,
  • a story that describes the problem in informal terms,
  • a theory Defs containing the necessary imports and definitions for the problem,
  • a theory Check containing the theorem(s) to be shown,
  • a template theory Submission which you can use to develop your solution in.

Here is an illustrative example for Isabelle:

Uno, dos, tres:
Isabelle is learning Spanish but still has problems with numbers: Can you help out?

theory Defs
 imports Main
begin
 definition "uno = 1"
end
theory Submission 
 imports Defs
begin
 lemma goal: "1=uno"
 sorry
end
theory Check
 imports Submission
begin 
 theorem "1=uno"
  by(rule Submission.goal)
end

Developing and Submitting Solutions

In order to develop a correct solution to a problem we recommend to save the three theories Defs, Submission and Check in a separate folder on your machine and edit Submission with Isabelle/jEdit. The Submission template theory usually contains the required theorems that you need to prove. The public Check theory tests whether the required problems are solved.

To submit your solution, just navigate to the appropriate submit form and upload only your Submission theory. On the 'View Submissions' page you can review the status of your submission and the leaderboard shows you how you perform relative to your competitors.

After receiving your Submission, its proofs will be checked together with the Defs and Check file. You will gain a point if Isabelle accepts your solution: be aware that proof holes (e.g. using sorry), and extra axioms (e.g. using axiomatization) are not allowed. Moreover, the proof-checking must terminate in under 10 seconds.

Competitions

Current


Past

  • June 2019
    (ended July 1, 2019, midnight)
    june contest 2019

  • ACF
    (ended Aug. 1, 2020, midnight)
    Exercises for the ACF Course (http://people.irisa.fr/Thomas.Genet/ACF/).

  • Test
    (ended April 30, 2020, 12:28 p.m.)
    Test for pusher

  • Proof Olympiad
    (ended Aug. 2, 2021, 4:10 p.m.)
    Welcome to the Proof Olympiad!

  • Isa21-1Test
    (ended Dec. 18, 2021, noon)
    .

  • Semantics Mock Exam 2022
    (ended Jan. 27, 2023, 11:17 a.m.)
    .


Further Information

This is a prototype system for hosting proving contests for Isabelle and other proof assistants. It was developed by Maximilian P.L. Haslbeck and Simon Wimmer. If you have any questions, want to host your own contest or tutorial, or want to extend the system for your favourite proof assistant, feel free to contact us via email.


Terms and Conditions