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.
$\begingroup$
$\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$– wizzwizz4Feb 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$– CrabManFeb 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$– wizzwizz4Feb 13, 2022 at 22:52
-
$\begingroup$ @wizzwizz4 I've flagged the question asking the moderators to make it Community Wiki. $\endgroup$– CrabManFeb 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$– Kevin BuzzardFeb 13, 2022 at 23:00
Add a comment
|
4 Answers
$\begingroup$
$\endgroup$
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).
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
The incredible proof machine 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)
$\begingroup$
$\endgroup$
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:
