## Proof Market

This was a proof market for the Coq proof assistant and Agda.

This site is closing on 2015-10-31. *We are trying to refund bounties to the unsolved problems. Contact i@yoichihirai.com .*

0 title | contact | created_at | bounty_address | solved | language -------------------------------------------+------------------+----------------------------+------------------------------------+--------+---------- hexagon equation | @maophilia | 2013-12-31 08:40:27.271869 | 1LvFUCehtTDoVZMZ7FqtYDgJcqG1gpYGV8 | f | Coq modus ponens with Axiom | @qnighy | 2013-12-28 15:23:51.895264 | 1Pzppmryn2Ra8sgXLyu3t7TTAfy9Dx9Qh3 | t | Coq mathcomp test | @pirapira | 2013-12-31 04:09:38.41717 | 1BjJpBwGZMwZswMcTXxToQiHbxrJENzepd | t | Coq left trace equals right trace | @maophilia | 2014-01-05 10:22:28.175956 | 1Pk4txc5YRKoJqZxpwGojX8Gx8k6qmhJ7f | f | Coq ssreflect test | @pirapira | 2013-12-31 03:37:53.468851 | 1DsHYiJC3cRe7S3H3hfavbYs68DNR1z52G | t | Coq modus ponens with Axiom (with new system) | @proofmarket | 2014-01-06 06:13:31.634811 | 148f1EUz1NwnnSSGV8JG6aCgwi2y3cpRx7 | t | Coq Regular Expression 2 | @qnighy | 2014-01-08 14:09:15.892133 | 17Cz7LJXndxBS8nWdBuPNNNg7w4XPAXMUs | f | Coq Make Contradiction | @qnighy | 2013-12-28 15:01:28.092478 | 1K73fjcDNdnAhWPKZuCqg8xEzWqrrB7SDG | t | Coq True | | 2014-01-06 23:50:10.004759 | 14ziqqZAJxS1EVxHqTFuEQ5UekLTaBnPes | t | Coq False, really | @pirapira | 2014-01-04 05:48:13.018896 | 1K5ENd34cVPDP3Fxp3U4rVHFQhTts4xEdh | t | Coq Addition tree compiler (corrected) | rotsor@gmail.com | 2014-02-11 21:19:45.209802 | 1DEfvCaaJz7KpWkbujDutEs3VWDmLoK4Qf | t | Agda One of Komori's problems | @pirapira | 2014-01-09 13:39:54.318142 | 12PWo48J7mYSJqCQBXW3oA6k9goGsEJ433 | f | Coq One of Komori's problems, revised | @pirapira | 2014-01-11 18:13:51.196602 | 15tmSq3CoNRrQhL3jonC2fRMoDn3cVi5im | f | Coq False | | 2014-04-26 21:20:43.610003 | 1NVMdWcXfzYVEp5KgspVV51sRDNAoASehJ | t | Agda CoInductive Plus 2 | @qnighy | 2013-12-31 02:52:05.162851 | 16f4wQV975KSU2Qe5SAvD4wjvQcWM3XGoD | t | Coq modus ponens in agda | @pirapira | 2014-01-13 21:38:06.456999 | 19db8MqmEPD3o4Yz1XhwVcDeTW4sPb21zz | t | Agda Tertium non datum. Negated. Twice. | @wojtekj | 2014-01-13 22:56:41.088673 | 1EbnhXaEThBQWkBFknfujSnbjYLEewb51C | t | Agda Termination of tak | | 2014-01-07 06:26:32.522701 | 1Dtn5eGimUPXVdXVo89TwPg1KKxbf5fgUm | t | Coq Takeuchi Function tak | | 2014-01-06 04:55:23.922154 | 1CXiRA89gGHiFV1WEhSphLFpwnEGDeeumE | t | Coq IffIffIff | @qnighy | 2013-12-31 04:30:08.484084 | 1NCYPrqsy1TsMS9fr6ohqw8ZfWMuHrkAHT | t | Coq Tertium non datum. Negated. Twice. Really. | | 2014-01-15 13:38:18.018994 | 17fuzJx5SJsJdApwmCVa8c48uM5PFvo5DQ | t | Agda Regular Expression 1 | @qnighy | 2014-01-08 14:09:06.515686 | 131aWRkNnek1oLRM4BQ6zY9qRUJrDs7uUW | t | Coq CoInductive Plus 1 | @qnighy | 2013-12-28 15:51:50.579581 | 1FTbG61CGKBfdQb3WLzPV2JYRkaXcAkgJF | t | Coq False | @pirapira | 2014-01-02 11:31:51.584454 | 1BkUZrkCARuu2LTmTbiRoTDFH83rzDGSDg | t | Coq Addition tree compiler | | 2014-02-11 12:48:31.086088 | 199qMZehKcLHMYoQj5ehiyRMGPyZbSoFVb | t | Agda Regular Expression 3 | @qnighy | 2014-01-08 14:09:19.660364 | 1KMhcwPhevHsKTjXRTd3KG1AiZAXSSj1R | t | Coq Lagrange's four-square theorem | | 2014-01-01 21:40:54.335038 | 1JL2YLssXjxXhYu1cjg3fRZGUS5ogBYpU7 | t | Coq Higman-Neuman theorem | | 2014-01-06 05:39:07.72327 | 15Ju12t52ZL1f8rA6vRTbk3SmzKngZ9c3L | t | Coq Untyped lambda calculus 1 | @pi8027 | 2014-03-24 02:42:27.116383 | 1QGjsuQwBCYBuPGa5urFfs8Cjs1Qp1Defe | t | Agda

### FAQ

- Is this site written in Coq?
- No, in Haskell, an inconsistent type theory. Although every type is inhabited, not all terms can be typed.
- Why has False been proved?
- First time, the meaning of False was changed. Second time, it was proved in Coq 8.4pl2, an older version.
- What Coq commands were used to check the answer?
- Some keyword screening (like Cd).
- coqc Definitions.v (if the problem contains definitions)
- coqc Answer.v
- coqc -require Definitions Verify.v (if the problem contains definitions. Otherwise, "-require Definitions " is omitted.)
- coqchk Answer -o -norec

- What Agda commands were used to check the answer?
- agda Definitions.agda (if the problem contains definitions)
- agda --safe Answer.agda
- agda Verifier.agda

- What Coq commands were used to check the problem?
- Some keyword screening (like Cd).
- coqc Definitions.v (if the problem contains definitions)
- coqc Answer.v (this comes from "Answer Template")
- coqc -require Definitions Verify.v (if the problem contains definitions. Otherwise, "-require Definitions " is omitted.)

- Whos runs this site?
- Yoichi Hirai
- About the bounty on False, it seems like you just threw away 0.999 BTC and no one will ever get them.
- Somebody got it.
- Are all solutions public?
- No. Some solutions are hidden until a price is paid. The price is specified when the solution is submitted. However, we require every submission to be licensed under Creative Commons Attribution 4.0 International License.
- How can I learn about Coq?
- I recommend reading and typing in Software Foundations

Contact: i@yoichihirai.com or
https://twitter.com/proofmarket

This site is based on
kik's Yesod-Anarchy-Proof-Server