Dungeon Proof Crawler: Roguelike Proofs in Your Browser
🎮 Dungeon Proof Crawler
dhilst (Algae). Browser. Play it here · Tutorial · GitHub
I clicked in expecting a pixel dungeon and got a lemma. A demon stole your wedding ring on the eve of the wedding; Miriam wants it back before sunrise. You descend seven levels, and each sphinx or dragon guards an unfinished formal proof, not a health bar.
Combat is proof completion. Every room holds a monster and an Algae proof that ends in
wip, the marker for a goal you have not closed yet. Replace eachwipwith a real step, finish the block withqed, and press Cast Proof. The same WebAssembly kernel that powers the Algae playground re-checks every step locally. No errors and nothing left admitted means the monster falls.Difficulty tracks depth, not gear. Early floors ask for a single
refl. Near the bottom you are writing full proofs by induction. Beat monsters to raise your max health, open chests for food and lore, and keep moving: hunger drains while you stare at a stuck goal.The win condition is a story beat. Reach Level -6, recover the ring, and climb back out before sunrise. World generation, your run, and saved progress all stay in the browser. Nothing leaves the page.
It is a teaching toy with rough edges. The author says progression and help text still need manual work, and some challenges can fail to load. Fair warning if you hit a soft lock. The Algae tutorial is the real prerequisite; the crawler assumes you can already read a proof tree.
Play it if: you want a roguelike skin on proof practice, or you liked formal methods in school and miss them.
Skip it if: logic puzzles make you quit tabs, or you want combat that does not end in qed;. This is a proof editor wearing a dungeon coat.
Related TMFNK Content
- Chess in Pure SQL: Play Chess Against a Database Another browser oddity where the game is really a formal system pretending to be fun.
- Euclidea Construction puzzles with the same satisfaction of a step that either checks or does not.
- TinyWind: Pixel Pirate Sailing in Your Browser Different genre, same HN-era browser roguelite energy and honest alpha caveats.
Crepi il lupo! 🐺