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:

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.