15
$\begingroup$

A game is a fun interactive tutorial/puzzle/challenge that provides the user with a DAG of definitions, theorem statements, examples, etc. and asks the user to prove all the theorems in this DAG. For instance, there is the natural numbers game in Lean. Games are fun because of high interactivity, quick feedback, low entry barrier, ease of use, and absence of long boring reading. In this question, let's compile all the games available for all the proof assistants. Note: if some tutorial is highly interactive, accessible, etc. but its author doesn't call it a game, it can still be included here.


Please use one answer per proof assistant. If you want to add a new game and there is already an answer for the proof assistant used in it, please edit the corresponding question.
$\endgroup$
5
  • $\begingroup$ This seems too broad… you really want all the games available for all the proof assistants? I suppose it could work if there was one answer per assistant, but people tend to post duplicate answers to these sorts of questions and it gets really messy to find anything. $\endgroup$
    – wizzwizz4
    Feb 13, 2022 at 22:45
  • 2
    $\begingroup$ @wizzwizz4 I assumed that there exist at most 20 games. Also, can I somehow make it so that there are wiki-answers - one per assistant? $\endgroup$
    – CrabMan
    Feb 13, 2022 at 22:46
  • $\begingroup$ There might not be many games now, but there will be hundreds at least by the time the site reaches 10000 questions. Making the question Community Wiki will make answers Community Wiki, though I believe only moderators can do that these days. (You could flag the question.) $\endgroup$
    – wizzwizz4
    Feb 13, 2022 at 22:52
  • $\begingroup$ @wizzwizz4 I've flagged the question asking the moderators to make it Community Wiki. $\endgroup$
    – CrabMan
    Feb 13, 2022 at 22:54
  • $\begingroup$ Following wizzwizz4 I've written two answers "per proof assistant" and hopefully people will edit them rather than adding their own $\endgroup$ Feb 13, 2022 at 23:00

4 Answers 4

14
$\begingroup$

Cubical Agda suggestions

The HoTT game

The HoTT Game was written by some Imperial undergraduates; the goal is to prove that the fundamental group of the circle is the integers, in cubical Agda. You can play online without installing Agda at Agdapad (instructions here).

$\endgroup$
14
$\begingroup$

Lean suggestions

The max minigame

Short online game here. Something I knocked off with a couple of collaborators when we were trying to work out how to make a real number game. We still haven't got to the bottom of this.

Lean maze game

The Lean maze game. Me trying to work out how you can write bespoke tactics to do more than prove theorems. A short experiment.

The complex number game

The complex number game. You have to install Lean to play this one; It's an introduction to how to define the complex numbers from first principles in Lean (assuming anything you like about the real numbers) and prove they're a field.

$\endgroup$
11
$\begingroup$

The incredible proof machine is a game with a collection of theorems for classical propositional logic, classical first-order logic, and the simply typed lambda calculus.


Example (think Visio)

enter image description here

$\endgroup$
3
$\begingroup$

Coq suggestions

Çoqoban

A sokoban where your solution is a proof. You can play it in your browser thanks to the awesome work of Shachar Itzhaky (one of the jsCoq maintainers): https://coq-next.vercel.app/fun/coqoban.html

Screenshot:

Coqoban goal shown in jsCoq

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.