An Existence Theorem of Nash Equilibrium in Coq and Isabelle
An Existence Theorem of Nash Equilibrium in Coq and Isabelle
Nash equilibrium (NE) is a central concept in game theory. Here we prove formally a published theorem on existence of an NE in two proof assistants, Coq and Isabelle: starting from a game with finitely many outcomes, one may derive a game by rewriting each of these outcomes with either …