Currently a tiny fraction of what is formalizable is of interest to mathematics; maybe humans will stop doing "serious" mathematics, but mathematics is beautiful and we will not stop playing with math, like we did not stop playing chess.
I would love to see a theory in the spirit of Guerino Mazzola work, but for (combinatorial) games.