# 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.

## News

- System
- 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