Pith. sign in

REVIEW 3 major objections 7 minor 44 references

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

T0 review · 3 major / 7 minor · reviewed 2026-07-10 · glm-5.2

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Most-played Pokémon deck excluded from every Nash equilibrium

desk verdict Private letter to colleague on arXiv:2607.08692 read the letter →

arxiv 2607.08692 v1 pith:7S7MHVD5 submitted 2026-07-09 cs.GT cs.FL

Arthur F. Ramos , Tulio Soria This is my paper · ORCID
classification cs.GTcs.FL
keywords dragapultequilibriumgamenashanalysisleanmetagamepressure
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that formal verification—specifically Lean 4 theorem proving over exact rational arithmetic—can be applied to competitive game metagame analysis, turning qualitative strategic narratives into machine-checkable theorems. The demonstration uses real Pokémon Trading Card Game tournament data from January–February 2026 across 14 archetypes and their full pairwise matchup matrix. The central empirical finding is a popularity paradox: the most-played deck (Dragapult, 15.5% metagame share) has only a 46.7% expected win rate, while a less popular deck (Grimmsnarl, 5.1% share) achieves 52.7%. The central game-theoretic finding is that Dragapult receives 0% weight in both the raw-game Nash equilibrium and the unique symmetric Nash equilibrium of the constant-sum symmetrization, verified by exhaustive enumeration over all 2^14 − 1 nonempty support subsets. Because Dragapult's payoff against the equilibrium mix falls 40.4 permil strictly below the game value of 500, complementary slackness in the constant-sum symmetrization excludes it from every Nash equilibrium—symmetric or asymmetric. This exclusion tolerates perturbations up to approximately 20 permil, several times the Wilson sampling error of 1.8–9 permil. Single-step replicator dynamics confirm downward fitness pressure on Dragapult and upward pressure on Grimmsnarl. The authors position the specific results as illustrative; the primary contribution is methodological, showing that a proof assistant can serve as a practical scientific instrument for competitive game ecosystems, with the pipeline portable to any domain with discrete strategies and measurable outcomes.

What carries the argument

The pipeline encodes tournament matchup data as exact rational constants in Lean 4, then verifies game-theoretic claims (Nash equilibrium best-response conditions for all 14 strategies simultaneously, replicator dynamics, type-effectiveness bridges) via native_decide, which compiles decidability witnesses to native code and trusts Lean's compiler rather than its kernel. The trust boundary is made explicit: 145 of 2,627 theorems use native_decide; the remaining 2,482 close via kernel-checked tactics. Complementary slackness in the constant-sum symmetrization converts a strict best-response gap into universal equilibrium exclusion, and exhaustive enumeration over all 2^14 − 1 support subsets确认

What would settle it

If a future tournament window shows Dragapult's expected win rate rising above 50% without a change in the matchup matrix, or if a Swiss-utility equilibrium analysis assigns positive weight to Dragapult, the 'suboptimal' label would need qualification.

Watch

Extended reading notes

Core claim

The central mechanism is a verification pipeline in which tournament matchup data enters Lean 4 as exact rational constants, and game-theoretic claims become typed propositions that the machine rejects if any underlying number is mis-entered. The load-bearing logical step is the application of complementary slackness in a constant-sum game: if a strategy earns strictly less than the game value against an optimal opponent strategy, it cannot appear in the support of any Nash equilibrium. Dragapult's strict 40.4 permil deficit against the verified equilibrium mix thus converts a single best-response check into a universal exclusion claim. The pipeline also bridges type-effectiveness rules to实证

Load-bearing premise

The payoff model treats each deck as a point strategy optimizing expected single-match win rate, explicitly omitting Swiss-tournament consistency incentives. A deck with lower expected win rate but lower variance could be rational under a real tournament's cut-line probability objective, which the authors acknowledge but do not model.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 7 minor

Summary. This paper presents a metagame analysis of the competitive Pokémon Trading Card Game, formalized and machine-checked in Lean 4. Using Trainer Hill tournament data (January–February 2026, 50+ player events), the authors model 14 archetypes and their full pairwise matchup matrix. They prove a 'popularity paradox': the most popular deck (Dragapult, 15.5% share) has only 46.7% expected win rate, while Grimmsnarl (5.1% share) achieves 52.7%. They verify a Nash equilibrium of the raw 14×14 game assigning Dragapult 0% weight, and exhaustively enumerate all 2^14−1 support subsets to confirm a unique symmetric Nash equilibrium of the constant-sum symmetrization (seven-deck support), against which Dragapult has a strict 40.4 permil best-response gap. By complementary slackness, this strict gap excludes Dragapult from every equilibrium of the symmetrization. Single-step replicator dynamics show downward pressure on Dragapult and upward pressure on Grimmsnarl. A 10,000-iteration sensitivity analysis confirms qualitative stability of the core support. The artifact comprises ~31,900 lines, 87 files, and 2,627 theorems with no sorry, admit, or custom axioms.

