Formalizing Combinatorial Game Theory in Lean 4

Combinatorial Games in Lean

I am building a comprehensive library in Lean 4 to formalize combinatorial game theory, covering general concepts like temperature and specific games such as Nim and Hackenbush. This project also aims to rigorously prove properties of nimbers and surreal numbers, ensuring mathematical certainty through code.

"A combinatorial game is two-player terminating game with perfect information where whoever is left without a move to make loses."