Impartial games and the Sprague-Grundy theroem

Stream: general

[Fox Thomson]

I have defined impartial games and nim and managed to prove the Sprague-Grundy theorem as part of @Kevin Buzzard 's Xena summer projects. The code is at https://github.com/foxthomson/impartial.
Let me know if you have any feedback/suggestions!

[Kevin Buzzard]

@Scott Morrison should this go in mathlib?

[Markus Himmel]

I'm not Scott, but I'd love to see this in mathlib, just because it will allow me to create some fun Codewars kata.

[Bryan Gin-ge Chen]

I agree, this would be nice to have in mathlib.

[Aaron Anderson]

It’s on a todo list on a mathlib docstring already...

[Aaron Anderson]

Also, should some or all of the set-theoretic game stuff be moved to a top-level game_theory directory?

[Aaron Anderson]

Nim seems like game theory, surreals feel like set theory, but they probably still belong together

[Jalex Stark]

a top level game_theory folder should be about the notions studied by economists and computer scientists. i'd advocate for combinatorial_game_theory

[Scott Morrison]

I'm not sure they are such separate subjects.

[Aaron Anderson]

I would think that we would put this in game_theory/combinatorial_game_theory, but we don’t have any other kind of game theory yet