Turn the ICFP tutorial into a Lean game

[RaitoBezarius]

We can either self-host the game, implying some sysadmin, or we can reach out to the Lean community to add our own game.

Docs on how to create a game:

• https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md

[sonmarcho]

This looks super fun, that's a great idea 😆

[arademaker]

Can you point to the ICFP tutorial?

[sonmarcho]

Can you point to the ICFP tutorial?

I intend to create a repo with only the tutorial, and I'm still modifying it (see the last PR for instance), but you can find the tutorial here:

• the Rust code: https://github.com/AeneasVerif/aeneas/blob/main/tests/src/tutorial/src/lib.rs
• the Lean tutorial itself (Tutorial.lean is the result of the translation, Exercises.lean the exercises and Solutions.lean contains possible solutions with explanations): https://github.com/AeneasVerif/aeneas/tree/main/tests/lean/Tutorial

Note that this tutorial was designed to be presented at conferences: it should start with a live introduction, and the exercises are meant to be done while interacting with the speaker. We will of course shortly turn it into a more detailed tutorial that can be consulted online (and feeback is welcome, of course!).