GitHub - vihdzp/combinatorial-games: Combinatorial game library in Lean 4 · GitHub
/" data-turbo-transient="true" />
Skip to content
Search or jump to...
Search code, repositories, users, issues, pull requests...
-->
Search
Clear
Search syntax tips
Provide feedback
--><br>We read every piece of feedback, and take your input very seriously.
Include my email address so I can be contacted
Cancel
Submit feedback
Saved searches
Use saved searches to filter your results more quickly
-->
Name
Query
To see all available qualifiers, see our documentation.
Cancel
Create saved search
Sign in
/;ref_cta:Sign up;ref_loc:header logged out"}"<br>Sign up
Appearance settings
Resetting focus
You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.
Dismiss alert
{{ message }}
vihdzp
combinatorial-games
Public
Notifications<br>You must be signed in to change notification settings
Fork<br>11
Star<br>62
master
BranchesTags
Go to file
CodeOpen more actions menu
Folders and files<br>NameNameLast commit message<br>Last commit date<br>Latest commit
History<br>363 Commits<br>363 Commits
.github/workflows
.github/workflows
.vscode
.vscode
CombinatorialGames
CombinatorialGames
docbuild
docbuild
scripts
scripts
.gitignore
.gitignore
CombinatorialGames.lean
CombinatorialGames.lean
LICENSE
LICENSE
README.md
README.md
lake-manifest.json
lake-manifest.json
lakefile.toml
lakefile.toml
lean-toolchain
lean-toolchain
View all files
Repository files navigation
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)
About
Combinatorial game library in Lean 4
vihdzp.github.io/combinatorial-games/
Resources
Readme
License
Apache-2.0 license
Uh oh!
There was an error while loading. Please reload this page.
Activity
Stars
62<br>stars
Watchers
watching
Forks
11<br>forks
Report repository
Releases
No releases published
Packages
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
Contributors
Uh oh!
There was an error while loading. Please reload this page.
Languages
Lean<br>100.0%
You can’t perform that action at this time.