A formalization of topics within combinatorial game theory in Lean 4.
A combinatorial game is two-player terminating game with perfect information. In other words, two players (called Left and Right) alternate changing some game state, which they always have full knowledge of. The game cannot go on forever, and whoever is left without a move to make loses. There are no draws.
Examples of combinatorial games include Nim, Hackenbush, and Chomp. Counterexamples include poker, which has chance elements, Chess, which can end in a tie, or the Gale–Stewart games within Borel determinacy, which go on forever (see however this repo for more info on them).
There are broadly four things this repository aims to formalize:
- The theory of general combinatorial games (temperature, dominated positions, reversible positions, etc.)
- The theory of specific combinatorial games (poset games, Hackenbush, tic-tac-toe, etc.)
- The theory of nimbers (prove their algebraic completeness, prove the simplicity theorems)
- The theory of surreal numbers (set up their field structure, prove their representations as Hahn series)
Our development of combinatorial game theory is based largely on Conway (2001), supplemented by various other more modern resources.
- 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)