Lean 4で組合せゲーム理論を形式化するライブラリ「combinatorial-games」
Combinatorial Games in Lean
Lean 4で書かれた組合せゲーム理論の形式化ライブラリ。NimやHackenbushなどのゲーム、温度や可逆位置などの一般理論、ニンバー（代数的閉体性や拡張定理）、そしてConwayの超現実数（体構造やHahn級数表現）を対象とする。Conwayの『On Numbers and Games』を基盤に、Schleicher & StollやSiegelの文献を補助として使用。GitHub上で開発が進められており、10人のコントリビューターが参加している。
組合せゲームとは、二人のプレイヤー（LeftとRight）が完全情報のもとで交互にゲーム状態を変更し、手番で動けなくなった方が負けとなる、終端が保証されたゲームです。