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

  • AllTime
    (ends Oct. 31, 2028, 12:29 p.m.)
    All tasks

  • Semantics 2024/2025
    (ends March 31, 2025, 11:59 p.m.)
    Semantics Winter Semester 2024/2025 @ TUM


Past

  • Tutorial
    (ended Sept. 11, 2020, 4:08 p.m.)
    How to use the contest system.

  • October
    (ended Oct. 31, 2018, 11:59 p.m.)
    Monthly Contest

  • Semantics 2018/19 (Archived)
    (ended March 31, 2019, 5:24 p.m.)
    Homework exercises for the winter term 2018/19 edition of the "Semantics of Progamming Languages" course @TUM.

  • November
    (ended Nov. 30, 2018, 11:59 p.m.)
    Monthly Contest

  • March 2019
    (ended March 31, 2019, 11:59 p.m.)
    Monthly Contest

  • FDS2019
    (ended Aug. 29, 2019, 3:51 p.m.)
    FDS Summer Semester 2019

  • July 2019
    (ended Aug. 10, 2019, midnight)
    Summer challenges

  • August 2019
    (ended Sept. 12, 2019, 11:59 p.m.)
    Monthly Contest.

  • Proof Ground 2019 - Morning
    (ended Sept. 13, 2019, 9:30 p.m.)
    The morning session of the Proof Ground 2019 Competition.

  • Proof Ground 2019 - Afternoon
    (ended Sept. 14, 2019, 12:30 a.m.)
    The afternoon session of the Proof Ground 2019 Competition.

  • Semantics 2019/20 (Archived)
    (ended March 31, 2020, midnight)
    Homework exercises for the winter term 2019/20 edition of the "Semantics of Programming Languages" course @TUM.

  • FDS 2020
    (ended Aug. 31, 2020, 4:06 p.m.)
    FDS Summer Semester 2020

  • Proof Ground 2020 - Morning
    (ended June 29, 2020, 12:30 p.m.)
    The morning session of the Proof Ground 2020 Competition.

  • Proof Ground 2020 - Afternoon
    (ended June 29, 2020, 3:30 p.m.)
    The afternoon session of the Proof Ground 2020 Competition.

  • Semantics 2020/2021 (Archived)
    (ended March 10, 2021, 3:01 p.m.)
    Homework exercises for the winter term 2020/21 edition of the "Semantics of Progamming Languages" course @TUM

  • FDS 2021
    (ended July 15, 2021, 11:59 p.m.)
    FDS Summer Semester 21

  • Proof Ground 2021 - Morning
    (ended June 28, 2021, 12:30 p.m.)
    The morning session of the Proof Ground 2021 Competition.

  • Proof Ground 2021 - Afternoon
    (ended June 28, 2021, 4 p.m.)
    The afternoon session of the Proof Ground 2021 Competition.

  • Semantics 2021/2022
    (ended Feb. 16, 2022, 8:12 a.m.)
    Homework exercises for the winter term 2021/22 edition of the "Semantics of Progamming Languages" course @TUM

  • FDS 2022
    (ended Oct. 24, 2022, 5 p.m.)
    FDS Summer Semester 22

  • Semantics 2022/2023
    (ended Feb. 13, 2023, 11:59 p.m.)
    Homework exercises for the winter term 2022/23 edition of the "Semantics of Progamming Languages" course @TUM

  • FDS 2023
    (ended July 21, 2023, 11:59 p.m.)
    FDS Summer Semester 23

  • Semantics 2023/2024
    (ended April 12, 2024, 1:29 p.m.)
    Homework exercises for the last edition of the "Semantics of Progamming Languages" course @TUM, winter term 2023/24.

  • FDS SS24
    (ended July 31, 2024, 11:59 p.m.)
    FDS summer semester 2024

  • FDS Exam 2024
    (ended July 24, 2024, 1:10 p.m.)
    FDS Exam contest.


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