A Lean 4 formalization proves that the most popular Pokémon TCG deck is excluded from Nash equilibrium, demonstrating machine-checked metagame analysis over real tournament data.
Introducing the Hearthstone-AI Competition
1 Pith paper cite this work. Polarity classification is still indexing.
abstract
The Hearthstone AI framework and competition motivates the development of artificial intelligence agents that can play collectible card games. A special feature of those games is the high variety of cards, which can be chosen by the players to create their own decks. In contrast to simpler card games, the value of many cards is determined by their possible synergies. The vast amount of possible decks, the randomness of the game, as well as the restricted information during the player's turn offer quite a hard challenge for the development of game-playing agents. This short paper introduces the competition framework and goes into more detail on the problems and challenges that need to be faced during the development process.
fields
cs.GT 1years
2026 1verdicts
ACCEPT 1representative citing papers
citing papers explorer
-
From Rules to Nash Equilibria: A Lean 4 Case Study in Game-Theoretic Analysis of a Competitive Trading Card Game
A Lean 4 formalization proves that the most popular Pokémon TCG deck is excluded from Nash equilibrium, demonstrating machine-checked metagame analysis over real tournament data.