Agda Challenge

This is a proof server. You can enjoy theorem proving here in Agda.

How to submit proofs.

Open problem page. There are some code fragments (Definitions, Theorem and Verifier).

Some problem contains 'Definitions' part. In this case, save as 'Definitions.agda'.

$ agda Definitions.agda

Next, save 'Theorem' as 'Theorem.agda'. This part has postulated theorems. Complete proof.

$ agda --safe Theorem.agda

Finally, if you have proved it, post your 'Theorem.agda'.

How to create a new problem

First, feel free to create a new problem. Any problem is welcomed.

Create files named 'Definitions.agda', 'Theorem.agda' and 'Verifier.agda'. 'Definitions.agda' is optional. Please consult the problems already posted.