Formalizan la teoría de juegos combinatorios en Lean 4
Combinatorial Games in Lean
El repositorio combinatorial-games de vihdzp formaliza en Lean 4 la teoría de juegos combinatorios, incluyendo juegos generales, juegos específicos como Nim y Hackenbush, nimbers y números surreales. El proyecto, basado en Conway y otras referencias, busca demostrar propiedades como el cierre algebraico de los nimbers y la representación de los surreales como series de Hahn.
Un juego combinatorio es un juego de dos jugadores que termina y con información perfecta; en otras palabras, dos jugadores (llamados Left y Right) alternan cambios en un estado del juego, del cual siempre tienen pleno conocimiento.