Significance. The paper's primary contribution is methodological: it demonstrates that formal verification can turn qualitative metagame narratives into machine-checkable strategic science. The strengths are concrete. The artifact ships reproducible, machine-checked proofs over exact rational arithmetic (no floating-point error), with an explicitly documented trust boundary (145 of 2,627 theorems use native_decide; the remaining 2,482 are kernel-checked). The untrusted Python discovery layer is cleanly separated from the Lean certification layer, and the Nash equilibrium is discovered by an external LP solver but independently certified by Lean's best-response checks. The replicator dynamics yield falsifiable directional predictions, two of three of which were confirmed against out-of-sample data (Section VII-B). The sensitivity analysis (10,000 resampled equilibria, Wilson intervals) provides empirical robustness on top of the formal guarantees. The framework is parameterized over an abstract FiniteGame, making the game-theoretic harness reusable across domains. These are genuine advances in the application of formal methods to empirical game theory.

major comments (3)
  1. Section VII, paragraph beginning 'For the raw game M': The paper states that 'the same slackness logic applies up to the constant-sum deviation' for the raw game M, but the magnitude of this deviation is never quantified. The reader is told that M_ij + M_ji ≠ 1000 for many pairs and that deviations 'arise from the tie convention,' but no bound on max_{i,j} |M_ij + M_ji - 1000| is reported. Since the strict gap for Dragapult is 40.4 permil, knowing whether the constant-sum deviation is, say, 2 permil or 20 permil would materially affect the reader's assessment of how well the symmetrization results transfer to the raw game. The paper falls back to direct verification of one computed NE and a 77.9% bootstrap exclusion rate for M, which is honest, but reporting the deviation bound would strengthen the bridge between the two games and is a straightforward computation from the already-encoded
  2. Section VII-B (Preliminary Directional Check): One of three replicator predictions was disconfirmed (Grimmsnarl declined despite being predicted to grow), and the paper attributes this to a multi-step cascade (Mega Absol rises, then preys on Grimmsnarl). This is a reasonable explanation, but it highlights that the single-step replicator analysis has limited predictive power even one day out. The paper frames replicator outputs as 'directional diagnostics' rather than predictions, which is appropriate, but the abstract's claim that replicator dynamics 'indicate downward fitness pressure on Dragapult, upward pressure on Grimmsnarl' could be read as a stronger predictive statement than the out-of-sample evidence supports. Consider qualifying the abstract to match the more cautious framing in Section VII-A ('population-level directional diagnostics, not predictions about any individual's
  3. Section VII, uniqueness argument: The paper claims uniqueness of the symmetric Nash equilibrium via non-degeneracy (exactly seven best responses matching the seven-deck support). The non-degeneracy theorem for constant-sum games is cited as [36, Nisan et al.], but the specific theorem invoked is not named or stated. Since this is a load-bearing step in the uniqueness claim, a brief statement of the theorem and why its hypotheses are satisfied (beyond the support-size match) would improve rigor. The exhaustive enumeration over all 2^14−1 subsets independently confirms uniqueness, which mitigates this concern, but the theoretical argument should be stated precisely.
