From Rules to Nash Equilibria Lean 4 Case Study in Game-Theoretic Analysis of Competitive Trading Card Game

Jul 16, 2026

Upload by Sage

A metagame analysis for a competitive Pokémon Trading Card Game is machine-checked in Lean 4 using real tournament data. The work formalizes expected-value computations, type-to-matchup bridges, and machine-verified strategic dynamics including Nash equilibrium and replicator dynamics over 14 archetypes. It establishes a strict popularity paradox where the most-played deck underperforms equilibrium predictions while a less-played deck achieves higher expected win rate. A 10,000-iteration sensitivity study confirms qualitative stability of equilibrium support.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages13

Reading Time33 min

Introduction

Related Work

Lean Modeling and Rules Formalization

Probability and Resource Theory

Data and Measurement

Popularity Paradox

Equilibrium and Dynamics

Tournament Strategy

Formalization Methodology

Validity Threats

Conclusion

From Rules to Nash Equilibria: A Lean 4 Case Study in Game-Theoretic Analysis of a Competitive Trading Card Game Arthur F. Ramos and Tulio Soria arXiv :2607 .08692v 1 [ cs .GT] 9 Jul 2026 Abstract—We present a metagame analysis of the competitive Pokmon Trading Card Game, machine-checked in Lean 4 over real tournament data. The headline game-theoretic results (Nash equilibrium, replicator dynamics, and the matrix-level typebridge computation) rely on native_decide, which trusts Lean’s compiler rather than its kernel; the trust boundary is detailed in Section IX. 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 (January–February 2026, 50+ player events) over 14 archetypes and their full pairwise matchup matrix, we prove a popularity paradox: the most played deck (Dragapult, 15.5% share) has only 46.7% expected win rate, while Grimmsnarl (5.1% share) achieves 52.7% . A machine-checked Nash equilibrium of the raw game assigns Dragapult 0% weight; exhaustive enumeration over all 214 − 1 subsets confirms a unique symmetric Nash equilibrium of the constant-sum symmetrization (seven-deck support), against whose mix Dragapult falls 40.4 permil below the game value. This gap is strict, so in the symmetrization complementary slackness excludes Dragapult from every equilibrium—symmetric or asymmetric—and the raw-game equilibria concur, although“suboptimal” remains relative to a single-match payoff model that omits Swiss and consistency incentives. Single-step replicator dynamics on the full 14-deck game 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: core support decks appear in >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. Index Terms—Formal verification, game theory, trading card games, Nash equilibrium, theorem proving, metagame analysis, replicator dynamics, Lean 4 I. INTRODUCTION Tournament outcomes in competitive trading card games (TCGs) are often shaped before round one begins. The pretournament deck-selection problem is naturally modeled as a strategic game where payoffs derive from matchup win ratesand the population distribution of opponents. The Pokmon TCG is especially suitable for this analysis: it has a large A. F. Ramos is with Microsoft, Redmond, WA, USA (e-mail: arfre[ita@microsoft.com](ita@microsoft.com)) . T. Soria is an Independent Researcher (e-mail: [tulio.soria@gmail.com](tulio.soria@gmail.com)). This work has been submitted to the IEEE for possible publication. Copyright may be transferred without notice, after which this version may no longer be accessible. organized-play ecosystem, clearly defined public rules, and ametagame that evolves quickly enough to produce measurable strategic cycles, yet hidden information and stochastic effects make intuition unreliable even for experienced players. By encoding game semantics in Lean 4 [1] and proving strategic statements directly over exact data representations, we build a proof-carrying metagame analytics pipeline where the verified objects are (i) data representation and ingestion, (ii) expected-value computations over the field,(iii) machine-checked Nash-equilibrium computation and full 14-deck replicator dynamics, and (iv) tournament-objective transforms (Bo3, Swiss) . Figure 1 shows how an untrusted discovery layer and the trusted Lean verifier interact; Table I collects notation. Our empirical foundation is Trainer Hill metagame data [2],[3] for 50+ player tournaments from January 29 to February 19, 2026 . We model the top 14 archetypes and their full pairwise

FAQs

What problem does the paper address in competitive trading card games?

It analyzes how pre-tournament deck selection can be modeled as a strategic game where payoffs come from matchup win rates and the opponent population distribution.

How does the paper ensure the results are machine-checked?

It encodes game semantics in Lean 4 and verifies strategic statements directly over exact data representations, including Nash equilibrium computation and replicator dynamics.

What is the “popularity paradox” reported in the results?

The most played deck has a lower expected win rate than equilibrium-based expectations, while a less played deck achieves a higher expected win rate, yielding a strict gap confirmed by equilibrium analysis.

Jul 16, 2026

Upload by Sage