Agents-programmes a budget explicite - compagnon Python

Ce notebook est le compagnon Python du module Lean 4 ProgramGames.Bounded, livre par la PR #15395 dans le lake game_theory_lean. Le module represente explicitement le code public et le budget de raisonnement fini d’un agent-programme (modele structurel de Barasz et al. 2014 et Critch 2016), avec un interprete total : un budget nul produit immediatement une action, aucun resultat ne depend d’une recherche de preuve non bornee.

Le pivot conceptuel general reste GameTheory-06e-Open-Source-Game-Theory-Python.ipynb ; ce compagnon se concentre sur le modele borne et ne duplique pas son contenu.

Ce que fait ce notebook - et ce qu’il ne fait pas

Le role du compagnon Python est double :

1. reproduire independamment la famille finie de bots (cooperateBot, defectBotBounded, mirrorBot, basicFamily, canonicalPD) depuis zero, sans importer le code Lean ;
2. rejouer les certificats calculables du module et comparer chaque verdict Python au theoreme Lean correspondant.

La distinction est fondamentale : le Python verifie une matrice finie (quelques agents, quelques budgets) ; le Lean prouve des quantifications universelles (pour toute famille, pour tout adversaire de la liste). Un verdict Python conforme ne remplace jamais la preuve formelle - il la rend inspectable : chaque ligne du tableau ci-dessous peut etre relue, modifiee, contredite par l’etudiant. Ce notebook ne formalise ni logique de prouvabilite ni theoreme de Lob, et n’extrapole pas vers Godel : le module Lean lui-meme s’en garde explicitement.

Le code public et l’agent borne

Un BoundedAgent porte un code public inspectable (un des trois bots temoins) et un budget de raisonnement naturel. La traduction Python est fidele a la structure Lean ProgramCode / BoundedAgent :

from dataclasses import dataclass
from enum import Enum, auto


class ProgramCode(Enum):
    """Code public d'un agent-programme (ProgramCode du module Lean)."""
    COOPERATE_BOT = auto()
    DEFECT_BOT = auto()
    MIRROR = auto()


@dataclass(frozen=True)
class BoundedAgent:
    """Agent associant un code public a un budget de raisonnement fini."""
    code: ProgramCode
    budget: int

    def __repr__(self):
        return f"{self.__class__.__name__}({self.code.name}, budget={self.budget})"


cooperate_bot = BoundedAgent(ProgramCode.COOPERATE_BOT, 0)
defect_bot_bounded = BoundedAgent(ProgramCode.DEFECT_BOT, 0)
mirror_bot = BoundedAgent(ProgramCode.MIRROR, 1)
basic_family = [cooperate_bot, defect_bot_bounded, mirror_bot]

print("Famille temoin basicFamily :")
for agent in basic_family:
    print(f"  {agent}")

Famille temoin basicFamily :
  BoundedAgent(COOPERATE_BOT, budget=0)
  BoundedAgent(DEFECT_BOT, budget=0)
  BoundedAgent(MIRROR, budget=1)

Lecture de la sortie — la famille temoin et ses budgets. Trois lignes suffisent a poser le decor : BoundedAgent(COOPERATE_BOT, budget=0), BoundedAgent(DEFECT_BOT, budget=0), BoundedAgent(MIRROR, budget=1). Les deux bots vivent a budget nul — leur decision ne regarde ni l’historique ni l’adversaire, aucune memoire a payer. Le miroir seul porte budget=1 : relire le dernier coup adverse coute exactement une unite, et c’est ce cout qui distinguera le miroir riche (b=1, il reflete) du miroir casse (b=0, l’exercice 1 y viendra) — la meme ligne de code, deux comportements selon un seul entier. Toute la question du notebook est deja la : que reste-t-il du jeu quand la lecture a un prix ?

L’interprete total act

L’interprete ne fait aucune recherche de preuve : il inspecte le code adverse et le budget, puis produit une action. A budget nul, mirror deve (il n’a pas les moyens de simuler son adversaire) ; a budget positif, il coopere sauf contre le code explicitement defecteur :

def act(agent: BoundedAgent, opponent: ProgramCode) -> str:
    """Interprete total des codes publics (act du module Lean).

    Budget nul : mirror deve immediatement. Budget positif : mirror
    coopere sauf contre le code explicitement defecteur.
    """
    if agent.code is ProgramCode.COOPERATE_BOT:
        return "cooperate"
    if agent.code is ProgramCode.DEFECT_BOT:
        return "defect"
    # MIRROR
    if agent.budget == 0:
        return "defect"
    return "defect" if opponent is ProgramCode.DEFECT_BOT else "cooperate"


