Summary of July 2019 Contest at Proving for Fun:

This repository contains a summary of the July 2019 Contest at "Proving for Fun".

Here, we summarize what happend from begin to end of the contest, announce the winners here, and collect and discuss solutions. Feel free to send us pull requests with your solutions and discuss them in the respective issues.

Chronology:

• 2019-07-05 17:13 - Contest starts with 4+1 Tasks and support for Isabelle and Coq
• After 3 hours - eberlm submits first overall solution for task Special Pythagorean Triple in Isabelle
• Shortly after - eberlm submits first overall solution for task Fun modulo 5 in Isabelle
• Shortly after - Azael solves Special Pythagorean Triple and Fun modulo 5 in Coq
• 5 hours into the contest - eberlm submits first correct solution for task A Funky Grammar in Isabelle
• 23 hours into the contest - eberlm submits the first correct solution for XOR in Isabelle, and thus has solved all 4 solvable tasks.
• Day 3 - jonathye submits the first Coq solution for XOR and later the same day the first Coq solution for A Funky Grammar, and thus is second to solve all solvable tasks
• Day 5 - the user named j has solved all four tasks in Coq
• Day 9 - tahasaf has solved all four tasks in Isabelle, as well as Nitrate did in Coq
• Day 13 - lasydler solved all 4 tasks in Coq
• Day 26 - s-quark and aleksey did all 4 tasks in Coq
• Day 26 - ACL2 and Lean enter the competition and alexjbest is the first to trick the system by solving break the system for Lean. Subsequently the loophole is closed, but the point is still valid to alexjbest and chrishughes24.
• Day 27 - The first correct Lean solutions start to come in: alexjbest is the first for Special Pythagorean Triple and chrishughes24 for Fun modulo 5
• Day 28 - monadius solved all 4 tasks in Coq and also submits a correct solution in Lean, being the first to submit solutions in two ITPs.
• After roughly a month - lasydler, jonathye and monadius use a known Coq bug to break the system. They thus overtake eberlm with now five solved tasks. Using a soundness bug is considered okay in that task, only in the first four tasks it is disqualified.
• 2019-08-09 midnight - contest ends

Winners and Awards:

jonathye wins the July Contest - congratulations! The contestant is followed by lasydler and monadius, all three solving all four solvable tasks in Coq and additionally breaking our system.

eberlm and tahasaf solve all four tasks with Isabelle and result in placements 4 and 6. The user j is 5th with solving problems with Coq.

The best Lean user were alexejbest shortly followed by chrishughes24 with 3 solved tasks: both solving two tasks with Lean and tricking our system.

In total we had 33 participants, 18 using Coq, 12 using Isabelle, 5 using Lean, and 1 using ACL2.

lasydler and monadius even used two different proof assistants! :)

Solutions and Discussions for the Tasks:

1. Special Pythagorean Triple

Task was stated by Maximilian P. L. Haslbeck in Isabelle, and translated to Coq by Armaël Guéneau, to Lean by Kevin Kappelmann and to ACL2 by Sebastiaan Joosten.

See issue #2 for that task, and take part in the discussion by commenting. Feel free to send us a pull request to add your solution to the repository.

2. Fun modulo 5

Task was stated by Maximilian P. L. Haslbeck in Isabelle, and translated to Coq by Armaël Guéneau, to Lean by Kevin Kappelmann and to ACL2 by Sebastiaan Joosten.

See issue #3 for that task, and take part in the discussion by commenting. Feel free to send us a pull request to add your solution to the repository.

3. XOR

Task was stated by Maximilian P. L. Haslbeck in Isabelle, and translated to Coq by Armaël Guéneau.

See issue #1 for that task, and take part in the discussion by commenting. Feel free to send us a pull request to add your solution to the repository.

4. A funky grammar

Task was stated by Simon Wimmer in Isabelle, and translated to Coq by Armaël Guéneau, and to ACL2 by Sebastiaan Joosten.

See issue #4 for that task, and take part in the discussion by commenting. Feel free to send us a pull request to add your solution to the repository.

5. Break the System

Task was stated by Maximilian P. L. Haslbeck in Isabelle, and translated to Coq by Armaël Guéneau, to Lean by Kevin Kappelmann and to ACL2 by Sebastiaan Joosten.

See issue #5 for that task, and take part in the discussion by commenting. Feel free to send us a pull request to add your solution to the repository.