Email Gateway (May 08 2026 at 17:54): Email Gateway (May 08 2026 at 17:54):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce another significant contribution by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz: Nash Equilibria for Finite Games in Isabelle/HOL
Abstract
This development formalizes Nash equilibria for finite strategic form games, following Nash’s equilibrium concept [5, 4]. It gives reusable definitions of profiles, unilateral deviations, best responses, dominant strategies, and pure Nash equilibria; proves existence for finite ordinal potential games [3] and games with dominant strategies; and verifies matching pennies as a finite game with no pure Nash equilibrium. It also formalizes mixed-strategy profiles for finite games, support lem mas for equilibrium strategies, Dirac embeddings of pure profiles, and the existence of a mixed Nash equilibrium using Brouwer’s fixed point theorem. Worked examples cover the Prisoner’s Dilemma, a coordina tion game, matching pennies, and rock-paper-scissors. AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle.
https://isa-afp.org/entries/Nash_Equilibrium.html
Last updated: May 23 2026 at 03:31 UTC