def outcome_bounded(row: BoundedAgent, column: BoundedAgent) -> tuple[str, str]:
    """Resultat ordonne de l'interprete : (action de row, action de column)."""
    return (act(row, column.code), act(column, row.code))

for left in basic_family:
    for right in basic_family:
        print(f"outcome_bounded({left.code.name:13s} b={left.budget}, "
              f"{right.code.name:13s} b={right.budget}) = {outcome_bounded(left, right)}")

outcome_bounded(COOPERATE_BOT b=0, COOPERATE_BOT b=0) = ('cooperate', 'cooperate')
outcome_bounded(COOPERATE_BOT b=0, DEFECT_BOT    b=0) = ('cooperate', 'defect')
outcome_bounded(COOPERATE_BOT b=0, MIRROR        b=1) = ('cooperate', 'cooperate')
outcome_bounded(DEFECT_BOT    b=0, COOPERATE_BOT b=0) = ('defect', 'cooperate')
outcome_bounded(DEFECT_BOT    b=0, DEFECT_BOT    b=0) = ('defect', 'defect')
outcome_bounded(DEFECT_BOT    b=0, MIRROR        b=1) = ('defect', 'defect')
outcome_bounded(MIRROR        b=1, COOPERATE_BOT b=0) = ('cooperate', 'cooperate')
outcome_bounded(MIRROR        b=1, DEFECT_BOT    b=0) = ('defect', 'defect')
outcome_bounded(MIRROR        b=1, MIRROR        b=1) = ('cooperate', 'cooperate')

Lecture chiffree — les issues bornees, ligne par ligne. La sortie egraine outcome_bounded sur chaque paire. Les lignes COOPERATE_BOT : (cooperate, cooperate) contre son semblable, (cooperate, defect) contre DEFECT_BOT — le coopereur ne s’adapte pas, il subit. Les lignes DEFECT_BOT font le symetrique : (defect, cooperate) puis (defect, defect). La ligne qui instruit est la troisieme colonne : contre MIRROR b=1, COOPERATE_BOT obtient ('cooperate', 'cooperate') — le miroir ouvre sur la cooperation, lit coop, et la boucle reste bloquee dessus ; DEFECT_BOT contre le miroir obtient la paire symetrique de defection : le miroir lit defect et le renvoie. Deux bots a budget nul ont des issues independantes du budget ; le miroir a b=1 est le seul dont l’issue depende de ce qu’il a pu lire — la famille temoin deliberate ce contraste.

La matrice des issues de la famille temoin se lit d’un coup d’oeil :

print("Matrice des issues de basicFamily (ligne = agent, colonne = adversaire)\n")
header = "".join(f"{a.code.name[:9]:>12s}" for a in basic_family)
print(f"{'':>14s}{header}")
for row in basic_family:
    cells_row = "".join(
        f"{outcome_bounded(row, col)[0][0].upper()}/{outcome_bounded(row, col)[1][0].upper():>4s}"
        for col in basic_family
    )
    print(f"{row.code.name[:9]:>12s} b={row.budget} {cells_row}")
print("\nC = cooperate, D = defect (format : action de l'agent en ligne / action de l'adversaire)")

Matrice des issues de basicFamily (ligne = agent, colonne = adversaire)

                 COOPERATE   DEFECT_BO      MIRROR
   COOPERATE b=0 C/   CC/   DC/   C
   DEFECT_BO b=0 D/   CD/   DD/   D
      MIRROR b=1 C/   CD/   DC/   C

C = cooperate, D = defect (format : action de l'agent en ligne / action de l'adversaire)

Lecture de la matrice — trois lignes, trois caracteres. Le tableau croise condense la sortie precedente : ligne = agent, colonne = adversaire, format action de l'agent / action de l'adversaire. La ligne COOPERATE_BOT affiche trois C/ : il coopere contre tous, sans exception ni memoire. La ligne DEFECT_BOT affiche trois D/ : defection systématique, le complement exact. La ligne MIRROR recopie la colonne de son adversaire : C/C face au coopereur, D/D face au defecteur, C/C face a lui-meme — la matrice entiere de MIRROR se deduit de la premiere ligne des autres. Cette symetrie de copie est la signature visuelle du miroir : dans un tableau fini, il apparait comme la transposee du champ adverse.

