Dungeon Proof Crawler: learn how to write proofs with RPG

https://dhilst.github.io/algae/game/index.html

by SchwKatze • 17 days ago

82 26 17 days ago

dhilst.github.io

Vedor• 17 days ago

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).

heftig• 17 days ago

I had the exact opposite experience. It doesn't teach the basics needed to even solve the first puzzle. Which language are we even writing in? Clicking help explains what exactly to do but not why, as well as lots of rules with unexplained terminology.

klibertp• 17 days ago

There's a chance it's this: https://github.com/dhilst/algae

wizzwizz42• 17 days ago

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.

geckones9• 17 days ago

I fixed some bugs regarding the stairs. Can you share your seed? I can play the same game and try to reproduce it. It shows up in the top-right corner

geckones9• 17 days ago

Oh you just said "seed 0" I will try it

adamddev1• 17 days ago

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.

mmooss• 17 days ago

"Every monster is a proof. Bring back the ring before sunrise."

SchwKatze• 17 days ago

Sorry, I didn't even know RPG is a language, it's too late to edit tho

marktani• 17 days ago

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.

slicendice• 17 days ago

Such a great idea!

geckones9• 17 days ago

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.

woolion• 17 days ago

To me, what makes a game a game is that you can learn how it works simply by interacting with it; you don't need to open a separate wiki. That is not entirely true, as for examples fighting games have been infamous for needing to go online to learn how combos work, but this is widely considered to be a major factor of why the genre is unpopular, and recent games have tried to at least give proper tools (in training mode). Right now, it feels a bit like a series of exercises with the guiding text replaced by dungeon fluff; it's pretty neat, yet you could as much say 'just give me the tutorial'.

In a game format I would for instance expect not to have to type the "proof [...] qed" part for example; its purpose is to be a bounding box, but interacting through text is cumbersome -- it isn't really for a developer who sees the benefit of plain text, but it is for a most users who might bang their head against the syntactic impedance mismatch.

To put that into perspective though, I remember Brett Victor's "Alligator Eggs", and the idea is very compelling; games are self-motivating, so if you can learn some real skills then you solved everything. Combinatory logic, sequent calculi etc naturally lend themselves pretty well to the puzzle formats, yet I don't think there's anyone who really succeeded at any real implementation of it.

I'm mostly rambling my own view on the subject here, it's certainly an interesting experiment :-)

geckones9• 17 days ago

Yeah the game was thought to be an extension of the tutorial and an educational/grinding environment for the theory and the language.

About interacting with text, in that case I think it is exactly the opposite. The purpose is to be a funny shell around a bunch of exercises that would fell tedious (for me, at last) without it. It is meant to be a roguelike dungeon crawler about proof theory, so yeah, it is expected the player to learn to write proofs.

To me there are still 2 big problems

1. The language ergonomics. This is what I want to work on next. 2. The progression of the game levels and the tutorial. The goal is that they introduce the tool (algae), introduce proof techniques (ex: to proof a conditional you assume the premise and prove the conclusion) with some progression, and provide a playground through the game

smj-edison• 17 days ago

Have you looked at Metamath Zero[1] before? You mentioned using sorts which is what reminded me of it. Just thought I'd point to some additional interesting work :)

[1] https://github.com/digama0/mm0

geckones9• 17 days ago

I didn't thanks for sharing

It looks a cool project, definetely related

bartleeanderson• 17 days ago

Yeah, adding the tutorial before letting them battle monsters would only be fair.

geckones9• 17 days ago

done!

shiandow• 17 days ago

Having to replace wip with qed when indentation makes it clear it's the only thing that fits is a bit tedious.

geckones9• 17 days ago

Yeah, I guess I can fix this easily by using qed instead of wip in the templates, but I have to check if the error messages will persist, I believe the qed error suppress the helpful messages now.

But this does not scale, there is a lot of copy and paste when the proofs require case analysis, I want to check if I can emit edit comands to the editor in a sane way to automate that copy and pasting.

wizzwizz42• 17 days ago

Wouldn't it be better to improve the proof language so that copy-pasting is not necessary? (I know that's very hard, though.)

pjmlp• 17 days ago

Me thinking this was about actual RPG, https://en.wikipedia.org/wiki/IBM_RPG

nanolith• 16 days ago

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.

geckones9• 15 days ago

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.

Dungeon Proof Crawler: learn how to write proofs with RPG

Related Stories