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
Classification of Finite Simple Groups Formalized in Lean
A complete formalization of the Classification of Finite Simple Groups in Lean 4, with every logical step checked by Lean's kernel, spanning 43.1M lines of Lean and following the first-generation proof. Along the way, the team discovered an issue in a published argument for the Unbalanced Group Theorem and devised an alternative route.
Scaling Lean Theorem Proving for Real-World Code Verification
The paper presents EasyProver, a Lean proving system using recursive agents and asynchronous search that near-saturates PutnamBench and IMO benchmarks with an off-the-shelf frontier model, plus Aegis, a pipeline converting competitive programming into harder real-world Rust-to-Lean verification tasks for benchmarking and RL.
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.
Formalizing the Enormous Theorem (27 minute read)
Axiom Math released the first complete computer-checked proof of the Classification of Finite Simple Groups in Lean, using swarms of dozens of AI agents over 24 days to produce ~43.1 million lines of code, while also surfacing 34 deviations from the published record and a new result in group theory.