minor comments (7)
  1. Table III caption says 'TOP-6 SUBSET' but the table header lists six columns while the rows show only six archetypes, which is correct but the caption could clarify that both rows and columns are the same six archetypes.
  2. Section III-C, Listing 4: The theorem name 'grimmsnarl_dark_beats_all_psychic' uses the identifier 'GrimssnarlFroslass' (with double-s), which the paper notes in footnote 2 is a 'typographic inconsistency.' While the paper explains this is cosmetic, it would aid readability to mention the correct spelling in the code listing comment or use a consistent spelling.
  3. Section V-A: The paper states the top-14 aggregate is 69.5% of the full field but does not report how many total archetypes exist in the dataset or how the 14th vs. 15th cutoff was determined. A brief note on the cutoff rationale would help readers assess selection bias.
  4. Figure 2: The tier labels (S, A, B, C) are defined in Table V but not in the figure caption. Adding the tier definitions to the caption would make the figure self-contained.
  5. Section VIII: The Bo3 amplification formula P_Bo3 = 3p² - 2p³ is stated without derivation. A one-line derivation or reference would help readers unfamiliar with the binomial calculation.
  6. Section IX-A: The paper notes that replacing native_decide with kernel-checked decide is 'a tractable but costly future engineering task.' It would be useful to note whether the Mathlib community is actively working on kernel-efficient reduction for Fin.foldl, as this affects the replicability of the approach for future practitioners.
  7. Table II: The 'Point Est.' column for Gholdengo Lunatone shows '—' (zero weight in point estimate) but the 95% range extends to 34.5%. This is correct but could benefit from a footnote explaining that a deck with zero point-estimate weight can still appear in resampled equilibria.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: all claims verified against external data with independent certification

full rationale

The paper's derivation chain is self-contained and non-circular. The central claims are verified against external tournament data from Trainer Hill (an independent third-party platform), the type-effectiveness rules are grounded in official Pokémon Company rule documents, and the Nash equilibrium is discovered by an untrusted Python LP solver then independently certified by Lean's best-response checks. No claim reduces to a fitted parameter renamed as a prediction, and no self-citation chain is load-bearing. The expected win rate computation E[WR_i] = sum_j s_j * w_{i,j} is a standard weighted average over the empirical matchup matrix, not a definition that circularly produces its output. The Nash equilibrium verification checks best-response conditions for all 14 strategies against the candidate mix—this is a genuine certification, not a tautology. The replicator dynamics compute fitness from the same matrix, but the directional predictions (Dragapult declining, Grimmsnarl growing) are substantive consequences of the matrix structure, not definitions. The complementary-slackness argument for universal Dragapult exclusion in the symmetrization is a standard game-theoretic theorem applied to machine-checked constants, not a self-cited result. The skeptic's concern about the raw game M being only approximately constant-sum is a correctness/coverage issue (the universal exclusion is formally proven only for the symmetrization S, while for M it rests on a single verified equilibrium plus 77.9% bootstrap), not a circularity issue—no step reduces to its own inputs by construction.

Assumptions & free parameters 3 free parameters · 7 assumptions · 0 invented entities

No new mathematical objects, particles, forces, or dimensions are postulated. The framework uses standard game theory (Nash equilibrium, replicator dynamics, constant-sum games) applied to empirical data. The free parameters are modeling choices (tie weight, archetype cutoff, event threshold) rather than fitted constants, and the authors provide robustness checks for each. The most consequential axiom is the single-match payoff model, which defines 'suboptimal' in a narrow sense.

free parameters (3)
  • Tie weight coefficient (T/3) = 1/3
    Chosen to mirror the Pokémon Championship Series match-point system (3 for win, 1 for tie, 0 for loss). Not fitted to data but a domain modeling choice. Authors show results are algebraically independent of this choice in the symmetrization.
  • Top-14 archetype cutoff = 14 decks (69.5% of field)
    Chosen to capture the dominant archetypes while maintaining statistical power. Worst-case bounds (Section X) show Dragapult needs 57.6% WR vs unmodeled decks to reach 50%, so the cutoff does not drive the paradox.
  • 50+ player event threshold = 50 players
    Data selection criterion for tournament inclusion. Standard threshold for competitive relevance but introduces potential selection bias acknowledged in Section X.
assumptions (7)
  • standard math Nash's theorem (existence of Nash equilibria in finite games)
    Invoked in Section VII to guarantee existence of equilibria. Standard result from game theory (Nash 1950, ref 37).
  • standard math von Neumann minimax theorem
    Invoked in Section VII for the zero-sum special case. Standard result (ref 38).
  • standard math Complementary slackness in constant-sum games
    Used in Section VII to prove Dragapult's exclusion from all equilibria. Standard LP duality result.
  • domain assumption native_decide correctness
    145 theorems trust Lean's compiler code generation rather than the kernel. Section IX-A explicitly documents this trust boundary. No such bugs reported in practice.
  • domain assumption Trainer Hill data accuracy
    The matchup matrix is sourced from a third-party platform. Section V-C states: 'the pipeline transforms data faithfully, but does not vouch for the data's ultimate accuracy.'
  • domain assumption Archetype type assignments (attack/defense types)
    Section III-C: assignments are 'domain-expert modeling choices' not formally derived from card data. Headline result is invariant to borderline classifications.
  • ad hoc to paper Single-match payoff model represents strategic optimality
    Section VIII: the model omits Swiss-system consistency incentives. 'Suboptimal' is defined relative to this single-match benchmark, not actual tournament utility.

