Lean Game Definitions

Définitions de types partagées en Lean 4, utilisées par plusieurs projets Lean de GameTheory. Projet Lake autonome et self-contained (zéro dépendance, cœur Lean uniquement) — fournit des définitions de référence recopiées dans les notebooks d’enseignement ; lake build est le chemin de vérification (localement et en CI).

Statut

  • Type : Projet Lake autonome (lakefile.toml, lean-toolchain pinné v4.32.1, lake-manifest.json)
  • Fichiers : 12 .lean (6 FR + 6 siblings _en, EPIC #4980 Pattern A)
  • Compte de sorry : 0 (définitions uniquement, pas de preuves)
  • Dépendance Mathlib : aucune — tous les fichiers utilisent le cœur de Lean 4 uniquement
  • Compilable isolément : Oui — lake build (harnais posé par #2752, review ai-01)
  • CI dédiée : .github/workflows/lean-game-defs.yml + lean-game-defs-ext.yml
  • Dernier audit sorry : 2026-05-29
  • Dernière correction de compilation : 2026-06-10 (See #2748)

Fichiers

  • Basic.lean — 107 lignes. Structures NormalFormGame, FiniteGame, Game2x2 + paiements espérés. Source : GameTheory-16-Lean-Definitions.ipynb.
  • Nash.lean — 139 lignes. Meilleure réponse, équilibre de Nash pur/mixte, dominance stricte. Source : GameTheory-16-Lean-Definitions.ipynb.
  • Combinatorial.lean — 113 lignes. GameTree, évaluation minimax, détermination victoire/défaite. Source : GameTheory-18-Lean-CombinatorialGames.ipynb.
  • SocialChoice.lean — 126 lignes. Preference, StrictPref, axiomes d’Arrow (énoncés). Source : GameTheory-19-Lean-SocialChoice.ipynb.
  • Bayesian.lean — Jeux bayésiens à information incomplète : BayesianGame, TypeStrategy, BayesianNashEquilibrium, InformationSet, SignalingGame, FirstPriceAuction, définitions du poker de Kuhn. Source : GameTheory-11-BayesianGames-Python.ipynb, GameTheory-13-ImperfectInfo-CFR-Python.ipynb.
  • Regret.lean — Minimisation du regret et CFR : CumulativeRegret, regretMatchingStrategy, CounterfactualRegret, CFRState, FictitiousPlayState. Source : GameTheory-13-ImperfectInfo-CFR-Python.ipynb, GameTheory-17-MultiAgent-RL-Python.ipynb.

Utilisation

Ces fichiers sont des définitions de référence (couche introductive, 0 preuve), vérifiables par lake build. Utilisation :

  1. Copier-coller dans une cellule de notebook (workflow pédagogique typique dans GameTheory-2b, GameTheory-8b, etc.).

  2. Importer depuis un projet Lake adjacent en ajoutant le chemin du fichier au lakefile.lean du projet. Exemple depuis game_theory_lean/SocialChoice/ :

    import GameTheory.lean_game_defs.Basic
import GameTheory.lean_game_defs.SocialChoice

  3. Exploration autonome via le kernel Lean 4 WSL (voir scripts/README.md pour la configuration du kernel).

Pour le support complet de PGame (théorie des jeux combinatoires dans toute sa généralité mathématique), utiliser Mathlib directement :

import Mathlib.SetTheory.PGame.Basic
import Mathlib.SetTheory.Game.Nim

Relation aux autres projets Lean de GameTheory

  • game_theory_lean/ — Projet Lake multi-module (StableMarriage = formalisation Gale-Shapley, EPIC #4365 ; CooperativeGames absorbé depuis cooperative_games_lean/ rm #6587).
  • game_theory_lean/SocialChoice/ — Module absorbé dans game_theory_lean (Arrow / Sen / électeur médian / Voting, EPIC #4365).
  • social_choice_lean_peters/ — Projet Lake indépendant référençant Peters au commit 94a4c650 du lake-manifest.json (Gibbard-Satterthwaite, Duggan-Schwartz).

Ces projets ne dépendent pas de lean_game_defs/ à la compilation — ils vendorent leurs propres définitions adaptées à leurs obligations de preuve. lean_game_defs/ est la couche introductive utilisée par les notebooks d’enseignement.

Architecture en couches — la couche de définitions introductive (ce module, sans preuves) vs. les projets Lake qui portent les preuves formelles (chacun vendore ses propres définitions) :

flowchart TD
    NOTEBOOKS["Notebooks d'enseignement<br/><i>copier-coller les définitions</i>"]
    INTRO["lean_game_defs/<br/><b>couche introductive</b><br/>définitions uniquement · 0 sorry · cœur Lean<br/>lake autonome (ce module)"]
    PROJ["Projets Lake — preuves formelles<br/>chacun vendore ses définitions adaptées"]
    SC["game_theory_lean/SocialChoice/<br/>Arrow · Sen · électeur médian<br/>Voting (absorbé, EPIC #4365)"]
    COOP["cooperative_games_lean/<br/>Shapley · Cœur · Banzhaf"]
    SM["game_theory_lean/<br/>StableMarriage (Gale-Shapley)"]
    CGT["conway_cgt_lean/<br/>surréels · nimbers (via Mathlib)"]

    NOTEBOOKS -->|"copier-coller"| INTRO
    INTRO -.->|"inspire (sans obligation de compilation commune)"| PROJ
    PROJ --> SC
    PROJ --> COOP
    PROJ --> SM
    PROJ --> CGT

Voir aussi

Conclusion

lean_game_defs/ est la couche de définitions introductive du track Lean de GameTheory : définitions de types partagées en Lean 4 (pas de preuves, 0 sorry) utilisées par les notebooks d’enseignement et recopiées par les projets Lake adjacents. C’est un projet Lake autonome depuis #2752 — lakefile.toml, lean-toolchain pinné, CI dédiée — sans aucune dépendance Mathlib : chaque fichier utilise le cœur de Lean 4 uniquement, et lake build vérifie l’ensemble (12 modules, FR + siblings _en).

Ce qu’elle fournit

Six fichiers de référence couvrant le curriculum de théorie des jeux : jeux sous forme normale / finis (Basic.lean), équilibre de Nash et dominance (Nash.lean), arbres de jeux combinatoires avec minimax (Combinatorial.lean), primitives de choix social et axiomes d’Arrow (SocialChoice.lean), jeux bayésiens et signalisation (Bayesian.lean), et minimisation du regret / CFR (Regret.lean). Chaque fichier correspond à un notebook d’enseignement spécifique et est autonome.

La carte du curriculum — six fichiers, du jeu sous forme normale jusqu’au CFR, chacun rattaché à son notebook pédagogique source :

flowchart LR
    BASIC["Basic.lean<br/>NormalFormGame · FiniteGame · Game2x2<br/><i>16-Lean-Definitions</i>"]
    NASH["Nash.lean<br/>meilleure réponse · Nash pur/mixte<br/>dominance stricte<br/><i>16-Lean-Definitions</i>"]
    COMB["Combinatorial.lean<br/>GameTree · minimax · détermination<br/><i>18-CombinatorialGames</i>"]
    SC["SocialChoice.lean<br/>Preference · axiomes d'Arrow<br/><i>19-SocialChoice</i>"]
    BAY["Bayesian.lean<br/>BayesianGame · Nash bayésien · poker de Kuhn<br/><i>11-Bayesian · 13-CFR</i>"]
    REG["Regret.lean<br/>CumulativeRegret · CFR · FictitiousPlay<br/><i>13-CFR · 17-MultiAgent-RL</i>"]

    BASIC --> NASH
    NASH --> COMB
    NASH --> SC
    NASH --> BAY
    BAY --> REG

Comment elle est utilisée

  • Copier-coller dans une cellule de notebook (le workflow pédagogique typique) ;
  • Importer depuis un projet Lake adjacent via import GameTheory.lean_game_defs.* ; ou
  • Explorer de façon autonome via le kernel Lean 4 WSL.

Pour la théorie complète des jeux combinatoires (PGame, surréels, nimbers), le track renvoie au SetTheory.PGame de Mathlib / à la visite conway_cgt_lean/ plutôt que de la redéfinir ici.

Où aller ensuite

Retour au sommet