La théorie du choix social étudie comment agréger des préférences individuelles en une décision collective. Ses résultats les plus célèbres sont des théorèmes d’impossibilité : le théorème d’Arrow (1951) montre qu’aucune règle de vote ne peut satisfaire simultanément des axiomes “raisonnables” (Pareto, IIA, non-dictature) dès que 3 alternatives ou plus sont en jeu ; le théorème de Sen (1970) démontre un conflit fondamental entre liberté individuelle et efficacité collective.
Parcours d’apprentissage
Les cinq premiers notebooks attaquent les mêmes résultats d’impossibilité sous des angles complémentaires – l’intuition par la simulation, la pratique électorale, la certitude formelle, la vérification automatique et la manipulation stratégique – qui convergent vers une cartographie des relaxations possibles ; le SC-06 ouvre la face coopérative du problème : agréger non plus des préférences mais des valeurs de coalition ; le SC-07 change une seconde fois d’objet — élire non plus un gagnant unique mais un comité, et y transférer la notion de stabilité : le core existe toujours (Becker, Greger & Peters).
flowchart TD
Result["Résultats d'impossibilité<br/>Arrow (1951) · Sen (1970)"]
E1["SC-01 · Simulation Python<br/>test empirique des axiomes (Geanakoplos)<br/>→ intuition"]
E2["SC-03 · Méthodes de vote<br/>Condorcet · Borda · électeur médian<br/>→ pratique électorale"]
E3["SC-02 · Preuve formelle Lean 4<br/>infinité des cas couverte · 0 sorry<br/>→ certitude"]
E4["SC-04 · Vérification SAT/Z3<br/>impossibilité = UNSAT<br/>→ vérification automatique"]
E5["SC-05 · Gibbard-Satterthwaite<br/>manipulation comme témoin<br/>→ comportement stratégique"]
E1 --> Result
E2 --> Result
E3 --> Result
E4 --> Result
E5 --> Result
Result -.- Relax["Cartographie des relaxations<br/>électeur médian (Downs) · Split Cycle<br/>chaque paire d'axiomes réalisable"]
Result -.- Coop["Face coopérative (SC-06)<br/>Möbius · dividendes de Harsanyi<br/>v = Σ m(T)·u_T · poids ≠ pouvoir"]
Coop -.- Comm["Comités par approbation (SC-07)<br/>core toujours non vide<br/>quotas Hare/Droop · certificats"]
Étape 1 : Le théorème d’Arrow par la simulation (SC-01, 45 min)
Le notebook SC-01 introduit les trois axiomes d’Arrow (Pareto faible, IIA, non-dictature) en les testant empiriquement sur des règles de vote usuelles (Borda, pluralité, dictature). Il suit la structure de la preuve de Geanakoplos (2005) – lemme extrémal, existence du pivot, dictateur partiel – et l’illustre pas à pas en Python. Le test empirique rend la triple contrainte tangible : chaque axiome pris isolément est satisfait par au moins une règle, mais aucune règle ne les satisfait tous les trois à la fois.
Sortie du SC-01 : trois panneaux (Borda, Pluralité, Dictature), chacun portant trois barres — Pareto, IIA, Non-dictature — en vert « SATISFAIT » ou rouge « VIOLÉ ». Borda et Pluralité respectent Pareto et la non-dictature mais violent l’IIA ; la Dictature satisfait Pareto et l’IIA mais viole la non-dictature. Aucun panneau n’est entièrement vert : la simulation matérialise l’impossibilité qu’Arrow démontre pour toute règle.
La conclusion du notebook montre alors pourquoi la preuve formelle couvre une infinité de cas que la simulation ne peut qu’échantillonner.
Étape 2 : Méthodes de vote et paradoxes (SC-03, 35 min)
Le notebook SC-03 implémente les règles de vote classiques (pluralité, Borda, Copeland) et déroule les paradoxes qui les minent, avant de montrer les conditions sous lesquelles un vainqueur cohérent réapparaît. Ce notebook est le compagnon Python du formalisme Lean du SC-02.
Le premier paradoxe est celui de Condorcet : la comparaison par paires à la majorité peut produire un cycle, si bien qu’aucune alternative ne bat toutes les autres.
Sortie du SC-03 : les trois alternatives A, B, C disposées en triangle, reliées par les arêtes du tournoi majoritaire (graphe orienté). Le cycle qu’elles forment est le résultat lui-même — aucun sommet ne domine les deux autres, donc aucun vainqueur de Condorcet n’existe.
Le théorème de Sen (1970) exhibe un conflit d’une autre nature — entre liberté individuelle et efficacité parétienne — sur l’exemple de Lady Chatterley.
Sortie du SC-03 : trois états sociaux a, b, c. Deux flèches vertes pleines encodent la liberté individuelle (le Prude décide c>a, le Lecteur décide b>c) ; une flèche orange pointillée horizontale porte l’étiquette Pareto (a>b, en rouge), tandis que la transitivité imposerait b>a (étiquette orange). Les relations forment un cycle a>b>c>a : les préférences collectives se contredisent, la liberté minimale et Pareto sont incompatibles.
À l’inverse, le théorème de l’électeur médian restaure l’existence d’un vainqueur dès que les préférences sont unimodales sur un axe unique.
Sortie du SC-03, deux panneaux : à gauche, l’histogramme des pics de préférence des électeurs avec la médiane (ligne pointillée rouge, ici à la position 5) ; à droite, trois courbes d’utilité unimodales (une par électeur), où l’utilité décroît linéairement avec la distance au pic. Sous cette hypothèse, la position médiane bat toute autre en duel majoritaire.
Le modèle de Downs (1957) en tire une prédiction politique : deux partis en concurrence pour les voix convergent vers l’électeur médian.
Sortie du SC-03, deux panneaux : à gauche, la distribution des électeurs avec les positions initiales (Gauche = 2, Droite = 8) et finales (toutes deux ≈ 4,8) des partis ; à droite, les trajectoires du parti de gauche (bleu, montant) et de droite (rouge, descendant) qui convergent en une vingtaine de rounds vers la médiane (vert pointillé). La compétition électorale aspire les deux partis vers le centre.
Étape 4 : Vérification mécanique par SAT et Z3 (SC-04, 45 min)
Le notebook SC-04 encode les théorèmes d’Arrow et de Sen comme des problèmes SAT (PySAT) et SMT (Z3). Le résultat UNSAT des solveurs constitue une preuve mécanique de l’impossibilité. Il compare les approches SAT (variables booléennes, clauses CNF) et SMT (variables entières, rangs sociaux), et analyse la relaxation des axiomes (chaque paire d’axiomes est réalisable). L’impossibilité se lit alors de deux façons complémentaires — conceptuellement comme une intersection vide de contraintes, et concrètement comme une explosion du nombre de profils à vérifier.
Illustration conceptuelle du SC-04 (et non une sortie du solveur), deux panneaux : à gauche, le diagramme de Venn des trois contraintes Pareto / IIA / Non-dictature dont l’intersection centrale est marquée « VIDE » ; à droite, la courbe semi-log du nombre de profils (m!)^k croissant avec le nombre d’alternatives m et d’électeurs k — 36 profils pour 2 électeurs et 3 alternatives, 216 pour 3 électeurs — avec l’annotation « Arrow ne s’applique pas » au point m = 2, seuil en deçà duquel le théorème est muet.
Étape 5 : Gibbard-Satterthwaite, la manipulation comme témoin (SC-05, 30 min)
Le notebook SC-05 retourne la question des quatre premières étapes : au lieu de demander quelle règle agrège honnêtement, il demande laquelle peut être instrumentée par un électeur stratégique. Une règle est manipulable s’il existe un profil et un électeur qui, avec un bulletin insincère, obtient un résultat strictement préféré — et le notebook exhibe ce témoin d’exploitation par le code (3 votants, 3 candidats, recherche explicite sur les bulletins), au lieu de le postuler. Le théorème de Gibbard-Satterthwaite (1973/1975) en donne la version générale : toute règle non-dictatoriale sur 3+ alternatives est manipulable ; sa formalisation Lean figure dans le tour de la librairie SocialChoiceLean du SC-02. Re-slot depuis GameTheory-22 (doctrine #5081, geste 1).
Étape 6 : Möbius sur le treillis des coalitions (SC-06, 40 min)
Le notebook SC-06 ouvre la face coopérative de l’agrégation : ce que l’on agrège n’est plus un classement mais une valeur de coalition \(v : 2^N \to \mathbb{R}\). La loi centrale est l’inversion de Möbius — \(v(S) = \sum_{T \subseteq S} m(T)\), où le dividende de Harsanyi \(m(T)\) mesure la synergie pure de \(T\) au-delà de ses sous-coalitions — vérifiée par reconstruction exacte puis mise au travail comme instrument de lecture du pouvoir (valeur de Shapley via les dividendes, calculée deux fois par des voies indépendantes ; indice de Banzhaf ; dummy du Luxembourg au Conseil européen de 1958) et de la manipulation pondérée (Gibbard-Satterthwaite sur un Borda à électeurs pondérés). La loi est attestée sur deux substrats indépendants : exécutée en Python (miroir de Mobius.mobiusCoeff / Mobius.mobiusReconstruction) et prouvée formellement dans le lac Lean du dépôt (Shapley.lean, phi_weightedUnanimity + shapley_uniqueness, 0 sorry).
Étape 7 : Élections de comité par approbation (SC-07, 40 min)
Le notebook SC-07 change d’objet une seconde fois : on n’élit plus un gagnant unique mais un comité de k sièges, sur des bulletins d’approbation. La notion de stabilité s’y transfère sous la forme du core : un comité W est dans le core si aucun groupe de votants (suffisamment gros au regard du quota Hare, confronté au quota Droop) ne peut lui opposer un ensemble de candidats qu’il approuverait unanimement. Le résultat central distillé — le théorème d’existence de Becker, Greger & Peters (arXiv 2609.11912) — est mis en machine sur le fil rouge n=4 votants, k=2 sièges : le comité favori des majoritaires n’est PAS dans le core (coalition bloquante exhibée), le comité proportionnel l’est, et un certificat de paiement (paiements + réserve) l’atteste. Trois règles concrètes — AV, PAV, règle de l’entropie harmonique — sont ensuite comparées sur 25 instances : leur taux de retour dans le core distingue ce qu’une règle simple garantit de ce qu’exige la stabilité.
Social Choice - Théorie du Choix Social
La théorie du choix social étudie comment agréger des préférences individuelles en une décision collective. Ses résultats les plus célèbres sont des théorèmes d’impossibilité : le théorème d’Arrow (1951) montre qu’aucune règle de vote ne peut satisfaire simultanément des axiomes “raisonnables” (Pareto, IIA, non-dictature) dès que 3 alternatives ou plus sont en jeu ; le théorème de Sen (1970) démontre un conflit fondamental entre liberté individuelle et efficacité collective.
Cette sous-série du parcours GameTheory explore ces résultats sous sept angles complémentaires : la simulation Python des axiomes, la formalisation en Lean 4 (preuve formelle), les méthodes de vote concrète, l’encodage SAT/Z3 pour la vérification mécanique, la manipulation stratégique comme témoin (Gibbard-Satterthwaite), l’agrégation coopérative par la décomposition de Möbius — dividendes de Harsanyi, poids contre pouvoir (SC-06) — et les élections de comité par approbation, où le core existe toujours (quotas Hare/Droop, certificats de paiement, SC-07).
À qui s’adresse cette série : étudiants en économie, informatique, sciences politiques et mathématiques appliquées. Les notebooks 01, 03, 06 et 07 ne nécessitent que Python (le 06 se contente de la bibliothèque standard). Les notebooks 02 (Lean) et 04 (SAT/Z3) requièrent des installations supplémentaires décrites dans le README parent. Aucun prérequis en théorie du choix social : les concepts sont introduits progressivement.
Notebooks
Durée totale : ~5h15
Parcours d’apprentissage
Les cinq premiers notebooks attaquent les mêmes résultats d’impossibilité sous des angles complémentaires – l’intuition par la simulation, la pratique électorale, la certitude formelle, la vérification automatique et la manipulation stratégique – qui convergent vers une cartographie des relaxations possibles ; le SC-06 ouvre la face coopérative du problème : agréger non plus des préférences mais des valeurs de coalition ; le SC-07 change une seconde fois d’objet — élire non plus un gagnant unique mais un comité, et y transférer la notion de stabilité : le core existe toujours (Becker, Greger & Peters).
Étape 1 : Le théorème d’Arrow par la simulation (SC-01, 45 min)
Le notebook SC-01 introduit les trois axiomes d’Arrow (Pareto faible, IIA, non-dictature) en les testant empiriquement sur des règles de vote usuelles (Borda, pluralité, dictature). Il suit la structure de la preuve de Geanakoplos (2005) – lemme extrémal, existence du pivot, dictateur partiel – et l’illustre pas à pas en Python. Le test empirique rend la triple contrainte tangible : chaque axiome pris isolément est satisfait par au moins une règle, mais aucune règle ne les satisfait tous les trois à la fois.
Sortie du SC-01 : trois panneaux (Borda, Pluralité, Dictature), chacun portant trois barres — Pareto, IIA, Non-dictature — en vert « SATISFAIT » ou rouge « VIOLÉ ». Borda et Pluralité respectent Pareto et la non-dictature mais violent l’IIA ; la Dictature satisfait Pareto et l’IIA mais viole la non-dictature. Aucun panneau n’est entièrement vert : la simulation matérialise l’impossibilité qu’Arrow démontre pour toute règle.
La conclusion du notebook montre alors pourquoi la preuve formelle couvre une infinité de cas que la simulation ne peut qu’échantillonner.
Étape 2 : Méthodes de vote et paradoxes (SC-03, 35 min)
Le notebook SC-03 implémente les règles de vote classiques (pluralité, Borda, Copeland) et déroule les paradoxes qui les minent, avant de montrer les conditions sous lesquelles un vainqueur cohérent réapparaît. Ce notebook est le compagnon Python du formalisme Lean du SC-02.
Le premier paradoxe est celui de Condorcet : la comparaison par paires à la majorité peut produire un cycle, si bien qu’aucune alternative ne bat toutes les autres.
Sortie du SC-03 : les trois alternatives A, B, C disposées en triangle, reliées par les arêtes du tournoi majoritaire (graphe orienté). Le cycle qu’elles forment est le résultat lui-même — aucun sommet ne domine les deux autres, donc aucun vainqueur de Condorcet n’existe.
Le théorème de Sen (1970) exhibe un conflit d’une autre nature — entre liberté individuelle et efficacité parétienne — sur l’exemple de Lady Chatterley.
Sortie du SC-03 : trois états sociaux a, b, c. Deux flèches vertes pleines encodent la liberté individuelle (le Prude décide c>a, le Lecteur décide b>c) ; une flèche orange pointillée horizontale porte l’étiquette Pareto (a>b, en rouge), tandis que la transitivité imposerait b>a (étiquette orange). Les relations forment un cycle a>b>c>a : les préférences collectives se contredisent, la liberté minimale et Pareto sont incompatibles.
À l’inverse, le théorème de l’électeur médian restaure l’existence d’un vainqueur dès que les préférences sont unimodales sur un axe unique.
Sortie du SC-03, deux panneaux : à gauche, l’histogramme des pics de préférence des électeurs avec la médiane (ligne pointillée rouge, ici à la position 5) ; à droite, trois courbes d’utilité unimodales (une par électeur), où l’utilité décroît linéairement avec la distance au pic. Sous cette hypothèse, la position médiane bat toute autre en duel majoritaire.
Le modèle de Downs (1957) en tire une prédiction politique : deux partis en concurrence pour les voix convergent vers l’électeur médian.
Sortie du SC-03, deux panneaux : à gauche, la distribution des électeurs avec les positions initiales (Gauche = 2, Droite = 8) et finales (toutes deux ≈ 4,8) des partis ; à droite, les trajectoires du parti de gauche (bleu, montant) et de droite (rouge, descendant) qui convergent en une vingtaine de rounds vers la médiane (vert pointillé). La compétition électorale aspire les deux partis vers le centre.
Étape 3 : Preuve formelle en Lean 4 (SC-02, 80 min)
Le notebook SC-02 formalise les préférences, les axiomes d’Arrow et de Sen, et le théorème de l’électeur médian en Lean 4. Il inclut un tour de la librairie SocialChoiceLean de DominikPeters (Gibbard-Satterthwaite, Split Cycle, 12 règles de vote, théorème de Duggan-Schwartz). Les définitions sont compatibles avec le projet Lake
game_theory_lean/SocialChoice/(0 sorry sur Arrow, Sen et Voting).Étape 4 : Vérification mécanique par SAT et Z3 (SC-04, 45 min)
Le notebook SC-04 encode les théorèmes d’Arrow et de Sen comme des problèmes SAT (PySAT) et SMT (Z3). Le résultat UNSAT des solveurs constitue une preuve mécanique de l’impossibilité. Il compare les approches SAT (variables booléennes, clauses CNF) et SMT (variables entières, rangs sociaux), et analyse la relaxation des axiomes (chaque paire d’axiomes est réalisable). L’impossibilité se lit alors de deux façons complémentaires — conceptuellement comme une intersection vide de contraintes, et concrètement comme une explosion du nombre de profils à vérifier.
Illustration conceptuelle du SC-04 (et non une sortie du solveur), deux panneaux : à gauche, le diagramme de Venn des trois contraintes Pareto / IIA / Non-dictature dont l’intersection centrale est marquée « VIDE » ; à droite, la courbe semi-log du nombre de profils
(m!)^kcroissant avec le nombre d’alternativesmet d’électeursk— 36 profils pour 2 électeurs et 3 alternatives, 216 pour 3 électeurs — avec l’annotation « Arrow ne s’applique pas » au point m = 2, seuil en deçà duquel le théorème est muet.Étape 5 : Gibbard-Satterthwaite, la manipulation comme témoin (SC-05, 30 min)
Le notebook SC-05 retourne la question des quatre premières étapes : au lieu de demander quelle règle agrège honnêtement, il demande laquelle peut être instrumentée par un électeur stratégique. Une règle est manipulable s’il existe un profil et un électeur qui, avec un bulletin insincère, obtient un résultat strictement préféré — et le notebook exhibe ce témoin d’exploitation par le code (3 votants, 3 candidats, recherche explicite sur les bulletins), au lieu de le postuler. Le théorème de Gibbard-Satterthwaite (1973/1975) en donne la version générale : toute règle non-dictatoriale sur 3+ alternatives est manipulable ; sa formalisation Lean figure dans le tour de la librairie SocialChoiceLean du SC-02. Re-slot depuis
GameTheory-22(doctrine #5081, geste 1).Étape 6 : Möbius sur le treillis des coalitions (SC-06, 40 min)
Le notebook SC-06 ouvre la face coopérative de l’agrégation : ce que l’on agrège n’est plus un classement mais une valeur de coalition \(v : 2^N \to \mathbb{R}\). La loi centrale est l’inversion de Möbius — \(v(S) = \sum_{T \subseteq S} m(T)\), où le dividende de Harsanyi \(m(T)\) mesure la synergie pure de \(T\) au-delà de ses sous-coalitions — vérifiée par reconstruction exacte puis mise au travail comme instrument de lecture du pouvoir (valeur de Shapley via les dividendes, calculée deux fois par des voies indépendantes ; indice de Banzhaf ; dummy du Luxembourg au Conseil européen de 1958) et de la manipulation pondérée (Gibbard-Satterthwaite sur un Borda à électeurs pondérés). La loi est attestée sur deux substrats indépendants : exécutée en Python (miroir de
Mobius.mobiusCoeff/Mobius.mobiusReconstruction) et prouvée formellement dans le lac Lean du dépôt (Shapley.lean,phi_weightedUnanimity+shapley_uniqueness, 0 sorry).Étape 7 : Élections de comité par approbation (SC-07, 40 min)
Le notebook SC-07 change d’objet une seconde fois : on n’élit plus un gagnant unique mais un comité de k sièges, sur des bulletins d’approbation. La notion de stabilité s’y transfère sous la forme du core : un comité W est dans le core si aucun groupe de votants (suffisamment gros au regard du quota Hare, confronté au quota Droop) ne peut lui opposer un ensemble de candidats qu’il approuverait unanimement. Le résultat central distillé — le théorème d’existence de Becker, Greger & Peters (arXiv 2609.11912) — est mis en machine sur le fil rouge n=4 votants, k=2 sièges : le comité favori des majoritaires n’est PAS dans le core (coalition bloquante exhibée), le comité proportionnel l’est, et un certificat de paiement (paiements + réserve) l’atteste. Trois règles concrètes — AV, PAV, règle de l’entropie harmonique — sont ensuite comparées sur 25 instances : leur taux de retour dans le core distingue ce qu’une règle simple garantit de ce qu’exige la stabilité.
Prerequisites
Installation
Pour le notebook 02 (Lean 4) : suivre les instructions dans README parent.
Formalisations Lean
Les notebooks SC-01 et SC-02 renvoient au projet Lake
game_theory_lean/SocialChoice/qui contient les preuves complètes :Arrow.leanSen.leanVoting.leanLe projet
social_choice_lean_peters/(au sein de cette série depuis #4362 ; DominikPeters, Lean 4 + Mathlib) formalise 12 règles de vote et 4 théorèmes d’impossibilité supplémentaires (Gibbard-Satterthwaite, Condorcet Participation, Condorcet Reinforcement, Duggan-Schwartz). Inventaire détaillé : LEAN_INVENTORY.md.Concepts clés
Navigation
Ressources
Conclusion / Prochaines étapes
Ce que vous avez appris
Cette sous-série vous a fait saisir pourquoi le choix social est l’un des résultats intellectuels les plus troublants de la théorie de la décision : il existe des limites mathématiquement prouvées à ce qu’une collectivité peut décider de manière cohérente. L’arc pédagogique repose sur sept angles complémentaires — cinq braqués sur les mêmes résultats d’impossibilité, les deux derniers changeant d’objet : la face coopérative puis l’élection de comité :
La thèse est puissante et honnêtement présentée : il n’existe pas de règle de vote idéale, mais un paysage de règles aux compromis clairement cartographiés — et la rigueur exige de les confronter simultanément à l’expérience, à la preuve formelle et à la vérification mécanique avant de prétendre les comprendre.
Prochaines étapes
game_theory_lean/SocialChoice/.Le fil rouge
Le choix social propose un changement de regard sur la décision collective : ne plus demander « quelle est la meilleure règle de vote ? » mais « quels axiomes suis-je prêt à sacrifier, et lesquels sont mutuellement incompatibles ? ». Cette sous-série vous a donné les résultats d’impossibilité (Arrow, Sen, Gibbard-Satterthwaite), les méthodes pour les établir (simulation, preuve Lean 4, vérification SAT/Z3), et l’intuition des relaxations (électeur médian, Split Cycle) pour transformer un constat d’impossibilité apparemment stérile en une compréhension fine de l’espace des règles possibles — en gardant à l’esprit qu’aucune règle ne domine partout, et que c’est précisément cette absence de « bonne » réponse universelle qui fait du choix social un domaine vivant.
Licence
Voir la licence du repository principal.