ポケモンカードゲームの競技メタゲーム（対戦環境）をゲーム理論で分析し、その結果をLean 4という定理証明支援系で機械的に検証したという画期的な研究が発表されました。このプロジェクトでは、実際の大会データを用いて約31,900行、87ファイル、2,627個の定理から成る膨大な検証アーティファクトが構築されており、その中の約200個が実証的な主張を直接的に検証しています。特筆すべきは、sorryやadmitといった未証明要素やカスタム公理を一切使用せず、完全に機械検証されている点です。 研究チームは2026年1月から2月のTrainer Hillデータから、50人以上が参加した大会を対象に、14種類のデッキアーキタイプとその完全な相互マッチアップマトリックスを分析しました。その結果、興味深い「人気のパラドックス」が発見されました。最も使用されているデッキであるドラパルトは全体の15.5%のメタゲームシェアを占めながら、期待勝率は46.7%に過ぎません。一方、グリムスナール（シェア5.1%）は52.7%という高い勝率を記録していたのです。 ナッシュ均衡の計算では、機械検証によりドラパルトに0%の重みが割り当てられました。全ての空でないサポート部分集合に対する網羅的列挙により、7種類のデッキで構成される唯一の対称ナッシュ均衡が確認されました。このゲーム均衡値と比較すると、ドラパルトは40.4パーミル下回っており、レプリケーターダイナミクス（進化動学）分析からもドラパルトには下向きの適応度圧力が、グリムスナールには上向きの圧力が確認されました。アラカザムが最も強い絶滅圧力にさらされていたほか、10,000回の感度分析により、コアなサポートデッキは再サンプリングされた均衡の96%以上に出現することが確認され、結果の堅牢性が示されました。 この研究の主要な貢献は方法論的なもので、形式検証がいかに定性的なメタゲーム分析を機械検証可能で再現性のある戦略科学へと転換できるかを示す、実用的で再利用可能なケーススタディとなっています。