Lean Grimoire
Lean Grimoire (terrytao.wordpress.com)
要約
数学者テリー・タオ氏が、2018年に作成した命題論理と一階述語論理を学ぶためのインタラクティブな教科書「QED」を、最新のコーディングエージェントを用いて「Lean Grimoire」として再構築したことを報告しています。この新しいバージョンでは、ゲームの進行状況に応じたLean証明の表示や、数学的要素をファンタジー風のテキストで表現する「ファンタジーモード」などの新機能が追加されています。タオ氏は、論理証明やLeanの学習ツールとしての有用性を高めるためのプレイテストを求めています。
全文翻訳
Lean Grimoire
7月に、私は現代のコーディングエージェントを使用して、いくつかの数学的視覚化アプレットを構築する実験を開始しました。ここ数ヶ月の非常に多忙な出来事のため、これらのプロジェクトは一時棚上げせざるを得ませんでしたが、最近、当時始めたプロジェクトの1つ、つまり2018年に作成し、このブログで以前に発表した「QED」というタイトルのJavaScriptインタラクティブ教科書を近代化する作業に少し時間を割くことができました。その教科書の目的は、命題論理と一階述語論理を、与えられた仮説のセットから望ましい結論に到達するために様々な論理規則を適用する「クラフトゲーム」の形式で教えることでした。
コーディングエージェントを使用して、私はゲーム（「Lean Grimoire」という作業タイトルを付けました）を再構築し、いくつかの新機能を追加しました。例えば、ゲームの状態の進行中のLean証明を表示するオプションを提供しました。単に楽しむために、「ファンタジーモード」でプレイするオプションも追加しました。このモードでは、様々なゲーム要素がファンタジー風のフレーバーテキストで描かれます（例えば、数学的命題は「ポーション」になり、数式は「巻物」になるなど）。以下は典型的なスクリーンショットで、命題 ［画像: A hymeleaf B］ の証明がほぼ完了しています。
このアプレットを、論理証明や/またはLeanを教えるための手段としてより有用にするために、いくつかのプレイテストを行いたいと考えています。