Nash equilibrium in finite games (Using Brouwer fixed point)

Stream: general

[Kim Morrison]

(Your URL in the announcement gives a 404; is the repo private?)

[Kim Morrison]

Discussion thread for #announce > Nash equilibrium in finite games (Using Brouwer fixed point)

[Chris Henson]

I think there's a typo in the link, as removing the "1" works

[Violeta Hernández]

I recall that a few months ago there was some discussion about a Lean repository for games (not the combinatorial ones!). Did that ever come to fruition? Would this result have a home there?

[Anthony Wang]

Cool project! I saw that the code proves the existence of a Nash equilibrium, but does it also prove that the number of Nash equilibria in "almost all" games is odd? If not, how much work would it take to prove that using the code that you already have?

[Lyu Yuwei]

@Anthony Wang
Scarf's Combinatorial Theorem states that there is at least one colorful room, and the number of such rooms is odd. So I think it can be prove but I'm not sure how much work would it take....
If you are interested in this project, you are very welcome to discuss with us or join us. The Nash equilibrium formalization is just one part of our plan, and we hope to do more work in this direction.

[Haocheng Wang]

@Violeta Hernández If you're referring to Combinatorial game theory, that's not our project. But I did start a discussion thread here

The Nash equilibrium formalization is indeed a key part of our overall game theory plan. Moving forward, we're planning to work on more game theory content, possibly complete more structural formalization content by autoformalization.
image.png

[GasStationManager]

Anthony Wang said:

Cool project! I saw that the code proves the existence of a Nash equilibrium, but does it also prove that the number of Nash equilibria in "almost all" games is odd? If not, how much work would it take to prove that using the code that you already have?

This would require a definition of what you mean by "almost all", ie. nondegeneracy in games. I think a starting point is to find a paper that did this (and then proved the # of Nash equilibrium is odd).

[GasStationManager]

Also wanted to say very impressive work! Both the Nash existence and Brouwer.