This is a proof server. You can enjoy theorem proving here in several languages (one language).
The list of all problemsOpen problem page. There are some code fragments (Definitions, Theorem and Verify).
Some problem contains 'Definitions' part. In this case, save as 'Definitions.v' and compile it.
$ coqc Definitions.v
Next, save 'Theorem' as 'Theorem.v'. This part has theorems not proved yet. Complete proof.
Finally, if you have proved it, post your 'Theorem.v'.
First, feel free to create a new problem. Any problem is welcomed.
Download problem checker from here.
Create files named 'Definitions.v', 'Theorem.v' and 'Verify.v'. 'Definitions.v' is optional. Please consult the problems already posted.
Run checker program. If 'success' is displayed, you can post it. If your problem requires some axioms, edit the checker output and copy it to 'Assumption' field.