El repositorio 'combinatorial-games', publicado por el usuario vihdzp en GitHub, ofrece una formalización en Lean 4 de temas centrales de la teoría de juegos combinatorios. Un juego combinatorio es, según define el propio proyecto, un juego entre dos jugadores —denominados Left y Right— que se turnan para modificar un estado del juego del que ambos tienen información perfecta; la partida termina siempre, y el jugador que se queda sin movimientos válidos pierde. No existen empates. Ejemplos clásicos dentro de esta categoría son el Nim, el Hackenbush y el Chomp, mientras que quedan fuera el póker (por incluir azar), el ajedrez (por poder terminar en tablas) o los juegos de Gale–Stewart, que no terminan.
El proyecto se organiza en torno a cuatro grandes líneas de formalización: la teoría general de juegos combinatorios (con conceptos como temperatura, posiciones dominadas o posiciones reversibles); la teoría de juegos específicos, entre ellos los juegos sobre conjuntos parcialmente ordenados, el Hackenbush o el tres en raya; la teoría de los nimbers, de los que se busca demostrar algebraicamente que forman un cuerpo cerrado; y la teoría de los números surrealistas, para la que se plantea dotarlos de estructura de cuerpo y probar su representación como series de Hahn.
La formalización se apoya de forma principal en la obra de Conway 'On numbers and games' (2001), complementada por otras referencias como la introducción de Schleicher y Stoll (2005) y el tratado de Siegel (2013). El repositorio se dirige a matemáticos, investigadores en verificación formal y estudiantes avanzados interesados en explorar la teoría de juegos combinatorios y los números surrealistas dentro del asistente de pruebas Lean 4.