TY - JOUR AU - Bagnall, Alexander AU - Merten, Samuel AU - Stewart, Gordon PY - 2017/01/01 Y2 - 2024/03/29 TI - A Library for Algorithmic Game Theory in Ssreflect/Coq JF - Journal of Formalized Reasoning JA - JFR VL - 10 IS - 1 SE - Articles DO - 10.6092/issn.1972-5787/7235 UR - https://jfr.unibo.it/article/view/7235 SP - 67 - 95 AB - We report on the formalization in Ssreflect/Coq of a number of concepts and results from algorithmic game theory, including potential games, smooth games, solution concepts such as Pure and Mixed Nash Equilibria, Coarse Correlated Equilibria, epsilon-approximate equilibria, and behavioral models of games such as best-response dynamics. We apply the formalization to proveĀ  Price of Stability bounds for, and convergence under best-response dynamics of, the Atomic Routing game, which has applications in computer networking. Our second application proves that Affine Congestion games are (5/3, 1/3)-smooth, and therefore have Price of Anarchy 5/2. Our formalization is available online. ER -