Leanにおける組み合わせゲーム

Leanにおける組み合わせゲーム Lean 4での組み合わせゲーム理論のトピックの形式化。 これは何ですか？ 組み合わせゲームとは、2人のプレイヤーが交互に状態を変更し、完全情報、有限性、引き分けなしという特徴を持つゲームです。プレイヤーは、常に完全な知識を持っているゲームの状態を交互に変更します。ゲームは永遠に続くことはなく、次に打つ手がなくなったプレイヤーが負けとなります。引き分けはありません。組み合わせゲームの例としては、Nim、Hackenbush、Chompなどが挙げられます。ポーカー（チャンス要素がある）、チェス（引き分けで終わる可能性がある）、またはボレル決定性内のGale–Stewartゲーム（永遠に続く）は例外です（ただし、それらに関する詳細はこのリポジトリを参照してください）。 スコープは何ですか？ このリポジトリは、大きく分けて4つのことを形式化することを目指しています。 一般的な組み合わせゲームの理論（温度、支配された位置、可逆な位置など） 特定の組み合わせゲームの理論（Posetゲーム、Hackenbush、tic-tac-toeなど） ニムバーの理論（代数的に閉じていることの証明、最も単純な拡張定理の証明） シュルレアル数の理論（体の構造の設定、Hahn seriesとしての表現の証明） 参考文献 組み合わせゲーム理論の開発は、主にConway (2001)に基づいており、さまざまなより現代的なリソースで補完されています。 Conway, J. H. - On numbers and games (2001) Dierk Schleicher and Michael Stoll - An Introduction to Conway's Games and Numbers (2005) Siegel, A. N. - Combinatorial game theory (2013)