Le dilemme du prisonnier canonique et le rang de paiement

Le parametrage canonique est T=5, R=3, P=1, S=0. Le module definit un rang de paiement fini payoffRank (CC=3, CD=0, DC=5, DD=1) et prouve (payoffRank_le_iff) que ce rang preserve exactement l’ordre des paiements du jeu canonique - evitant de comparer des reels arbitraires :

CANONICAL_PD = {"T": 5, "R": 3, "P": 1, "S": 0}

def stage_payoff(row_action: str, col_action: str) -> int:
    """Paiement de l'agent ligne dans le PD canonique."""
    if row_action == "cooperate" and col_action == "cooperate":
        return CANONICAL_PD["R"]
    if row_action == "cooperate":
        return CANONICAL_PD["S"]
    if col_action == "cooperate":
        return CANONICAL_PD["T"]
    return CANONICAL_PD["P"]

def payoff_rank(row_action: str, col_action: str) -> int:
    """Rang fini du module Lean : CC=3, CD=0, DC=5, DD=1."""
    return {("cooperate", "cooperate"): 3, ("cooperate", "defect"): 0,
            ("defect", "cooperate"): 5, ("defect", "defect"): 1}[(row_action, col_action)]

print(f"PD canonique : {CANONICAL_PD}")
for pair in [("cooperate", "cooperate"), ("cooperate", "defect"),
             ("defect", "cooperate"), ("defect", "defect")]:
    print(f"  {pair} -> stage_payoff={stage_payoff(*pair)}, payoffRank={payoff_rank(*pair)}")

PD canonique : {'T': 5, 'R': 3, 'P': 1, 'S': 0}
  ('cooperate', 'cooperate') -> stage_payoff=3, payoffRank=3
  ('cooperate', 'defect') -> stage_payoff=0, payoffRank=0
  ('defect', 'cooperate') -> stage_payoff=5, payoffRank=5
  ('defect', 'defect') -> stage_payoff=1, payoffRank=1

Lecture chiffree — le rang de paiement encode l’ordre du dilemme. La sortie applique le PD canonique {'T': 5, 'R': 3, 'P': 1, 'S': 0} aux quatre issues. Chaque ligne porte deux nombres : ('cooperate','cooperate') -> stage_payoff=3, payoffRank=3, ('cooperate','defect') -> 0, 0, ('defect','cooperate') -> 5, 5, ('defect','defect') -> 1, 1. Ici rang et gain coincident chiffre a chiffre parce que les quatre valeurs sont distinctes — le rang est l’ordre total T > R > P > S aplati sur des entiers. Le vocabulaire compte pour la suite : payoffRank servira d’echelle comparable entre familles de paiements differentes, la ou stage_payoff brut n’est portable d’un jeu a l’autre. Le certificat final du notebook (16 paires) portera precisement sur ce rang.

Les organes calculables

Le module expose trois organes booleens - mutualCooperationCheck, unexploitableCheck, programNashCheck - dont Lean prouve qu’ils refletent exactement les definitions propositionnelles. Le Python les reproduit tels quels :

def mutual_cooperation_check(left: BoundedAgent, right: BoundedAgent) -> bool:
    """Organe de cooperation mutuelle (mutualCooperationCheck)."""
    return outcome_bounded(left, right) == ("cooperate", "cooperate")


def unexploitable_check(agent: BoundedAgent, opponents: list[BoundedAgent]) -> bool:
    """Organe d'inexploitabilite sur une famille finie (unexploitableCheck).

    Inexploitable : jamais (cooperate, defect) - jamais de cooperation
    unilaterale pendant que l'adversaire deve.
    """
    return all(outcome_bounded(agent, opp) != ("cooperate", "defect")
               for opp in opponents)


def program_nash_check(family: list[BoundedAgent],
                       left: BoundedAgent, right: BoundedAgent) -> bool:
    """Organe d'equilibre relatif pour le PD canonique (programNashCheck).

    Aucune substitution unilaterale dans la famille n'ameliore
    strictement le paiement (compare via le rang fini).
    """
    left_ok = all(
        payoff_rank(*outcome_bounded(alt, right))
        <= payoff_rank(*outcome_bounded(left, right))
        for alt in family
    )
    right_ok = all(
        payoff_rank(outcome_bounded(left, alt)[1], outcome_bounded(left, alt)[0])
        <= payoff_rank(outcome_bounded(left, right)[1], outcome_bounded(left, right)[0])
        for alt in family
    )
    return left_ok and right_ok

