GameTheory — Théorie des jeux

Série pédagogique niveau 2 — Nash, Lemke-Howson, Folk, Shapley, Arrow, CFR, preuves Lean 4

Série GameTheory du dépôt CoursIA — équilibre de Nash, théorème minimax, dynamiques d’apprentissage, jeux coopératifs (Shapley, Core), mécanismes (VCG, Gale-Shapley), choix social (Arrow), formalisation Lean 4.

GameTheory — Théorie des jeux et choix social

La théorie des jeux est le langage mathématique de la stratégie. Cette série forme sur deux axes complémentaires : simuler des jeux avec Nashpy et OpenSpiel (équilibres de Nash, tournois itératifs, CFR/Deep CFR) et prouver des résultats en Lean 4 (existence de Nash via Brouwer/Kakutani, théorème d’Arrow, valeur de Shapley). À la fin, vous maîtriserez la théorie des jeux coopératifs (Shapley, Core) et non-coopératifs (Nash, SPE), et vous saurez formaliser ces résultats dans un assistant de preuve.

Vue d’ensemble

La série GameTheory comporte 96 notebooks racine + 8 SocialChoice répartis en 3 phases thématiques et une sous-série SocialChoice dédiée. Chaque notebook principal (Python/.NET) est exécuté et commité avec ses sorties (règle C.2). Les side tracks Lean 4 (*-Lean-*) requièrent WSL + elan ; les side tracks Python (*-Python) ajoutent des approfondissements.

Phase	Notebooks	Focus pédagogique
Phase 1 — Fondations statiques (1-6)	12+	Forme normale, dominance, équilibre de Nash (pur + mixte), Lemke-Howson, minimax, évolution de la confiance
Phase 2 — Dynamiques et information (7-12)	12+	Forme extensive, jeux combinatoires (Sprague-Grundy), induction arrière, SPE, jeux bayésiens, réputation
Phase 3 — Frontières (13-17)	7+	CFR, jeux différentiels, coopératifs (Shapley/Core), mécanismes (VCG, Gale-Shapley), multi-agent RL
SocialChoice (sous-série)	4	Arrow (impossibilité), formalisation Lean, méthodes de vote, agrégation computationnelle SAT/Z3

Kernels : python3 · .net-csharp (notebooks 2-12) · lean4 (side tracks *-Lean-* via WSL) · GPU : non · Prérequis : algèbre linéaire, probabilités de base. Aucun prérequis en théorie des jeux : les concepts sont introduits depuis les matrices de gains.

Parcours : Parcours 1 — local sobre · niveau 2

Phase 1 — Fondations statiques et équilibre de Nash (Notebooks 1-6)

Notebooks 1 à 6 + side tracks Lean (définitions, existence de Nash, minimax) et Python (existence Nash).

Phase 2 — Dynamiques, induction et information incomplète (Notebooks 7-12)

Notebooks 7 à 12 : forme extensive, jeux combinatoires, induction arrière, induction avant, jeux bayésiens, jeux de réputation.

Phase 3 — Frontières : algorithmes, coopération, mécanismes (Notebooks 13-17)

Notebooks 13 à 17 : CFR pour information imparfaite, jeux différentiels, coopératifs (Shapley/Core), mécanismes (VCG), multi-agent RL.

SocialChoice — Choix social et agrégation (sous-série)

Sous-série dédiée : impossibilité d’Arrow, formalisation Lean, méthodes de vote (Condorcet/Borda/Copeland), agrégation computationnelle (SAT/Z3).

Démarrage rapide

git clone https://github.com/jsboige/CoursIA.git
cd CoursIA
python -m venv .venv
source .venv/bin/activate     # ou .venv\Scripts\activate sous Windows
pip install jupyter papermill nashpy numpy matplotlib networkx
jupyter notebook MyIA.AI.Notebooks/GameTheory/

Pour les side tracks Lean 4 (*-Lean-*.ipynb) : WSL + elan toolchain + kernel Lean4 Jupyter (cf. MyIA.AI.Notebooks/GameTheory/install_wsl_kernel.md). Pour les side tracks Python (*-Python.ipynb) : Python seul suffit.

Ressources complémentaires

• Catalogue : COURSE_CATALOG.generated.md — inventaire exhaustif de la série avec statuts READY/DEMO, kernels, GPU.
• README de série : GameTheory/README.md — table des matières détaillée, structure pédagogique complète, side tracks Lean/Python.
• Séries connexes : Search (BFS/A*/MCTS, certains algorithmes sont des cas particuliers de théorie des jeux), Sudoku (CSP, vus comme jeux à un joueur), SymbolicAI/Planners (planification, théorie de la décision).

Note sur le rendu Quarto (.NET + Lean)

Cette page Quarto rend les notebooks Python natifs (et leurs _output.ipynb quand disponibles). Les notebooks .NET C# (notebooks 2-12 principaux) et les side tracks Lean 4 ne sont pas exécutés par Quarto : leur rendu s’appuie sur les *_output.ipynb committés dans le dépôt (règle C.2) via le mode freeze: auto de _quarto.yml. Pour une exécution locale des notebooks .NET, configurer le kernel dotnet-csharp ; pour Lean 4, suivre install_wsl_kernel.md. Ce point est la matière de la tranche 4 #4211 (GH Actions deploy) — un workflow dédié pourra automatiser l’exécution et la publication.

Pour aller plus loin

Une fois la série GameTheory maîtrisée, les parcours conseillés sont :

1. Vers l’apprentissage par renforcement : RL — multi-agent RL, équilibres appris, CFR approfondi
2. Vers le choix social et la décision collective : sous-série SocialChoice — Arrow, Sen, Condorcet
3. Vers la formalisation : SymbolicAI/Lean — preuves formelles en Lean 4
4. Vers l’optimisation et la planification : SymbolicAI/Planners — planificateurs, OR-tools