Discussion summary
Dungeon Proof Crawler is an RPG-inspired tool for learning proof writing, with mixed user experiences. Some praise its onboarding and mobile playability, while others find it confusing or incomplete.
What the discussion says
- Users appreciate the gradual onboarding and help menu.
- Some find the syntax and tutorial insufficient for beginners.
- There are technical issues like sphinxes not loading and error message concerns.
“Surprisingly interesting experience even for someone that does know nothing about writing proof.”
“It doesn't teach the basics needed to even solve the first puzzle.”
Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- 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).
by Vedor - Yeah, adding the tutorial before letting them battle monsters would only be fair.
- I spent some time this evening beating the dungeon. It took a bit of time to get my head around the syntax, but once I found the tutorial, it clicked.
The game reminds me quite a bit of The Little Prover and The Little Typer.
by nanolith - I updated the tutorial and the game; the most prominent update is that the editor now suggests fixes that solve copy/paste and mechanical editing. It makes the experience a lot better.
I also refactored the tutorial to be more introductory about the project.
by geckones - 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.
by wizzwizz4 - 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.
by marktani - 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.
by adamddev1 - The developer here! Thanks for all the feedbacks, here are some more info
There is a tutorial: https://dhilst.github.io/algae
The project (algae) is a algebraic specification tool. This means it is intended to allow you to write algebraic specs, in which you define your data types (sorts), operations (ops), and the the equations chatacterizing the operations (axioms). It is a formal specification technique. I designed because I want something to pratice/improve my proof theory skills, so, distinct from Lean4 or Roqc, all the proof information is visible in the surface syntax, but it still lack ergonomics.
About the tutorial and the game, I want it to be "proof theory introction"-like but the generated proofs are really not as good as I want they to be. The dificult progressions does not exist, the help sometimes does not help, some lemmas provide the proof in their arguments. To fix that I will need to go proof by proof and fix the help manually and also work on the progression. The AI is terrible at generating the proofs (yes it was made with AI help but I have formal specs experience).
About the game, it may still be buggy, feel free to open issues at https://github.com/dhilst/algae/issues, and I will fix it. I want to provide a cool playground for ppl to learn proof theory and for me to pratice it too.
by geckones