콤비네토리얼 게임 이론을 Lean 4로 완전히 형식화한 라이브러리
Combinatorial Games in Lean
vihdzp/combinatorial-games는 콤비네토리얼 게임 이론을 Lean 4로 형식화하는 오픈소스 프로젝트입니다. Nim, Hackenbush, Chomp 같은 게임을 포함해 일반 게임 이론(온도, 지배 위치 등), 특정 게임, nimber, 초현실수(surreal numbers)까지 다룹니다. Conway의 'On Numbers and Games'를 기반으로 하며, 현재 363개 커밋과 10명의 기여자가 참여 중입니다.
콤비네토리얼 게임은 두 명의 플레이어(Left와 Right)가 번갈아 게임 상태를 바꾸는, 완전 정보를 가진 유한한 2인용 게임입니다.