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.
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).
Most problems that you will find here follow an overall structure. They contain:
Here is an illustrative example for Isabelle:
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
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.
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.