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?
  1. Some keyword screening (like Cd).
  2. coqc Definitions.v (if the problem contains definitions)
  3. coqc Answer.v
  4. coqc -require Definitions Verify.v (if the problem contains definitions. Otherwise, "-require Definitions " is omitted.)
  5. coqchk Answer -o -norec
What Agda commands were used to check the answer?
  1. agda Definitions.agda (if the problem contains definitions)
  2. agda --safe Answer.agda
  3. agda Verifier.agda
What Coq commands were used to check the problem?
  1. Some keyword screening (like Cd).
  2. coqc Definitions.v (if the problem contains definitions)
  3. coqc Answer.v (this comes from "Answer Template")
  4. 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