Combinatorial Games in Lean
Summary
A formalization of combinatorial game theory in Lean 4, covering games, nimbers, and surreal numbers, based on Conway's work.
View Cached Full Text
Cached at: 07/15/26, 10:41 AM
vihdzp/combinatorial-games
Source: https://github.com/vihdzp/combinatorial-games
Combinatorial games in Lean
A formalization of topics within combinatorial game theory in Lean 4.
What is it?
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. Non-examples 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).
What’s in scope?
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 them algebraically closed, prove the simplest extension theorems)
- The theory of surreal numbers (set up their field structure, prove their representations as Hahn series)
References
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)
Similar Articles
All Lean Books and Where to Find Them
A curated list of Lean 4 books for learning the theorem prover, covering functional programming, metaprogramming, and logical verification, with opinions on each resource.
From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
This paper presents NSPI, a neuro-symbolic framework that combines LLMs and symbolic computation to prove polynomial inequalities. It uses LLM-generated sum-of-squares conjectures, refines them symbolically, and formally verifies the proofs in Lean, demonstrating scalability on polynomials with up to 10 variables.
@sophiamyang: Introducing Leanstral 1.5 A 119B (6B active) open model for formal proof engineering in Lean 4: 100% on miniF2F 587/672…
Introducing Leanstral 1.5, a 119B parameter (6B active) open model for formal proof engineering in Lean 4, achieving 100% on miniF2F, state-of-the-art scores on PutnamBench and FATE benchmarks, and discovering previously unknown bugs in open-source repositories.
Formalizing statistical learning theory in Lean 4 [R]
FormalSLT is a Lean 4 library that formally proves finite-sample statistical learning theory results (ERM, VC bounds, Rademacher bounds, PAC-Bayes, etc.) with explicit assumptions and zero sorry statements, providing a machine-checked foundation for ML theory.
Games Between Programs: The Ruliology of Competition
A systematic exploration of all possible strategies in a repeated two-player game using computational methods, analyzing cumulative payoffs and winning strategies through ruliology.