diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb index 4a28573e3e..670090b577 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb @@ -23,13 +23,13 @@ "## Pourquoi ce compagnon\n", "\n", "`calibration_lean` est un **micro-lake pedagogique** : trois modules courts, chacun avec\n", - "3-5 theoremes soigneusement choisis. Le lake est concu pour **etalonner** le harnais\n", + "3-5 théorèmes soigneusement choisis. Le lake est concu pour **etalonner** le harnais\n", "prover (iterations BG, agents multi), pas pour etre une bibliotheque reutilisable.\n", "Chaque cible exerce un chemin de preuve distinct :\n", "\n", - "- **Doomsday** : enchainement de fonctions, dates reelles calculables (#eval)\n", + "- **Doomsday** : enchainement de fonctions, dates réelles calculables (#eval)\n", "- **Nash PD** : analyse par cas sur `Fin 2`, pas de lemme de theorie des jeux dans Mathlib\n", - "- **Nim** : proprietes du XOR, lemmes cibles identifies (`Nat.xor_self`, `Nat.xor_zero`)\n", + "- **Nim** : propriétés du XOR, lemmes cibles identifies (`Nat.xor_self`, `Nat.xor_zero`)\n", "\n", "### Plan du notebook\n", "\n", @@ -42,9 +42,9 @@ "\n", "### Conventions du notebook\n", "\n", - "- **Kernel** : `lean4-wsl` (Lean 4 via WSL, requis pour executer le lake)\n", - "- **Sorties** : `#check` type, `#eval` calcul, `#print axioms` verification de la preuve\n", - "- **Pas de re-execution** : ce notebook utilise des `example : True := trivial` comme cellules neutres pour les exercices non resolus (convention C.1)\n", + "- **Kernel** : `lean4-wsl` (Lean 4 via WSL, requis pour exécuter le lake)\n", + "- **Sorties** : `#check` type, `#eval` calcul, `#print axioms` vérification de la preuve\n", + "- **Pas de re-exécution** : ce notebook utilise des `example : True := trivial` comme cellules neutres pour les exercices non resolus (convention C.1)\n", "\n", "### Substance formelle\n", "\n", @@ -57,9 +57,9 @@ "| Nim | `nim_winning_345` | `decide` | basse (etalon de coherence) |\n", "| Nim | `nimSum_self_cancel` | pivot `Nat.xor_self` | elevee (cible H du harnais) |\n", "\n", - "### Duree estimee\n", + "### Duree estimée\n", "\n", - "30 a 45 minutes en lecture interactive (kernel WSL requis pour l'execution reelle). Les sections 2-4 sont les plus substantielles -- le lecteur y voit la **difference entre une preuve qui calcule** (`#eval`) et une preuve qui **demontre** (`#print axioms`).\n", + "30 a 45 minutes en lecture interactive (kernel WSL requis pour l'exécution réelle). Les sections 2-4 sont les plus substantielles -- le lecteur y voit la **difference entre une preuve qui calcule** (`#eval`) et une preuve qui **démontre** (`#print axioms`).\n", "" ] }, @@ -106,7 +106,7 @@ "### Convention i18n FR/EN\n", "\n", "L'EPIC #4980 a ratifie la convention sibling pair : un fichier `.lean` (FR) coexiste\n", - "avec son jumeau `_en.lean` (EN). Les noms de theoremes restent en anglais (compat\n", + "avec son jumeau `_en.lean` (EN). Les noms de théorèmes restent en anglais (compat\n", "Mathlib, tactic DSL), seules les **docstrings** et les **commentaires** different.\n", "Dans ce lake, on importe uniquement les modules FR (les EN sont la pour la\n", "traduction automatique Phase 3).\n", @@ -125,7 +125,7 @@ "\n", "Le lakefile declare les modules buildés (`Calibration.Doomsday`, `Calibration.Nash`,\n", "`Calibration.Nim`) et leurs miroirs EN. Le repertoire racine `Calibration/` ne contient\n", - "que des `.lean`, pas de `.olean` directement -- c'est le compilateur qui decide de\n", + "que des `.lean`, pas de `.olean` directement -- c'est le compilateur qui décide de\n", "l'ordre de build selon les `import`.\n", "\n", "### Pourquoi ce lake est utile au harnais prover\n", @@ -133,7 +133,7 @@ "Le harnais prover (iterations BG, agents multi) a besoin de **cibles variees** pour\n", "etalonner ses strategies. Un seul type de cible (par exemple, uniquement du `decide`)\n", "ne teste qu'une competence (le pipeline SAT). Ce lake melange trois chemins :\n", - "1. Decide simple (`nim_winning_345`)\n", + "1. Décide simple (`nim_winning_345`)\n", "2. Lemme specifique (`nimSum_self_cancel` requiert `Nat.xor_self`)\n", "3. Pas de lemme (`strictly_domin_defect_pd` : analyse par cas)\n", "\n", @@ -291,10 +291,10 @@ "\n", "Chaque fonction est **pure** et **decidable**, ce qui permet le `#eval` direct.\n", "\n", - "### Verification empirique\n", + "### Vérification empirique\n", "\n", "`#eval dayOfWeek 2020 4 11` doit retourner `DayOfWeek.saturday`. Le compilateur Lean\n", - "execute reellement l'algorithme sur la date 11 avril 2020 et verifie que le resultat\n", + "exécute réellement l'algorithme sur la date 11 avril 2020 et vérifie que le résultat\n", "est samedi. C'est plus fort qu'un test unitaire : c'est une **preuve** que la\n", "formalisation est correcte pour cette date.\n", "\n", @@ -311,7 +311,7 @@ "\n", "### Sortie attendue\n", "\n", - "La cellule code[6] execute `#eval dayOfWeek 2026 8 21` (date du notebook), `#eval dayOfWeek 2020 4 11` (deces de Conway), `#eval doomsday 2026` (jour Doomsday de 2026). Chaque `#eval` doit retourner une valeur de `DayOfWeek`.\n", + "La cellule code[6] exécute `#eval dayOfWeek 2026 8 21` (date du notebook), `#eval dayOfWeek 2020 4 11` (deces de Conway), `#eval doomsday 2026` (jour Doomsday de 2026). Chaque `#eval` doit retourner une valeur de `DayOfWeek`.\n", "" ] }, @@ -656,7 +656,7 @@ } ], "source": [ - "-- L'algorithme EXECUTE (ces valeurs sont calculees par Lean, pas affichees a la main) :\n", + "-- L'algorithme Exécute (ces valeurs sont calculees par Lean, pas affichees a la main) :\n", "#eval doomsday 2026\n", "#eval doomsdayDate 8 2026 -- date pivôt d'aout\n", "#eval dayOfWeek 2026 8 21 -- le jour de ce commit\n", @@ -669,15 +669,15 @@ "source": [ "### Lecture des evaluations Doomsday\n", "\n", - "La cellule a execute quatre `#eval` :\n", + "La cellule a exécute quatre `#eval` :\n", "- `#eval doomsday 2026` : le jour Doomsday de 2026 (mardi)\n", "- `#eval doomsdayDate 8 2026` : la date pivôt d'aout 2026\n", "- `#eval dayOfWeek 2026 8 21` : le jour du 21 aout 2026 (jeudi)\n", "- `#eval dayOfWeek 2020 4 11` : le jour du deces de Conway (samedi)\n", "\n", - "### Verification croisee\n", + "### Vérification croisee\n", "\n", - "Chaque `#eval` est un **calcul**, pas une consultation. Lean a reellement evalue\n", + "Chaque `#eval` est un **calcul**, pas une consultation. Lean a réellement évalue\n", "`dayOfWeek 2020 4 11` en suivant le pipeline :\n", "1. `isLeapYear 2020` → `true` (2020 est bissextile)\n", "2. `centuryAnchor 2000` → jour 2 (mardi)\n", @@ -688,8 +688,8 @@ "### Le `#eval` comme oracle\n", "\n", "Le `#eval` est un **oracle de calcul** : si la valeur est decidable (ce qui est le\n", - "cas ici, `DayOfWeek` est un type fini), Lean l'evalue directement. C'est la forme\n", - "la plus **forte** de verification : pas une preuve par induction ou par axiome, mais\n", + "cas ici, `DayOfWeek` est un type fini), Lean l'évalue directement. C'est la forme\n", + "la plus **forte** de vérification : pas une preuve par induction ou par axiome, mais\n", "un calcul direct.\n", "\n", "### Limitation\n", @@ -847,7 +847,7 @@ } ], "source": [ - "-- Les theoremes de calibration du module :\n", + "-- Les théorèmes de calibration du module :\n", "#check leap_year_2000\n", "#check leap_year_1900\n", "#check leap_year_2024\n", @@ -871,16 +871,16 @@ "\n", "### Ce que cette preuve signifie\n", "\n", - "Le théorème `conway_death_day` est une **egalite dependante** : le membre gauche\n", + "Le théorème `conway_death_day` est une **égalité dependante** : le membre gauche\n", "(`dayOfWeek 2020 4 11`) est un calcul, le membre droit (`DayOfWeek.saturday`) est\n", - "une constante. Lean verifie l'egalite en **reduisant** le membre gauche jusqu'a\n", + "une constante. Lean vérifie l'égalité en **reduisant** le membre gauche jusqu'a\n", "obtenir `DayOfWeek.saturday`. C'est une preuve par **evaluation** (decidable), pas\n", "une preuve structurelle.\n", "\n", "### Difference avec une preuve par axiome\n", "\n", - "`#print axioms` liste les axiomes utilises. Si le theoreme utilisait `Classical.choice`\n", - "**sur une donnee non-decidable**, ce serait un signal d'alerte. Ici ici, l'axiome\n", + "`#print axioms` liste les axiomes utilises. Si le théorème utilisait `Classical.choice`\n", + "**sur une donnée non-decidable**, ce serait un signal d'alerte. Ici ici, l'axiome\n", "`Classical.choice` n'est utilise que dans le cadre de l'instance `DecidableEq` pour\n", "`DayOfWeek` (qui derive de la finitude de `Fin 7`).\n", "\n", @@ -894,17 +894,17 @@ "Le harnais prover peut essayer plusieurs strategies :\n", "1. `decide` (la plus directe, devrait fonctionner)\n", "2. `native_decide` (plus rapide mais moins puissant)\n", - "3. Pipeline manuel (decomposition des definitions)\n", + "3. Pipeline manuel (decomposition des définitions)\n", "\n", "C'est une cible **facile** (le `decide` ferme en 1-2 iterations) mais qui force le\n", "harnais a choisir entre strategies.\n", "\n", "### Limite pedagogique du `#eval`\n", "\n", - "Le `#eval` execute Lean comme un **langage de programmation**, pas comme un\n", - "**assistant de preuve**. Pour les preuves reelles, on utilise `rfl`, `decide`, ou\n", + "Le `#eval` exécute Lean comme un **langage de programmation**, pas comme un\n", + "**assistant de preuve**. Pour les preuves réelles, on utilise `rfl`, `decide`, ou\n", "des tactiques structurelles (`simp`, `omega`, `linarith`). Le `#eval` est ici\n", - "utilise pour **illustrer** la correction de la formalisation, pas comme methode\n", + "utilise pour **illustrer** la correction de la formalisation, pas comme méthode\n", "de preuve.\n", "\n", "### Sortie verbatim attendue\n", @@ -915,7 +915,7 @@ "```\n", "\n", "Cette sortie est la **signature de la preuve** : pas de `sorry`, pas d'axiome\n", - "exotique. Le compilateur Lean a verifie que la preuve est close.\n", + "exotique. Le compilateur Lean a vérifie que la preuve est close.\n", "" ] }, @@ -961,7 +961,7 @@ "```\n", "\n", "`a` domine strictement `a'` si **pour toute action de l'adversaire**, le paiement de\n", - "`a` est superieur. C'est la definition classique de la dominance stricte en theorie\n", + "`a` est supérieur. C'est la définition classique de la dominance stricte en theorie\n", "des jeux.\n", "\n", "### L'equilibre de Nash\n", @@ -975,7 +975,7 @@ "Un profil (a1, a2) est equilibre si **aucun joueur ne peut ameliorer son paiement\n", "en deviation unilaterale**.\n", "\n", - "### Le theoreme clef : strictly_domin_defect_pd\n", + "### Le théorème clef : strictly_domin_defect_pd\n", "\n", "`Trahir` domine strictement `Cooperer` dans le dilemme du prisonnier. La preuve ne\n", "peut **pas** invoquer de lemme de theorie des jeux dans Mathlib (Mathlib n'a pas de\n", @@ -1117,7 +1117,7 @@ } ], "source": [ - "-- Les definitions :\n", + "-- Les définitions :\n", "#check Game2x2\n", "#check Game2x2.payoff1\n", "#check Game2x2.payoff2\n", @@ -1267,12 +1267,12 @@ "source": [ "### Lecture de la matrice du dilemme\n", "\n", - "La cellule a execute trois `#eval` sur la matrice du dilemme :\n", + "La cellule a exécute trois `#eval` sur la matrice du dilemme :\n", "- `#eval prisonersDilemma.payoff1 Trahir Cooperer` = 5 (la tentation)\n", "- `#eval prisonersDilemma.payoff1 Cooperer Cooperer` = 3 (la recompense)\n", "- `#eval prisonersDilemma.payoff1 Trahir Trahir` = 1 (la punition)\n", "\n", - "### Verification de la matrice\n", + "### Vérification de la matrice\n", "\n", "La matrice du dilemme est :\n", "```\n", @@ -1281,7 +1281,7 @@ "Trahir 5 1\n", "```\n", "\n", - "Ces valeurs sont les **constantes du module** `Calibration.Nash`. Elles definissent\n", + "Ces valeurs sont les **constantes du module** `Calibration.Nash`. Elles définissent\n", "le jeu de maniere unique (avec la symetrie : payoff1(a,b) = payoff2(b,a)).\n", "\n", "### Interpretation economique\n", @@ -1295,7 +1295,7 @@ "\n", "L'equilibre de Nash est `(Trahir, Trahir)` : aucun joueur ne peut ameliorer son\n", "paiement en deviation unilaterale. Si l'adversaire trahit (donne 1), mieux vaut\n", - "trahir aussi (donne 1, meme resultat). Si l'adversaire coopere (donne 3),\n", + "trahir aussi (donne 1, meme résultat). Si l'adversaire coopere (donne 3),\n", "mieux vaut trahir (donne 5 au lieu de 3).\n", "\n", "### Paradoxe\n", @@ -1438,7 +1438,7 @@ } ], "source": [ - "-- Les quatre theoremes du dilemme :\n", + "-- Les quatre théorèmes du dilemme :\n", "#check strictly_domin_defect_pd\n", "#check pd_defect_is_pure_ne\n", "#check pd_cooperate_not_ne\n", @@ -1462,15 +1462,15 @@ "### Decomposition du paradoxe\n", "\n", "Le paradoxe du dilemme du prisonnier tient en 4 faits :\n", - "1. `Trahir` domine strictement `Cooperer` (chaque joueur prefere trahir contre toute action de l'adversaire)\n", + "1. `Trahir` domine strictement `Cooperer` (chaque joueur préfère trahir contre toute action de l'adversaire)\n", "2. `(Trahir, Trahir)` est l'equilibre de Nash (aucun ne regrette unilateralement)\n", "3. `(Cooperer, Cooperer)` **n'est PAS** un equilibre (chaque joueur peut ameliorer en trayant)\n", - "4. La **double defection** `(1, 1)` est Pareto-inferieure a la cooperation mutuelle `(3, 3)`\n", + "4. La **double defection** `(1, 1)` est Pareto-inférieure a la cooperation mutuelle `(3, 3)`\n", "\n", - "Les 4 faits sont prouves par le module `Calibration.Nash`. Ils sont **independants**\n", + "Les 4 faits sont prouvés par le module `Calibration.Nash`. Ils sont **independants**\n", "dans le sense que chaque preuve est mecanique (analyse par cas sur `Fin 2`).\n", "\n", - "### Verification des paiements\n", + "### Vérification des paiements\n", "\n", "```lean\n", "#eval prisonersDilemma.payoff1 Trahir Cooperer -- = 5\n", @@ -1478,9 +1478,9 @@ "#eval prisonersDilemma.payoff1 Trahir Trahir -- = 1\n", "```\n", "\n", - "Le `#eval` verifie la **matrice** du dilemme : la tentation (5), la recompense (3),\n", + "Le `#eval` vérifie la **matrice** du dilemme : la tentation (5), la recompense (3),\n", "la punition (1), le couillon (0). Ces valeurs sont les **constantes** du module,\n", - "elles definissent le jeu.\n", + "elles définissent le jeu.\n", "\n", "### Importance pour l'IA et l'economie\n", "\n", @@ -1517,7 +1517,7 @@ "strategie gagnante est connue depuis Bouton (1901/1902) : elle repose sur le **XOR\n", "des tailles de tas** (la somme de Grundy).\n", "\n", - "### Definition formelle\n", + "### Définition formelle\n", "\n", "```lean\n", "abbrev NimPosition := List Nat\n", @@ -1538,7 +1538,7 @@ "```\n", "\n", "Une position est gagnante pour le joueur qui doit jouer **si et seulement si** le\n", - "XOR des tailles est non nul. C'est le theoreme fondamental de Bouton.\n", + "XOR des tailles est non nul. C'est le théorème fondamental de Bouton.\n", "\n", "### Les lemmes d'auto-annulation\n", "\n", @@ -1549,7 +1549,7 @@ "\n", "Ces lemmes sont les **cibles D et H** du harnais prover. La cible H est la plus\n", "difficile : `nimSum_self_cancel` requiert `Nat.xor_self` (le lemme du XOR sur\n", - "l'egalite avec soi-meme), pas un `simp` generique.\n", + "l'égalité avec soi-meme), pas un `simp` générique.\n", "\n", "### Strategie gagnante\n", "\n", @@ -1561,7 +1561,7 @@ "\n", "Le calcul de `nimSum` est en **O(n)** ou n est le nombre de tas. Le calcul de la\n", "strategie gagnante (trouver le bon mouvement) est aussi en **O(n)**. C'est un des\n", - "rares jeux combinatoires ou la strategie gagnante est **computable en temps lineaire**.\n", + "rares jeux combinatoires ou la strategie gagnante est **computable en temps linéaire**.\n", "\n", "### Sortie attendue\n", "\n", @@ -1657,7 +1657,7 @@ } ], "source": [ - "-- Les definitions :\n", + "-- Les définitions :\n", "#check NimPosition\n", "#check nimSum\n", "#check isWinningNim" @@ -1787,7 +1787,7 @@ "source": [ "### Lecture des evaluations Nim\n", "\n", - "La cellule a execute cinq `#eval` :\n", + "La cellule a exécute cinq `#eval` :\n", "- `#eval nimSum [3, 4, 5]` = 2 (XOR des tailles)\n", "- `#eval isWinningNim [3, 4, 5]` = true (position gagnante)\n", "- `#eval nimSum [7, 7]` = 0 (position perdante par auto-annulation)\n", @@ -1828,7 +1828,7 @@ "### Pourquoi `nimSum []` = 0\n", "\n", "C'est une **convention** : la position vide est perdante pour le joueur qui doit\n", - "jouer (il ne peut pas jouer). Definir `nimSum [] = 0` (egal a la convention) rend\n", + "jouer (il ne peut pas jouer). Définir `nimSum [] = 0` (egal a la convention) rend\n", "la condition `isWinningNim p = nimSum p ≠ 0` coherente.\n", "\n", "### Sortie attendue\n", @@ -1980,9 +1980,9 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "### Lecture des theoremes Nim\n", + "### Lecture des théorèmes Nim\n", "\n", - "La cellule declare les cinq theoremes du module Nim et verifie la preuve de\n", + "La cellule declare les cinq théorèmes du module Nim et vérifie la preuve de\n", "`nimSum_self_cancel` par `#print axioms` :\n", "- `nim_winning_345` : la position [3, 4, 5] est gagnante (cible A)\n", "- `nimSum_single` : nimSum [n] = n (cible D)\n", @@ -1990,17 +1990,17 @@ "- `nimSum_cancel_pair` : generalisation pour paires\n", "- `nimSum_empty` : cas de base (nimSum [] = 0)\n", "\n", - "### Verification du certificat\n", + "### Vérification du certificat\n", "\n", "`#print axioms nimSum_self_cancel` doit lister les axiomes utilises. Pour cette\n", "preuve, on attend :\n", - "- `propext` : standard pour l'egalite des types inductifs\n", + "- `propext` : standard pour l'égalité des types inductifs\n", "- `Classical.choice` : pour les instances `Decidable`\n", "- `Quot.sound` : pour les types quotients (rare ici)\n", - "- Plus specifiquement : `Nat.xor_self` (le lemme du XOR sur l'egalite)\n", + "- Plus specifiquement : `Nat.xor_self` (le lemme du XOR sur l'égalité)\n", "\n", "L'absence de `sorry` est **essentielle** : un `sorry` indiquerait une preuve\n", - "incomplete, ce qui invaliderait la cible H.\n", + "incomplète, ce qui invaliderait la cible H.\n", "\n", "### Difference entre les cibles\n", "\n", @@ -2008,15 +2008,15 @@ "- **D (nimSum_single)** : necessite `Nat.xor_zero` (lemme specifique du XOR)\n", "- **H (nimSum_self_cancel)** : necessite `Nat.xor_self` (lemme plus profond)\n", "\n", - "La cible H est la plus interessante pedagogiquement : un `simp` generique stagne,\n", + "La cible H est la plus interessante pedagogiquement : un `simp` générique stagne,\n", "il faut **decouvrir** le bon lemme. C'est l'equivalent, en preuve formelle, du\n", "**pattern matching** : il faut identifier la **forme** de la preuve avant de\n", - "l'executer.\n", + "l'exécuter.\n", "\n", "### Role du `#check` vs `#print axioms`\n", "\n", "- `#check nim_winning_345` : type-check uniquement (rapide)\n", - "- `#print axioms nim_winning_345` : liste les axiomes (verification semantique)\n", + "- `#print axioms nim_winning_345` : liste les axiomes (vérification semantique)\n", "\n", "Les deux sont **necessaires** pour une cible de calibration : `#check` garantit la\n", "**correction syntaxique**, `#print axioms` garantit la **correction semantique**\n", @@ -2043,7 +2043,7 @@ "le joueur qui doit jouer. C'est la cible H du harnais : un `simp` naïf stagne, il faut\n", "pivoter vers le lemme spécifique `Nat.xor_self`.\n", "\n", - "### Verification XOR\n", + "### Vérification XOR\n", "\n", "```\n", "3 = 011 (bits)\n", @@ -2073,13 +2073,13 @@ "### Importance de `nimSum_self_cancel`\n", "\n", "C'est la **cible H** du harnais prover (la plus difficile). Sa preuve requiert :\n", - "1. Devoilement de la definition par `simp` ou `cases`\n", + "1. Devoilement de la définition par `simp` ou `cases`\n", "2. Reduction de `n ^^^ n` vers le lemme `Nat.xor_self`\n", "3. Application du lemme\n", "\n", - "Le `simp` generique stagne car il ne specialise pas vers `Nat.xor_self`. Le harnais\n", + "Le `simp` générique stagne car il ne specialise pas vers `Nat.xor_self`. Le harnais\n", "doit **decouvrir** que le lemme specifique est necessaire. C'est l'illustration du\n", - "**pivot du generique vers le specifique** que le harnais doit apprendre.\n", + "**pivot du générique vers le specifique** que le harnais doit apprendre.\n", "\n", "### Sortie attendue\n", "\n", @@ -2102,10 +2102,10 @@ "des tests unitaires :\n", "\n", "```lean\n", - "-- Cible A nim_winning_345 : decide simple, ferme en 1-2 iterations\n", + "-- Cible A nim_winning_345 : décide simple, ferme en 1-2 iterations\n", "-- Cible D nimSum_single : requiert Nat.xor_zero, non trivial mais borne\n", "-- Cible H nimSum_self_cancel : simp naif stagne, requiert Nat.xor_self cible\n", - "-- (pivot du generique vers le specifique)\n", + "-- (pivot du générique vers le specifique)\n", "-- Cible C strictly_domin_defect_pd : aucun lemme de theorie des jeux dans Mathlib\n", "-- -> analyse par cas sur Fin 2\n", "```\n", @@ -2118,7 +2118,7 @@ "Un harnais prover qui ne teste que des cibles `decide` ne valide que le **pipeline SAT**\n", "(solveur Z3). Un harnais qui ne teste que des lemmes specifiques ne valide que la\n", "**recherche de lemmes**. Un lake calibre melange les deux :\n", - "- Decide (`nim_winning_345`)\n", + "- Décide (`nim_winning_345`)\n", "- Lemme specifique (`nimSum_self_cancel`)\n", "- Pas de lemme (`strictly_domin_defect_pd`)\n", "\n", @@ -2145,9 +2145,9 @@ "\n", "`calibration_lean` est concu pour le **prouveur**, pas pour le compilateur. Les\n", "autres bancs d'essai du depot :\n", - "- `sudoku_lean` : solveur de Sudoku (mixte lemmes + decide)\n", + "- `sudoku_lean` : solveur de Sudoku (mixte lemmes + décide)\n", "- `knot_lean` : theorie des noeuds (lemmes topologiques)\n", - "- `stable_marriage_lean` : algorithme de Gale-Shapley (decide + inductif)\n", + "- `stable_marriage_lean` : algorithme de Gale-Shapley (décide + inductif)\n", "\n", "Chacun a son propre **profil de calibration**.\n", "" @@ -2161,11 +2161,11 @@ "Extrait des docstrings du lake (chemins de harnais par cible) :\n", "\n", "```lean\n", - "-- Cible A nim_winning_345 : decide simple, ferme en 1-2 iterations\n", + "-- Cible A nim_winning_345 : décide simple, ferme en 1-2 iterations\n", "-- (controle de coherence du pipeline)\n", "-- Cible D nimSum_single : requiert Nat.xor_zero, non trivial mais borne\n", "-- Cible H nimSum_self_cancel : simp naif stagne, requiert Nat.xor_self cible\n", - "-- (pivot du generique vers le specifique)\n", + "-- (pivot du générique vers le specifique)\n", "-- Cible C strictly_domin_defect_pd : aucun lemme de theorie des jeux dans Mathlib\n", "-- -> analyse par cas sur Fin 2\n", "```\n", @@ -2176,7 +2176,7 @@ "est : `Cible : `.\n", "\n", "- `` : A = facile (etalon), B-D = moyen (lemmes), E-H = difficile (pivot)\n", - "- `` : le nom du theoreme dans le module\n", + "- `` : le nom du théorème dans le module\n", "- `` : une ligne qui dit **pourquoi cette cible est interessante**\n", "\n", "### Pourquoi les lettres\n", @@ -2265,7 +2265,7 @@ "### Sortie attendue\n", "\n", "La cellule ne produit pas de sortie visible : c'est un commentaire pedagogique. Mais\n", - "le lecteur qui execute le notebook verra la these s'incarner dans les **resultats\n", + "le lecteur qui exécute le notebook verra la these s'incarner dans les **résultats\n", "concrets** : `nim_winning_345` ferme en 1-2 iterations (cible A), `nimSum_self_cancel`\n", "peut necessiter 5-10 iterations (cible H).\n", "" @@ -2288,7 +2288,7 @@ "Le pattern correct est :\n", "- Commentaire `-- #eval dayOfWeek 1789 7 14`\n", "- Cellule neutre `example : True := trivial`\n", - "- L'etudiant decommente et execute\n", + "- L'étudiant decommente et exécute\n", "\n", "C'est ce que font les cellules code[23], code[24], code[25].\n", "\n", @@ -2301,8 +2301,8 @@ "> **Indice pour l'exercice 1 :**", "\n", "Le siecle est 1700. L'ancre de 1700 n'est pas celle de 2000. Il faut consulter\n", - "`centuryAnchor 1700` (ou simplement executer `#eval dayOfWeek 1789 7 14` pour\n", - "verifier la reponse).\n", + "`centuryAnchor 1700` (ou simplement exécuter `#eval dayOfWeek 1789 7 14` pour\n", + "vérifier la reponse).\n", "\n", "> **Indice pour l'exercice 2 :**", "\n", @@ -2319,7 +2319,7 @@ "### Sortie attendue\n", "\n", "Aucune sortie visible -- les cellules contiennent `example : True := trivial` tant\n", - "que la solution est commentee. Quand l'etudiant decommente et execute, il obtient\n", + "que la solution est commentee. Quand l'étudiant decommente et exécute, il obtient\n", "les valeurs concretes (jour de la semaine, bool de position, paiements).\n", "" ] @@ -2567,7 +2567,7 @@ "\n", "| Cible | Module | Difficulte | Statut |\n", "|-------|--------|-----------|--------|\n", - "| A | Nim | basse (decide) | ferme en 1-2 iter |\n", + "| A | Nim | basse (décide) | ferme en 1-2 iter |\n", "| D | Nim | moyenne (Nat.xor_zero) | ferme en 2-4 iter |\n", "| H | Nim | elevee (Nat.xor_self) | ferme en 5-10 iter |\n", "| C | Nash | elevee (cases Fin 2) | ferme en 3-5 iter |\n", @@ -2576,9 +2576,9 @@ "\n", "### Trois takeaways\n", "\n", - "1. **Le `#eval` est un oracle** : si la date est calculable, Lean la calcule reellement.\n", + "1. **Le `#eval` est un oracle** : si la date est calculable, Lean la calcule réellement.\n", "2. **Le `#print axioms` est un certificat** : la liste des axiomes utilises est la preuve que la preuve est close.\n", - "3. **Le `#check` est un typage** : il valide la signature du theoreme sans l'executer.\n", + "3. **Le `#check` est un typage** : il valide la signature du théorème sans l'exécuter.\n", "\n", "### Cycle suivant\n", "\n", @@ -2593,9 +2593,9 @@ "transpose a :\n", "- **Generation de code** : un harnais de generation SQL pourrait avoir des cibles « schema inconnu », « schema connu », « requete recursive »\n", "- **Theorem proving Coq/Agda** : les lemmes specifiques sont l'equivalent de la cible H\n", - "- **Verification formelle de circuits** : les proprietes de stabilite sont equivalentes a des lemmes decidables\n", + "- **Vérification formelle de circuits** : les propriétés de stabilite sont equivalentes a des lemmes decidables\n", "\n", - "C'est un **pattern general** de l'outillage de verification.\n", + "C'est un **pattern général** de l'outillage de vérification.\n", "\n", "### Pour aller plus loin\n", "\n", @@ -2606,7 +2606,7 @@ "### References\n", "\n", "- Conway 1982 *Doomsday Algorithm* (originaux, presentation a Cambridge)\n", - "- Bouton 1901/1902 *Nim, a game with a complete mathematical theory* Annals of Mathematics\n", + "- Bouton 1901/1902 *Nim, a game with a complète mathematical theory* Annals of Mathematics\n", "- Nash 1950 *Equilibrium Points in n-Person Games* PNAS (Nobel 1994)\n", "- Bouton-Nash-Sprague-Grundy 1902-1936 : theorie des jeux combinatoires et du mex\n", "- EPIC #4980 (convention sibling pair FR/EN pour Lean)\n", @@ -2629,4 +2629,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file