Rejeu des certificats Lean

Chaque theoreme du module est rejoue ci-dessous. Le verdict Python est calcule sur la matrice finie ; la colonne de droite rappelle le theoreme Lean qui couvre le cas generique. Certains couples partagent une meme ligne Python : les certificats 6 et 7 sont deux theoremes Lean distincts (l’assertion d’equilibre et sa version decidable) reposant sur une meme decision calculee.

Protocole de lecture — decoder une ligne de certificat. Chaque ligne de sortie a suivre a la meme grammaire : un nom court (mirror_mirror), un verdict Python=True, une fleche <-, puis l’enonce Lean dont c’est la replique (MutualCooperationBounded mirrorBot mirrorBot). Trois choses a ne pas confondre : le verdict True dit que LE CALCUL Python rend vrai sur la famille temoin, pas que l’enonce general est demontre ; le nom court est une cle de lecture, pas l’enonce ; et la fleche pointe de la preuve calculee vers la cible formelle — le sens du rejeu. Les enonces quantifies (sur toute une famille d’adversaires) se lisent differemment des egalites simples : l’interpretation qui suit cette section detaille ce partage.

certificats = []

def verifier(nom: str, verdict_python: bool, theoreme_lean: str):
    certificats.append((nom, verdict_python, theoreme_lean))
    print(f"{nom:42s} Python={str(verdict_python):5s}  <-  {theoreme_lean}")

# 1. Deux bots cooperateurs produisent la cooperation mutuelle
verifier("cooperate_cooperate",
         mutual_cooperation_check(cooperate_bot, cooperate_bot),
         "MutualCooperationBounded cooperateBot cooperateBot")

# 2. Deux bots defecteurs produisent la defection mutuelle
verifier("defect_defect",
         outcome_bounded(defect_bot_bounded, defect_bot_bounded) == ("defect", "defect"),
         "outcomeBounded defectBotBounded defectBotBounded = (defect, defect)")

cooperate_cooperate                        Python=True   <-  MutualCooperationBounded cooperateBot cooperateBot
defect_defect                              Python=True   <-  outcomeBounded defectBotBounded defectBotBounded = (defect, defect)

Lecture chiffree — les deux premieres egalites calculees. cooperate_cooperate Python=True <- MutualCooperationBounded cooperateBot cooperateBot : les deux coopereurs bornes cooperent mutuellement — une egalite que la matrice de la section precedente montrait deja case par case (C/ C en haut a gauche), ici confrontee a l’enonce exact. defect_defect Python=True <- outcomeBounded defectBotBounded defectBotBounded = (defect, defect) : la paire de defecteurs se defie mutuellement, meme egalite sur l’autre coin diagonal. Les deux certificats bornent la matrice par ses deux extremites pures — cooperation universelle d’un cote, defection universelle de l’autre — avant que les suivants n’attaquent les cas ou la strategie depend de l’autre.

Ce que chaque certificat engage

Les deux premiers certificats sont des egalites calculees sur la matrice finie : on evalue une decision et on la compare au membre droit de l’enonce Lean. Les suivants melangent deux natures : des egalites du meme genre, et un enonce quantifie (UnexploitableInFamily defectBotBounded opponents), dont le verdict ne se lit plus cellule par cellule mais sur toute la famille d’adversaires.

Un calcul Python peut corroborer un enonce quantifie sur la famille temoin ; il ne peut pas l’etablir pour une famille arbitraire. C’est le partage des roles que ce rejeu met en scene : le calcul exhibe un contre-exemple s’il en existe un, la preuve Lean fournit la quantification.

# 3. Le bot miroir coopere avec lui-meme (budget positif)
verifier("mirror_mirror",
         mutual_cooperation_check(mirror_bot, mirror_bot),
         "MutualCooperationBounded mirrorBot mirrorBot")

# 4. Le bot defecteur est inexploitable contre toute famille :
#    son action n'est JAMAIS cooperate (argument structurel,
#    verifie ici sur la famille temoin)
verifier("defectBotBounded_unexploitable",
         unexploitable_check(defect_bot_bounded, basic_family),
         "UnexploitableInFamily defectBotBounded opponents (quantifie)")

