从规则到纳什均衡：竞争性集换式卡牌游戏博弈论分析的Lean 4案例研究

我们展示了竞技宝可梦集换式卡牌游戏的元游戏分析，该分析在Lean 4中基于真实锦标赛数据进行了机器验证。主要的博弈论结果，包括纳什均衡、复制者动力学和矩阵级类型桥接计算，依赖于native_decide，它信任Lean的编译器而非其内核；信任边界被明确说明。该工件跨越约31,900行、87个文件和2,627个定理，其中约200个直接验证了实证声明，没有sorry、admit或自定义公理。分析2026年1月至2月Trainer Hill中至少50名玩家参与的事件数据，涵盖14种原型及其完整的成对对战矩阵，我们证明了一个流行度悖论：使用率最高的卡组Dragapult，拥有15.5%的元游戏份额，但预期胜率仅为46.7%，而Grimmsnarl以5.1%的份额实现了52.7%的胜率。原始游戏的机器验证纳什均衡赋予Dragapult 0%的权重；对所有非空支撑子集的穷举枚举确认了常数和对称化游戏的唯一对称纳什均衡，其支撑包含七个卡组。针对此均衡混合策略，Dragapult低于游戏价值40.4个千分点。单步复制者动力学表明Dragapult面临向下的适应度压力，Grimmsnarl面临向上的压力，而Alakazam面临最强的灭绝压力。10,000次迭代的敏感性分析确认了定性稳定性，核心支撑卡组出现在超过96%的重采样均衡中。主要贡献是方法论上的：一个可复现的案例研究，展示了形式验证如何将定性的元游戏叙事转变为可机器检查、可重运行的策略科学。