Terence Taoがコーディングエージェントで論理学ゲーム「Lean Grimoire」を再構築
2018年に公開したJavaScript製の対話型教科書「QED」を、コーディングエージェントを使って刷新。命題論理と一階論理を「クラフトゲーム」形式で学ぶ内容で、進行中のLean証明を表示する機能を追加した。数学的命題を「ポーション」、数式を「スクロール」に見立てるファンタジーモードも搭載。論理証明やLeanの教材として役立てるため、プレイテストを募っている。
その教科書の目的は、与えられた仮説の集合からさまざまな論理規則を適用して望む結論に到達するという「クラフトゲーム」の形で、命題論理と一階論理を教えることでした。
HNでの議論
11- torben-friis
なんてひどい教育ゲームなんだ。
否定的で申し訳ないが、LLMっぽい導入文はほとんど解析できないし、あのコントロールはまるで未完成の個人的なObsidianドキュメントみたいだ。
Taoからするとちょっと変だな、彼の数学ノートはとても親しみやすくてよく書けていたのを覚えている。