An Existence Theorem of Nash Equilibrium in Coq and Isabelle

Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus

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…