Dungeon Proof Crawler: learn how to write proofs with RPG

【HN用户评论摘要】 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. 原始链接: https://dhilst.github.io/algae/game/index.html