Lean 4 中组合博弈论的完整形式化

Combinatorial Games in Lean

这是一个在 Lean 4 中形式化组合博弈论的项目，涵盖了从一般理论到具体游戏（如 Nim、Hackenbush）的广泛内容。项目旨在通过形式化方法，深入探讨组合博弈的核心概念，包括温度、支配位置、可逆位置等，并致力于证明 nimbers 的代数封闭性以及 surreal numbers 的域结构。该项目基于 Conway 的经典著作，并结合了现代资源，为数学和计算机科学领域的研究者提供了一个强大的工具。

"组合博弈是一种两人终止且信息完美的游戏，两名玩家（称为 Left 和 Right）轮流改变游戏状态，且始终拥有完全的信息。"