RPGで学ぶ形式手法：ダンジョン探索しながら証明力を鍛えよう！

「Dungeon Proof Crawler」は、ダンジョン探索というRPGの要素を取り入れながら、形式証明（Formal Proofs）の書き方を楽しく学べる画期的な学習ツールです。難しい理論に挫折しがちな証明の世界を、ゲーム感覚で攻略してみませんか？

証明を書くことについて全くの素人でも驚くほど面白い体験だった。段階的なオンボーディングとしっかりしたヘルプメニューのおかげだね。あと、モバイルでも問題なく遊べるよ（少なくとも最初のモンスター数体は）。

シード0の最初と南西端のスフィンクスがロードされなくて、ゲームが進行不能になる（ソフトロック）。（幸いセーブデータは壊れないみたいだけど）

追記：他のスフィンクスを十分に倒してから戻ると最初のはロードできたけど、西端のは明確なエラーメッセージが出て失敗する。

This challenge failed to load. Retreating.

次の階層でも、出口の階段にあるスフィンクスが失敗して進めなくなっちゃう。

てっきりプログラミング言語のRPGを使って証明を書く話かと思って興味を惹かれたよ。RPG（ロールプレイングゲーム）であることをはっきりさせるには、タイトルに「an」を入れる必要があるんじゃないかな。

ここのロジックを理解する前に、最初のいくつかの謎解きを（ヘルプメニューも助けにして）なんとなくリバースエンジニアリングしてみた。

理解したことはこんな感じ：

• lemma banish() の引数は「与えられたもの（given）」
• lemma banish() の直後の文が証明したい内容
• 「wip」はすべて何かで置き換える必要がある
• ブロックは「qed;」で終わらせる必要がある

そこからは、使えるツールを駆使していく感じだね。

最高のアイデアだね！

開発者です！フィードバックありがとう。いくつか補足情報を載せておくね。

チュートリアルはこちら： https://dhilst.github.io/algae (https://dhilst.github.io/algae)

このプロジェクト（algae）は代数的仕様記述ツールなんだ。データ型（sorts）、操作（ops）、そして操作を特徴付ける等式（axioms）を定義して、代数的な仕様を記述するためのもの。形式手法の一種だよ。自分が証明理論のスキルを練習・向上させるために作ったものだから、Lean4やCoqとは違って証明情報がすべて表面の構文で見えるようになっているけど、まだ操作性はイマイチだね。

チュートリアルとゲームに関しては、「証明理論の入門」のような位置付けにしたいんだけど、生成される証明が期待しているほど良くないんだ。難易度の上昇もちゃんと機能していないし、ヘルプが役に立たないこともあれば、一部の補題（lemma）が引数の中に証明を出しちゃってたりする。これを直すには、一つずつ確認して手作業でヘルプを修正し、難易度設計も調整する必要があるね。AIは証明の生成に関してはひどい出来だよ（AIの助けを借りて作ったのは確かだけど、自分自身にも形式仕様の経験はあるからね）。

ゲームにバグがあったら、気軽に https://github.com/dhilst/algae/issues (https://github.com/dhilst/algae/issues) でIssueを上げてくれれば修正するよ。みんなが証明理論を学べて、自分も練習できるようなクールな遊び場にしたいと思ってる。