vihdzp/combinatorial-games

来源：https://github.com/vihdzp/combinatorial-games

Lean 中的组合博弈

在 Lean 4 中对组合博弈论主题的形式化。

这是什么？

组合博弈是一种双人终止型完全信息博弈。换句话说，两名玩家（称为 Left 和 Right）交替改变游戏状态，他们始终完全了解当前状态。游戏不能无限进行下去，无法移动的玩家即为输家。不存在平局。

组合博弈的例子包括 Nim (https://en.wikipedia.org/wiki/Nim)、Hackenbush (https://en.wikipedia.org/wiki/Hackenbush) 和 Chomp (https://en.wikipedia.org/wiki/Chomp)。非例子包括扑克 (https://en.wikipedia.org/wiki/Poker)（包含随机因素）、国际象棋 (https://en.wikipedia.org/wiki/Chess)（可能以平局结束），或 Borel 决定论中的 Gale–Stewart 博弈 (https://en.wikipedia.org/wiki/Borel_determinacy_theorem#Gale%E2%80%93Stewart_games)（可无限进行下去，详见此仓库 (https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean)）。

包含哪些内容？

本仓库大致旨在形式化以下四个方面的内容：

• 一般组合博弈理论 (https://github.com/users/vihdzp/projects/3)（温度、占优位置、可逆位置等）
• 特定组合博弈理论 (https://github.com/users/vihdzp/projects/7)（偏序集博弈、Hackenbush、井字棋等）
• 尼姆数理论 (https://github.com/users/vihdzp/projects/8)（证明其代数封闭性，证明最简扩张定理）
• 超现实数理论 (https://github.com/users/vihdzp/projects/9)（建立其域结构，证明其作为 Hahn 级数的表示）

参考文献

我们对组合博弈论的发展主要基于 Conway (2001)，并辅以其他各种现代资源。

• Conway, J. H. - On numbers and games (2001)
• Dierk Schleicher and Michael Stoll - An Introduction to Conway’s Games and Numbers (https://arxiv.org/abs/math/0410026) (2005)
• Siegel, A. N. - Combinatorial game theory (2013)