# 5. Le miroir est inexploitable dans la famille temoin
verifier("mirror_basicFamily_unexploitable",
         unexploitable_check(mirror_bot, basic_family),
         "unexploitableCheck mirrorBot basicFamily = true")

mirror_mirror                              Python=True   <-  MutualCooperationBounded mirrorBot mirrorBot
defectBotBounded_unexploitable             Python=True   <-  UnexploitableInFamily defectBotBounded opponents (quantifie)
mirror_basicFamily_unexploitable           Python=True   <-  unexploitableCheck mirrorBot basicFamily = true

Lecture chiffree — miroir, puis les deux inexploitabilites. Trois lignes, trois natures. mirror_mirror Python=True <- MutualCooperationBounded mirrorBot mirrorBot : deux miroirs a budget positif cooperent entre eux — chacun lit la cooperation initiale et la renvoie indefiniment, le budget de 1 suffit a entretenir la boucle. defectBotBounded_unexploitable Python=True <- UnexploitableInFamily defectBotBounded opponents : le defecteur est inexploitable DANS la famille — personne ne tire mieux que T=5 contre lui, et c’est un enonce quantifie sur tous les adversaires, pas une egalite ponctuelle. mirror_basicFamily_unexploitable Python=True <- unexploitableCheck mirrorBot basicFamily : le miroir aussi, sur la meme famille temoin. Noter la difference d’echelle des trois preuves : la premiere se verifie sur une case, les deux autres exigent le balayage de la famille entiere.

La proposition et son miroir decidable

Le module porte chaque enonce deux fois : comme proposition (ce que l’on prouve) et comme organe booleen (...Check ... = true, clos par decide). Les certificats 6 et 7 sont le meme fait sous ces deux formes. La decision calculee est identique ; seule change la cible Lean : un theoreme d’un cote, une fonction evaluable de l’autre.

Les deux formes ne sont pas redondantes : une proposition quantifiee se prouve, un organe booleen s’execute. Confronter l’une a l’autre est ce qui rend une divergence visible.

# 6. La defection mutuelle est un equilibre relatif dans la famille temoin
verifier("defect_profile_programNash",
         program_nash_check(basic_family, defect_bot_bounded, defect_bot_bounded),
         "ProgramNashBounded canonicalPD basicFamily defectBotBounded defectBotBounded")

# 7. Le meme certificat via l'organe booleen (Lean : decide)
verifier("defect_profile_check",
         program_nash_check(basic_family, defect_bot_bounded, defect_bot_bounded),
         "programNashCheck basicFamily defectBotBounded defectBotBounded = true")

# 8. Le rang fini preserve l'ordre des paiements (verification exhaustive 4x4)
rank_ok = all(
    (payoff_rank(a1, a2) <= payoff_rank(b1, b2))
    == (stage_payoff(a1, a2) <= stage_payoff(b1, b2))
    for a1 in ("cooperate", "defect") for a2 in ("cooperate", "defect")
    for b1 in ("cooperate", "defect") for b2 in ("cooperate", "defect")
)
verifier("payoffRank_le_iff (16 paires)", rank_ok,
         "payoffRank_le_iff : rang fini iff ordre des paiements")

print(f"\n{sum(1 for _, v, _ in certificats if v)}/{len(certificats)} certificats conformes")
assert all(v for _, v, _ in certificats), "divergence Python/Lean detectee"

defect_profile_programNash                 Python=True   <-  ProgramNashBounded canonicalPD basicFamily defectBotBounded defectBotBounded
defect_profile_check                       Python=True   <-  programNashCheck basicFamily defectBotBounded defectBotBounded = true
payoffRank_le_iff (16 paires)              Python=True   <-  payoffRank_le_iff : rang fini iff ordre des paiements

8/8 certificats conformes

Lecture chiffree — la ligne la plus riche : les 16 paires. Apres les certificats 6 et 7 (l’equilibre relatif de la defection mutuelle, en double ecriture proposition/organe), la sortie affiche payoffRank_le_iff (16 paires) Python=True <- payoffRank_le_iff : rang fini iff ordre des paiements. Le compte 16 est la vraie information : toutes les paires de paiements du PD canonique (issues et rangs croises) sont passees en revue, et pour chacune l’equivalence a ete evaluee — le rang et l’ordre s’accordent paire par paire, sans exception. La ligne finale 8/8 certificats conformes solde le rejeu : chaque fait calculable du module a sa replique Python identique, le partage des roles reste ce que la section suivante en dit.

