From Rules to Nash Equilibria: A Lean 4 Case Study in Game-Theoretic Analysis of a Competitive Trading Card Game
2026-07-09 • Computer Science and Game Theory
Computer Science and Game TheoryFormal Languages and Automata Theory
AI summaryⓘ
The authors analyzed competitive Pokemon Trading Card Game data using a formal method called Lean 4 to mathematically verify strategies and outcomes. They studied how popular different decks were and found that the most common deck actually performed worse than some less-used decks. Their analysis used advanced game theory concepts like Nash equilibrium and replicator dynamics to show which decks gain or lose advantage over time. This work mainly demonstrates how rigorous computer-checked proofs can improve understanding of game strategy beyond traditional explanations.
Pokemon Trading Card GameLean 4Nash equilibriumreplicator dynamicsmetagamegame theorymachine-checked proofpopularity paradoxsymmetric equilibriumsensitivity analysis
Authors
Arthur F. Ramos, Tulio Soria
Abstract
We present a metagame analysis of the competitive Pokemon Trading Card Game, machine-checked in Lean 4 over real tournament data. The headline game-theoretic results, including Nash equilibrium, replicator dynamics, and the matrix-level type-bridge computation, rely on native_decide, which trusts Lean's compiler rather than its kernel; the trust boundary is made explicit. The artifact spans approximately 31,900 lines, 87 files, and 2,627 theorems, of which roughly 200 directly verify empirical claims, with no sorry, admit, or custom axioms. Analyzing Trainer Hill data from January to February 2026 for events with at least 50 players, over 14 archetypes and their full pairwise matchup matrix, we prove a popularity paradox: the most played deck, Dragapult, with 15.5% metagame share, has only 46.7% expected win rate, while Grimmsnarl, with 5.1% share, achieves 52.7%. A machine-checked Nash equilibrium of the raw game assigns Dragapult 0% weight; exhaustive enumeration over all nonempty support subsets confirms a unique symmetric Nash equilibrium of the constant-sum symmetrization with seven-deck support. Against this equilibrium mix, Dragapult falls 40.4 permil below the game value. Single-step replicator dynamics indicate downward fitness pressure on Dragapult, upward pressure on Grimmsnarl, and strongest extinction pressure on Alakazam. A 10,000-iteration sensitivity analysis confirms qualitative stability, with core support decks appearing in more than 96% of resampled equilibria. The primary contribution is methodological: a reproducible case study showing how formal verification can turn qualitative metagame narratives into machine-checkable, re-runnable strategic science.