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.
- Agda version 2.3.2 (sci-mathematics/agda-2.3.2-r5)
- Agda Standard Library version 0.7 (sci-mathematics/agda-stdlib-0.7_pre20130109)
- Contact: n.ohkawa _at_ gmail.com ⊎ http://twitter.com/notogawa