Lean 4 proves Pokémon TCG's top deck is mathematically suboptimal

Arthur F. Ramos and Tulio Soria have published a groundbreaking paper that uses the Lean 4 proof assistant to formally verify a game-theoretic analysis of the competitive Pokémon Trading Card Game (TCG). The work, spanning 31,900 lines of code across 87 files and 2,627 theorems (with no sorry, admit, or custom axioms), represents the first machine-checked metagame study of a real trading card game. Using tournament data from Trainer Hill between January and February 2026—covering events with at least 50 players and 14 archetypes with full pairwise matchup matrices—the authors prove a striking popularity paradox.

The headline result: Dragapult, the most-played deck at 15.5% metagame share, has an expected win rate of just 46.7%, while Grimmsnarl, with only 5.1% share, wins 52.7% of its matches. 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 and upward pressure on Grimmsnarl, with 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: showing how formal verification can turn qualitative metagame narratives into machine-checkable, re‑runnable strategic science.