Kombinatorische Spieltheorie formalisiert in Lean 4
Combinatorial Games in Lean
Das Open-Source-Projekt 'Combinatorial Games' formalisiert die kombinatorische Spieltheorie im Beweisassistenten Lean 4. Es deckt allgemeine Spiele, Nimbers, surreale Zahlen und spezifische Spiele wie Hackenbush ab. Basierend auf Conway (2001) und weiteren Quellen, zielt es darauf ab, die Theorie vollständig maschinenverifiziert darzustellen.
Ein kombinatorisches Spiel ist ein Zwei-Personen-Spiel mit perfekter Information, das nach endlich vielen Zügen endet.