Dungeon Proof Crawler: learn how to write proofs with RPG

I thought this was about writing proofs with RPG the programming language and I was intrigued.

To make it clear that it is with an RPG (role playing game) it needs an "an" in the title.

I sort of reverse engineered the first couple riddles (the help menu helped too) before really getting the logic here.

What I gathered:

- the paramaeters in lemma banish() are "given" - the statement right after lemma banish() is what we want to prove - all "wip" needs to replaced by something - blocks need to be finished with "qed;"

From there it's using the available tools.

Surprisingly interesting experience even for someone that does know nothing about writing proof - thanks to gradual onboarding and a decent help menu.

Also, perfectly playable at mobile (at least a couple of first monsters).

Such a great idea!

The first and southwest-most sphinxes of seed 0 never load, which soft-locks the game. (Fortunately it doesn't corrupt the save-file.)

Edit: after fighting enough other sphinxes, the first one loads, but the west-most fails with an explicit error message:

> This challenge failed to load. Retreating.

On the next floor, the sphinx over the exit stairs fails, preventing me from progressing.