how reviews work

0 comments
Cite this review

Pith. "Pith review of From Rules to Nash Equilibria: A Lean 4 Case Study in Game-Theoretic Analysis of a Competitive Trading Card Game." pith.science (2026). https://pith.science/paper/7S7MHVD5

@misc{pith2026260708692,
  author       = {Pith},
  title        = {Pith review of: From Rules to Nash Equilibria: A Lean 4 Case Study in Game-Theoretic Analysis of a Competitive Trading Card Game},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7S7MHVD5}},
  note         = {Machine review of arXiv:2607.08692}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2607.08692 by the authors.

Figure 1
Figure 1. Verification pipeline. A Python layer (untrusted) only proposes candi￾date equilibria and resampled matrices; Lean certifies every claim at compile time via native_decide over exact rationals, and a separate runtime stage executes demonstration traces. Data enter once as exact constants, so the discovery tool can never inject an unverified number. (“does mix x beat every pure response?”) the tactics decide and nativ… view at source ↗
Figure 2
Figure 2. Popularity paradox: share versus expected win rate (top-14 nor [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Directed metagame interaction motif. decks appear. Dragapult’s exclusion, by contrast, tolerates perturbations up to ≈20‰ (Section X), a four-fold larger margin. Point-estimate support membership and perturbation￾stable exclusion are distinct claims, and our headline conclu￾sion rests only on the latter. A. Replicator Dynamics Replicator dynamics formalize directional pressure [41], [42]: x˙ i = xi(fi(x) − ¯f(x)). O… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages

  1. [1]

    The Lean 4 theorem prover and program- ming language,

    L. de Moura and S. Ullrich, “The Lean 4 theorem prover and program- ming language,” inAutomated Deduction – CADE-28, ser. LNCS, vol. 12699. Springer, 2021, pp. 625–635

    work page 2021

  2. [2]

    Pok ´emon tcg tournament metagame aggregates,

    Trainer Hill, “Pok ´emon tcg tournament metagame aggregates,” https: //www.trainerhill.com, 2026, aggregates Limitless TCG tournament re- sults; accessed: 2026-02-20

    work page 2026

  3. [3]

    Limitless tcg tournament platform,

    Limitless TCG, “Limitless tcg tournament platform,” https://limitlesstcg. com, 2024, accessed: 2026-02-20

    work page 2024

  4. [4]

    Programming a computer for playing chess,

    C. E. Shannon, “Programming a computer for playing chess,”The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science, vol. 41, no. 314, pp. 256–275, 1950

    work page 1950

  5. [5]

    On the complexity of some two-person perfect- information games,

    T. J. Schaefer, “On the complexity of some two-person perfect- information games,” inProc. 8th ACM Symp. Theory of Computing (STOC), 1978, pp. 216–225

    work page 1978

  6. [6]

    Computing a perfect strategy for n×nchess requires time exponential inn,

    A. S. Fraenkel and D. Lichtenstein, “Computing a perfect strategy for n×nchess requires time exponential inn,”Journal of Combinatorial Theory, Series A, vol. 31, no. 2, pp. 199–214, 1981

    work page 1981

  7. [7]

    Heads-up limit hold’em poker is solved,

    M. Bowling, N. Burch, M. Johanson, and O. Tammelin, “Heads-up limit hold’em poker is solved,”Science, vol. 347, no. 6218, pp. 145–149, 2015

    work page 2015

  8. [8]

    Superhuman AI for heads-up no-limit poker: Libratus beats top professionals,

    N. Brown and T. Sandholm, “Superhuman AI for heads-up no-limit poker: Libratus beats top professionals,”Science, vol. 359, no. 6374, pp. 418–424, 2018

    work page 2018

Show all 44 references
  1. [9]

    Superhuman AI for multiplayer poker,

    ——, “Superhuman AI for multiplayer poker,”Science, vol. 365, no. 6456, pp. 885–890, 2019

    2019

  2. [10]

    A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play,

    D. Silver, T. Hubert, J. Schrittwieser, I. Antonoglouet al., “A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play,”Science, vol. 362, no. 6419, pp. 1140–1144, 2018

    2018

  3. [11]

    Grandmaster level in StarCraft II using multi-agent reinforcement learning,

    O. Vinyals, I. Babuschkin, W. M. Czarneckiet al., “Grandmaster level in StarCraft II using multi-agent reinforcement learning,”Nature, vol. 575, no. 7782, pp. 350–354, 2019

    2019

  4. [12]

    Ensemble determinization in Monte Carlo tree search for the imperfect information card game Magic: The gathering,

    P. I. Cowling, C. D. Ward, and E. J. Powley, “Ensemble determinization in Monte Carlo tree search for the imperfect information card game Magic: The gathering,”IEEE Transactions on Computational Intelli- gence and AI in Games, vol. 4, no. 4, pp. 241–257, 2012

    2012

  5. [13]

    Monte Carlo search applied to card selection in Magic: The Gathering,

    C. D. Ward and P. I. Cowling, “Monte Carlo search applied to card selection in Magic: The Gathering,” in2009 IEEE Symposium on Computational Intelligence and Games, 2009, pp. 9–16

    2009

  6. [14]

    Monte Carlo tree search experi- ments in Hearthstone,

    A. Santos, P. Barros, and M. Arag ˜ao, “Monte Carlo tree search experi- ments in Hearthstone,” inProc. IEEE Conf. Computational Intelligence and Games (CIG), 2017, pp. 272–279

    2017

  7. [15]

    Improving Hearthstone AI by combining MCTS and supervised learning algorithms,

    S. Zhang and M. Buro, “Improving Hearthstone AI by combining MCTS and supervised learning algorithms,” inProc. AAAI Conf. Artificial Intelligence and Interactive Digital Entertainment (AIIDE), 2017, pp. 68–74

    2017

  8. [16]

    Deckbuilding in Magic: The Gathering using a genetic algorithm,

    M. Bjørke and D. Fludal, “Deckbuilding in Magic: The Gathering using a genetic algorithm,” inProceedings of NISK, 2017

    2017

  9. [17]

    Introducing the hearthstone-AI competition,

    T. Dockhornet al., “Introducing the hearthstone-AI competition,”arXiv preprint arXiv:1906.04238, 2019

    1906 arXiv

  10. [18]

    Summarizing strategy card game AI competition,

    J. Kowalski and R. Miernik, “Summarizing strategy card game AI competition,” in2023 IEEE Conference on Games (CoG), 2023, pp. 1–8

    2023

  11. [19]

    Formal proof — the four-color theorem,

    G. Gonthier, “Formal proof — the four-color theorem,”Notices of the American Mathematical Society, vol. 55, no. 11, pp. 1382–1393, 2008

    2008

  12. [20]

    A formally verified proof of the prime number theorem,

    J. Avigad, K. Donnelly, D. Gray, and P. Raff, “A formally verified proof of the prime number theorem,”ACM Transactions on Computational Logic, vol. 9, no. 1, pp. 2:1–2:23, 2007

    2007

  13. [21]

    The Lean mathematical library,

    The mathlib Community, “The Lean mathematical library,” inProceed- ings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). ACM, 2020, pp. 367–381

    2020

  14. [22]

    A formal proof of the kepler conjecture,

    T. Hales, M. Adams, G. Bauer, T. D. Dang, J. Harrison, H. Le Truong, C. Kaliszyk, V . Magron, S. McLaughlin, T. T. Nguyen, Q. T. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, A. H. Ta, T. D. Tran, T. H. Trieu, J. Urban, K. Vu, and R. Zumkeller, “A formal proof of...

    2017

  15. [23]

    Towards formal verification of card game mechanics,

    X. Li, J. Parsert, and C. Eisenhofer, “Towards formal verification of card game mechanics,” inProc. Workshop on Verification of Digital Systems (VDS), 2023, extended abstract

    2023

  16. [24]

    The logic of animal conflict,

    J. M. Smith and G. R. Price, “The logic of animal conflict,”Nature, vol. 246, pp. 15–18, 1973

    1973

  17. [25]

    Evolutionary stable strategies and game dynamics,

    P. D. Taylor and L. B. Jonker, “Evolutionary stable strategies and game dynamics,”Mathematical Biosciences, vol. 40, no. 1–2, pp. 145–156, 1978

    1978

  18. [26]

    J. W. Weibull,Evolutionary Game Theory. MIT Press, 1997

    1997

  19. [27]

    Pok ´emon trading card game — rules & resources,

    The Pok ´emon Company International, “Pok ´emon trading card game — rules & resources,” https://www.pokemon.com/us/pokemon-tcg/rules, 2024, accessed: 2026-02-20

    2024

  20. [28]

    Play pok ´emon tournament rules handbook,

    ——, “Play pok ´emon tournament rules handbook,” https://www.pokemon.com/us/play-pokemon/about/ tournaments-rules-and-resources, 2024, accessed: 2026-02-20

    2024

  21. [29]

    Probable inference, the law of succession, and statistical inference,

    E. B. Wilson, “Probable inference, the law of succession, and statistical inference,”Journal of the American Statistical Association, vol. 22, no. 158, pp. 209–212, 1927

    1927

  22. [30]

    Judgment under uncertainty: Heuristics and biases,

    A. Tversky and D. Kahneman, “Judgment under uncertainty: Heuristics and biases,”Science, vol. 185, no. 4157, pp. 1124–1131, 1974

    1974

  23. [31]

    Prospect theory: An analysis of decision under risk,

    D. Kahneman and A. Tversky, “Prospect theory: An analysis of decision under risk,”Econometrica, vol. 47, no. 2, pp. 263–291, 1979

    1979

  24. [32]

    A simple model of herd behavior,

    A. V . Banerjee, “A simple model of herd behavior,”The Quarterly Journal of Economics, vol. 107, no. 3, pp. 797–817, 1992

    1992

  25. [33]

    A theory of fads, fashion, custom, and cultural change as informational cascades,

    S. Bikhchandani, D. Hirshleifer, and I. Welch, “A theory of fads, fashion, custom, and cultural change as informational cascades,”Journal of Political Economy, vol. 100, no. 5, pp. 992–1026, 1992

    1992

  26. [34]

    Quantal response equilibria for normal form games,

    R. D. McKelvey and T. R. Palfrey, “Quantal response equilibria for normal form games,”Games and Economic Behavior, vol. 10, no. 1, pp. 6–38, 1995

    1995

  27. [35]

    Unraveling in guessing games: An experimental study,

    R. Nagel, “Unraveling in guessing games: An experimental study,” American Economic Review, vol. 85, no. 5, pp. 1313–1326, 1995

    1995

  28. [36]

    Nisan, T

    N. Nisan, T. Roughgarden, E. Tardos, and V . V . Vazirani, Eds.,Algo- rithmic Game Theory. Cambridge University Press, 2007

    2007

  29. [37]

    Equilibrium points inn-person games,

    J. F. Nash, “Equilibrium points inn-person games,”Proceedings of the National Academy of Sciences, vol. 36, no. 1, pp. 48–49, 1950

    1950

  30. [38]

    Zur Theorie der Gesellschaftsspiele,

    J. von Neumann, “Zur Theorie der Gesellschaftsspiele,”Mathematische Annalen, vol. 100, no. 1, pp. 295–320, 1928

    1928

  31. [39]

    Parameter estimation in large dynamic paired com- parison experiments,

    M. E. Glickman, “Parameter estimation in large dynamic paired com- parison experiments,”Journal of the Royal Statistical Society: Series C (Applied Statistics), vol. 48, no. 3, pp. 377–394, 1999

    1999

  32. [40]

    TrueSkill: A Bayesian skill rating system,

    R. Herbrich, T. Minka, and T. Graepel, “TrueSkill: A Bayesian skill rating system,” inAdvances in Neural Information Processing Systems, vol. 19. MIT Press, 2007

    2007

  33. [41]

    Hofbauer and K

    J. Hofbauer and K. Sigmund,Evolutionary Games and Population Dynamics. Cambridge University Press, 1998

    1998

  34. [42]

    W. H. Sandholm,Population Games and Evolutionary Dynamics. MIT Press, 2010

    2010

  35. [43]

    Analysis of swiss-system tournament pair- ings,

    O. Romero and I. Millet, “Analysis of swiss-system tournament pair- ings,”Journal of Quantitative Analysis in Sports, vol. 18, no. 3, pp. 213–229, 2022

    2022

  36. [44]

    Formally verified Pok ´emon TCG metagame analysis: Tournament data, matchup matrices, and Lean 4 proof artifact,

    A. F. Ramos and T. Soria, “Formally verified Pok ´emon TCG metagame analysis: Tournament data, matchup matrices, and Lean 4 proof artifact,” IEEE DataPort, 2026, https://dx.doi.org/10.21227/vty8-p429

    2026 doi

Pith tools

Reviewed July 10, 2026 · model on record in the stance chip above.