Comment by kevinbuzzard
6 years ago
First let me point out that you can jump to any level at any time, so you lose your progress, but only in a weak sense, if you lose your browser tab. You do lose your proofs though.
The natural number game was made by passing a repository which contains essentially nothing but Lean code, through this generic tool https://github.com/mpedramfar/Lean-game-maker which makes the html pages from the Lean code. If there is anyone out there who understands the Lean game maker code (I don't, it was written by my co-author) and is interested in implementing some kind of client side storage then feel free to ping me either at my Imperial email address or at the Lean Zulip chat https://leanprover.zulipchat.com .
Did you use a similar tool to make this mixed formal/informal presentation of the squeeze theorem? https://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html
I used Patrick Massot's Lean Formatter https://github.com/leanprover-community/format_lean to make the Lean web page with the analysis theorem on, and Mohammad Pedramfar's Lean game maker was very much inspired by the code in the formatter.