Les 8 verdicts sont conformes : sur la matrice finie, le verificateur Python independant confirme chaque certificat calculable du module. La preuve Lean garde ce que le calcul ne peut pas : la quantification sur toutes les familles et tous les budgets.

Exercice 1 - Le miroir sans budget

Le module documente qu’a budget nul, mirror deve. On construit mirror_broke = BoundedAgent(ProgramCode.MIRROR, 0). Question : ce miroir sans budget est-il inexploitable dans basic_family ? La cooperation mutuelle est-elle encore possible ? Completer la fonction pour calculer les deux verdicts, puis verifier contre l’intuition : un miroir a budget nul se comporte structurellement comme quel bot de la famille ?

mirror_broke = BoundedAgent(ProgramCode.MIRROR, 0)

def verdicts_miroir_sans_budget():
    """Renvoie (inexploitable, cooperation_mutuelle_avec_lui_meme)."""
    # TODO Etudiant : utiliser unexploitable_check et mutual_cooperation_check
    # sur mirror_broke (contre basic_family puis contre lui-meme).
    result = None  # TODO etudiant
    return result

print("Exercice 1 a completer : verdicts_miroir_sans_budget()")
print("Indice : budget nul => act(MIRROR, _) renvoie toujours...")

Exercice 1 a completer : verdicts_miroir_sans_budget()
Indice : budget nul => act(MIRROR, _) renvoie toujours...

Exercice 2 - Famille etendue aux budgets

On etend la famille temoin avec des variantes de budget : basic_family_etendue = basic_family + [BoundedAgent(ProgramCode.MIRROR, 5), mirror_broke]. Question : le profil de defection mutuelle (defect_bot_bounded, defect_bot_bounded) reste-t-il un equilibre relatif dans cette famille etendue ? Et la cooperation mutuelle des miroirs (mirror_bot, mirror_bot) devient-elle equilibre ? Completer le calcul des deux verdicts et interpreter pourquoi la reponse differe entre les deux profils.

basic_family_etendue = basic_family + [
    BoundedAgent(ProgramCode.MIRROR, 5),
    mirror_broke,
]

def equilibres_famille_etendue():
    """Renvoie (nash_defection, nash_cooperation_miroirs) dans la famille etendue."""
    # TODO Etudiant : appeler program_nash_check deux fois sur
    # basic_family_etendue avec les profils (defect, defect) puis
    # (mirror_bot, mirror_bot).
    result = None  # TODO etudiant
    return result

print("Exercice 2 a completer : equilibres_famille_etendue()")
print("Indice : contre un miroir a budget positif, que rapporte la deviation ?")

Exercice 2 a completer : equilibres_famille_etendue()
Indice : contre un miroir a budget positif, que rapporte la deviation ?

Exercice 3 - Le paiement du miroir contre le defecteur

Le theoreme mirror_basicFamily_unexploitable affirme que le miroir a budget positif est inexploitable dans la famille temoin : il deve contre defectBotBounded, cooperant avec les autres. Question : quel paiement le miroir obtient-il effectivement contre chaque membre de la famille, et quel membre est son pire adversaire ? Completer le calcul du dict des paiements et du pire adversaire, puis conclure : inexploitable signifie-t-il optimal ?

def paiements_miroir():
    """Renvoie (dict {adversaire: paiement du miroir}, pire_adversaire)."""
    # TODO Etudiant : pour chaque agent de basic_family, calculer
    # stage_payoff(*outcome_bounded(mirror_bot, adversaire))
    # (attention : outcome_bounded renvoie (action miroir, action adversaire)).
    result = None  # TODO etudiant
    return result

print("Exercice 3 a completer : paiements_miroir()")
print("Indice : inexploitable protege du pire (S=0), pas de l'optimum (T=5).")

Exercice 3 a completer : paiements_miroir()
Indice : inexploitable protege du pire (S=0), pas de l'optimum (T=5).

Navigation et suite

• Pivot conceptuel : GameTheory-06e-Open-Source-Game-Theory-Python.ipynb
• Module Lean (FR) : game_theory_lean/ProgramGames/Bounded.lean - miroir anglais : Bounded_en.lean
• Noyau fonctionnel : game_theory_lean/ProgramGames/Basic.lean
• Lake complet : game_theory_lean/README.md

Ce compagnon couvre le versant calcul fini du modele borne ; le versant preuve formelle (les 8 theoremes en quantification universelle) vit dans le lake. Les exercices 1 a 3 restent a completer.