From 1efd9bcd3b481a8303444d01b83eb01e12e64e97 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 27 Oct 2026 11:18:13 +0100 Subject: [PATCH 1/5] Refactor(analyse,#22649): etape c -- companion natif ANALYSE-06 devient 06b (git mv seul) Decision des deux objets distincts : commentaire 6413771956 sur #22649. Renommage pur, aucun octet de contenu modifie. Le recablage de navigation (etape d, #22671) vient apres, en PR empilee. Co-Authored-By: Claude Sonnet 5.5 --- ...te-2026-Lean.ipynb => ANALYSE-06b-Sensibilite-2026-Lean.ipynb} | 0 ...6-Lean_en.ipynb => ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/{ANALYSE-06-Sensibilite-2026-Lean.ipynb => ANALYSE-06b-Sensibilite-2026-Lean.ipynb} (100%) rename MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/{ANALYSE-06-Sensibilite-2026-Lean_en.ipynb => ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb} (100%) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb similarity index 100% rename from MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb rename to MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb similarity index 100% rename from MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb rename to MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb From 266ade7b68a0b35802cadfb5053f0f321ac6c1e8 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 27 Oct 2026 15:41:51 +0100 Subject: [PATCH 2/5] Fix(#22649): le rename 06->06b emporte ses registres -- reserve Hermes #22932 Option 1 de la review : les corrections mecaniques embarquent dans la PR. README ANALYSE (2 liens + labels), liens croises intra-paire cellule 0 des deux carnets (cibles seules), pedagogy_density_baseline.json (2 cles), translation_golden_set.json (fr/en), _quarto.yml render list (2 entrees -- sinon le build Quarto de main casse au merge), docs/curriculum (2 liens, meme famille). COURSE_CATALOG.generated.* intouchable (regle catalogue, regenere par l'automatisation). 11+/11-, aucune cellule code touchee. Co-Authored-By: Claude Sonnet 5.5 --- .../Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb | 2 +- .../Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb | 2 +- MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md | 2 +- _quarto.yml | 4 ++-- docs/curriculum/ia-symbolique.md | 4 ++-- scripts/notebook_tools/pedagogy_density_baseline.json | 4 ++-- translations/translation_golden_set.json | 4 ++-- 7 files changed, 11 insertions(+), 11 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb index 9c7f0ca4dc5..16652c0186f 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb @@ -28,7 +28,7 @@ "\n", "| Notebook précédent | Notebook suivant |\n", "|---|---|\n", - "| [ANALYSE-04 — Trois primitives de PFR](ANALYSE-04-PFR-Primitives-Python.ipynb) | [ANALYSE-06 — version anglaise](ANALYSE-06-Sensibilite-2026-Lean_en.ipynb) |" + "| [ANALYSE-04 — Trois primitives de PFR](ANALYSE-04-PFR-Primitives-Python.ipynb) | [ANALYSE-06 — version anglaise](ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb) |" ] }, { diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb index 00d2be7c70d..9f74604a2c1 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb @@ -28,7 +28,7 @@ "\n", "| Previous notebook | French version | Next notebook |\n", "|---|---|---|\n", - "| [ANALYSE-04 — Three PFR primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [ANALYSE-06 — French version](ANALYSE-06-Sensibilite-2026-Lean.ipynb) | [Lean-12b — Huang's Sensitivity Theorem](../Lean-12b-Lean-Sensitivity-Theorem.ipynb) |" + "| [ANALYSE-04 — Three PFR primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [ANALYSE-06 — French version](ANALYSE-06b-Sensibilite-2026-Lean.ipynb) | [Lean-12b — Huang's Sensitivity Theorem](../Lean-12b-Lean-Sensitivity-Theorem.ipynb) |" ] }, { diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md index 4ac3e1cfac4..fd7e7306772 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md @@ -14,7 +14,7 @@ La série principale garde son tutoriel (numéros 1 à 14) ; le présent dossier | [ANALYSE-03-PFR-Lean](ANALYSE-03-PFR-Lean.ipynb) | La conjecture PFR (polynomial Freiman–Ruzsa, ZMod 2) : méthode entropique de la preuve `teorth/pfr` — énoncé combinatoire, illustrations cosets dans F₂³, `#check` réels et axiomes du lac compilé | 45 min | | [ANALYSE-04-PFR-Primitives-Python](ANALYSE-04-PFR-Primitives-Python.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de ANALYSE-03 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min | | [ANALYSE-05-KLS-Lean-Python](ANALYSE-05-KLS-Lean-Python.ipynb) | La conjecture KLS démontrée (Bizeul–Klartag–Lehec, arXiv:2610.05474) : énoncé (Théorème 1.1), chaîne de la preuve en cinq maillons (thin-shell, germe quadratique, localisation stochastique, suspension, critère de Song–Zhang), lac local `kls_lean` — audit Mathlib au pin, six définitions, deux théorèmes prouvés (0 sorry, `#print axioms` propre) — thin-shell en Monte-Carlo avec saturation exacte à 8n par l'exponentielle produit, banc 1-lipschitzien minorant `poincareConstant` | 45 min | -| [ANALYSE-06-Sensibilite-2026-Lean](ANALYSE-06-Sensibilite-2026-Lean.ipynb) | La combinatoire booléenne 2026 d'openai/math (familles 127/132/186/192) lue depuis notre lac `Sensitivity` : Huang prouvé chez nous (`#check`/`#print axioms`), énoncés 2026 cités avec leur statut épistémique, et nos séparations sensibilité/sensibilité de bloc du module `Sensitivity.Separations`, prouvées et calculées (`#eval` natif, Pli 2 d'Origami #19898) ; jumeau anglais à code byte-identique : [ANALYSE-06-...-_en](ANALYSE-06-Sensibilite-2026-Lean_en.ipynb) | 35 min | +| [ANALYSE-06b-Sensibilite-2026-Lean](ANALYSE-06b-Sensibilite-2026-Lean.ipynb) | La combinatoire booléenne 2026 d'openai/math (familles 127/132/186/192) lue depuis notre lac `Sensitivity` : Huang prouvé chez nous (`#check`/`#print axioms`), énoncés 2026 cités avec leur statut épistémique, et nos séparations sensibilité/sensibilité de bloc du module `Sensitivity.Separations`, prouvées et calculées (`#eval` natif, Pli 2 d'Origami #19898) ; jumeau anglais à code byte-identique : [ANALYSE-06b-...-_en](ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb) | 35 min | | [ANALYSE-07-Percolation-Critique](ANALYSE-07-Percolation-Critique.ipynb) | Percolation critique et Ising sur l'arbre d-régulier — pli 3 de la digestion Origami (#19898) : les inégalités de Harris–Kleitman `#check`ées dans notre lac `percolation_lean`, les familles 2026 **213** (criticité Benjamini–Schramm) et **236** (seuil factor-of-IID de l'Ising sur l'arbre) citées avec leur statut, et deux calculs nôtres **exacts** — la probabilité critique p_c = 1/(d-1) par Galton–Watson (point fixe non trivial 4/9, vérifiable à la main) et l'écart entre seuil de reconstruction et seuil d'aimantation ; jumeau anglais à code byte-identique : [ANALYSE-07-...-_en](ANALYSE-07-Percolation-Critique_en.ipynb) | 40 min | | [ANALYSE-08-Ramsey-VdW](ANALYSE-08-Ramsey-VdW.ipynb) | Ramsey et van der Waerden par épuisement : R(3,3)=6 et W(2,3)=9 prouvés par énumération exhaustive (survivantes 18→12→0 côté graphes, 6→0 côté progressions), le mur 2^153 où le geste meurt, et le pont probabiliste d'Erdős (#19960, pli 4 Origami #19898) | 30 min | | [ANALYSE-09-Tuilage-Aperiodique](ANALYSE-09-Tuilage-Aperiodique.ipynb) | Famille 155 du corpus `openai/math` : un carreau de ℤ³ qui pave sans périodicité totale (contre-exemple de dimension trois). Le carnet ramène le pavage par translations à la couverture exacte que le dépôt formalise déjà (`sudoku_lean`, `ExactCover.IsExactCover`), puis mesure quatre expériences avec deux organes déterministes — backtracking borné `place_tiles` et rang de période `period_rank` (élimination de Gauss exacte sur ℚ) — la leçon transverse étant que la demi-fenêtre cache toute période plus longue qu'elle ; jumeau anglais à code byte-identique : [ANALYSE-09-...-_en](ANALYSE-09-Tuilage-Aperiodique_en.ipynb) | 30 min | diff --git a/_quarto.yml b/_quarto.yml index 78dd7fbc543..2f63d283888 100644 --- a/_quarto.yml +++ b/_quarto.yml @@ -2130,8 +2130,8 @@ project: - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en.ipynb" - - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb" - - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique_en.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-08-Ramsey-VdW.ipynb" diff --git a/docs/curriculum/ia-symbolique.md b/docs/curriculum/ia-symbolique.md index d2287bc9ea2..669dfcc7595 100644 --- a/docs/curriculum/ia-symbolique.md +++ b/docs/curriculum/ia-symbolique.md @@ -79,8 +79,8 @@ Preuves formelles en Lean 4, logique probabiliste avec Tweety, web sémantique, | 5 | [ANALYSE-05 : La conjecture KLS démontrée — digérer…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb) | BETA | Non | | 6 | [ANALYSE-06 : Sensibilité 2026 — Huang, le décideur qui…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb) | BETA | Non | | 7 | [ANALYSE-06: Sensitivity 2026 — Huang, the refuting…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en.ipynb) | BETA | Non | -| 8 | [ANALYSE-06 — Sensibilité 2026 : notre lac face aux…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb) | BETA | Non | -| 9 | [ANALYSE-06 — Sensitivity 2026: our lake facing the…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb) | BETA | Non | +| 8 | [ANALYSE-06 — Sensibilité 2026 : notre lac face aux…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb) | BETA | Non | +| 9 | [ANALYSE-06 — Sensitivity 2026: our lake facing the…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb) | BETA | Non | | 10 | [ANALYSE-07 — Percolation critique et Ising sur l'arbre…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique.ipynb) | BETA | Non | | 11 | [ANALYSE-07 — Critical percolation and Ising on the tree…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique_en.ipynb) | BETA | Non | | 12 | [ANALYSE-08 : Ramsey et van der Waerden — l'énumération…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-08-Ramsey-VdW.ipynb) | BETA | Non | diff --git a/scripts/notebook_tools/pedagogy_density_baseline.json b/scripts/notebook_tools/pedagogy_density_baseline.json index d563691fcf7..2369ee8a910 100644 --- a/scripts/notebook_tools/pedagogy_density_baseline.json +++ b/scripts/notebook_tools/pedagogy_density_baseline.json @@ -1127,8 +1127,8 @@ "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb": 2115.667, "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb": 2157.6, "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en.ipynb": 2110.8, - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb": 2414.5, - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb": 2401.625, + "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb": 2414.5, + "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb": 2401.625, "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique.ipynb": 1996.625, "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique_en.ipynb": 2016.0, "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-08-Ramsey-VdW.ipynb": 865.273, diff --git a/translations/translation_golden_set.json b/translations/translation_golden_set.json index 56b8e3e7d32..6da5645b90f 100644 --- a/translations/translation_golden_set.json +++ b/translations/translation_golden_set.json @@ -1808,8 +1808,8 @@ }, { "kind": "notebook", - "fr": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb", - "en": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb", + "fr": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb", + "en": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb", "sha1_fr": "eaf45cfea264a611cbdb5c523da69353249b3477", "sha1_en": "aa7ff661aae1abef4d08ba674296ca350a741fb6", "sources_sha1_fr": "1063a3296c8ff96e92b6c335b36d5fa920aa50cc", From 3d26f31cb2469d773d8bb431cd6fac9d8abd79f7 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 27 Oct 2026 15:47:20 +0100 Subject: [PATCH 3/5] Fix(#22649): dernieres references au nom 06 -- lien suite-de-serie du 04, intro du jumeau EN metadata.papermill du 04 reduit au basename par le hook auto (chemins absolus herites de la machine d'execution) ; paths des deux 06b laisses tels quels (basenames, trace du nom a l'execution). Zero reference fonctionnelle restante hors catalogue genere. Co-Authored-By: Claude Sonnet 5.5 --- .../Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb | 8 ++++---- .../ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb index 15dcb1b5556..128d88e11ae 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb @@ -60,7 +60,7 @@ "3. Primitive 3 — La fonctionnelle τ : patron de descente, **test de limite**.\n", "4. Conclusion — lien vers ANALYSE-03 et le lac `pfr`.\n", "\n", - "**Suite de la sous-série** : [ANALYSE-06 — Sensibilité 2026 (notre lac face aux familles d'openai/math)](ANALYSE-06-Sensibilite-2026-Lean.ipynb)\n", + "**Suite de la sous-série** : [ANALYSE-06 — Sensibilité 2026 (notre lac face aux familles d'openai/math)](ANALYSE-06b-Sensibilite-2026-Lean.ipynb)\n", "**Suite de la sous-série** : [ANALYSE-07 — Percolation critique (notre lac face aux familles 2026 213/236)](ANALYSE-07-Percolation-Critique.ipynb)" ] }, @@ -1647,8 +1647,8 @@ "end_time": "2026-10-23T22:00:28.041614+00:00", "environment_variables": {}, "exception": null, - "input_path": "D:\\Dev\\CoursIA-2-22206-analyse\\MyIA.AI.Notebooks\\SymbolicAI\\Lean\\ANALYSE\\ANALYSE-04-PFR-Primitives-Python.ipynb", - "output_path": "D:/Dev/CoursIA-2-22206-analyse/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb", + "input_path": "ANALYSE-04-PFR-Primitives-Python.ipynb", + "output_path": "ANALYSE-04-PFR-Primitives-Python.ipynb", "parameters": {}, "start_time": "2026-10-23T22:00:21.892909+00:00", "version": "2.6.0" @@ -1662,4 +1662,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb index 9f74604a2c1..d6adc21b0aa 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb @@ -18,7 +18,7 @@ "\n", "**ANALYSE** sub-series (#17545 grading) — Fold 2 of the **Origami** digestion (#19898): the Boolean-combinatorics results published by `openai/math` in 2026, read from **our** `Sensitivity` lake — the port of Huang's theorem (2019).\n", "\n", - "This notebook is a **native** companion: Lean 4 kernel under WSL, every `#check` queries the actually-compiled lake, every `#eval` really computes. Numerical computation is done **natively in Lean** — no Python fallback; the file-name suffix follows the series naming convention. This is the English twin of the French notebook `ANALYSE-06-Sensibilite-2026-Lean.ipynb`; it renders the **same** computation in English: the code cells are byte-identical to the French side (the repository's twin-parity invariant), while the lake's English siblings (`*_en`, i18n convention #4980) carry the English docstrings.\n", + "This notebook is a **native** companion: Lean 4 kernel under WSL, every `#check` queries the actually-compiled lake, every `#eval` really computes. Numerical computation is done **natively in Lean** — no Python fallback; the file-name suffix follows the series naming convention. This is the English twin of the French notebook `ANALYSE-06b-Sensibilite-2026-Lean.ipynb`; it renders the **same** computation in English: the code cells are byte-identical to the French side (the repository's twin-parity invariant), while the lake's English siblings (`*_en`, i18n convention #4980) carry the English docstrings.\n", "\n", "**Prerequisites**: the main series tutorial (notebooks 1 to 6). Reading [Lean-12b — Huang's Sensitivity Theorem](../Lean-12b-Lean-Sensitivity-Theorem.ipynb) makes section 1 more comfortable, but is not required: we recall what we need.\n", "\n", From ac9bdcaffbafcc059635786141bdc570e28341c6 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 27 Oct 2026 15:52:00 +0100 Subject: [PATCH 4/5] Fix(#22649): retirer les edits manuels des fichiers possedes par le cron catalogue Quarto render list, golden set de traduction et page parcours ia-symbolique sont regeneres et commites par catalog-cron.yml vers chore/catalog-refresh-pending (arbitrage #19901, docstring build_golden_set.py post-#22216 : une branche de contenu ne les regenere pas). La PR ne porte que les registres bloquants : README, liens croises cellule 0, cles pedagogy_density_baseline. Co-Authored-By: Claude Sonnet 5.5 --- _quarto.yml | 4 ++-- docs/curriculum/ia-symbolique.md | 4 ++-- translations/translation_golden_set.json | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/_quarto.yml b/_quarto.yml index 2f63d283888..78dd7fbc543 100644 --- a/_quarto.yml +++ b/_quarto.yml @@ -2130,8 +2130,8 @@ project: - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en.ipynb" - - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb" - - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique_en.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-08-Ramsey-VdW.ipynb" diff --git a/docs/curriculum/ia-symbolique.md b/docs/curriculum/ia-symbolique.md index 669dfcc7595..d2287bc9ea2 100644 --- a/docs/curriculum/ia-symbolique.md +++ b/docs/curriculum/ia-symbolique.md @@ -79,8 +79,8 @@ Preuves formelles en Lean 4, logique probabiliste avec Tweety, web sémantique, | 5 | [ANALYSE-05 : La conjecture KLS démontrée — digérer…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb) | BETA | Non | | 6 | [ANALYSE-06 : Sensibilité 2026 — Huang, le décideur qui…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb) | BETA | Non | | 7 | [ANALYSE-06: Sensitivity 2026 — Huang, the refuting…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en.ipynb) | BETA | Non | -| 8 | [ANALYSE-06 — Sensibilité 2026 : notre lac face aux…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb) | BETA | Non | -| 9 | [ANALYSE-06 — Sensitivity 2026: our lake facing the…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb) | BETA | Non | +| 8 | [ANALYSE-06 — Sensibilité 2026 : notre lac face aux…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb) | BETA | Non | +| 9 | [ANALYSE-06 — Sensitivity 2026: our lake facing the…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb) | BETA | Non | | 10 | [ANALYSE-07 — Percolation critique et Ising sur l'arbre…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique.ipynb) | BETA | Non | | 11 | [ANALYSE-07 — Critical percolation and Ising on the tree…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique_en.ipynb) | BETA | Non | | 12 | [ANALYSE-08 : Ramsey et van der Waerden — l'énumération…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-08-Ramsey-VdW.ipynb) | BETA | Non | diff --git a/translations/translation_golden_set.json b/translations/translation_golden_set.json index 6da5645b90f..56b8e3e7d32 100644 --- a/translations/translation_golden_set.json +++ b/translations/translation_golden_set.json @@ -1808,8 +1808,8 @@ }, { "kind": "notebook", - "fr": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb", - "en": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb", + "fr": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb", + "en": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb", "sha1_fr": "eaf45cfea264a611cbdb5c523da69353249b3477", "sha1_en": "aa7ff661aae1abef4d08ba674296ca350a741fb6", "sources_sha1_fr": "1063a3296c8ff96e92b6c335b36d5fa920aa50cc", From e5c3d1df4de03f0bafd973ac08c8c748f3ac0369 Mon Sep 17 00:00:00 2001 From: jsboige Date: Thu, 29 Oct 2026 17:33:11 +0100 Subject: [PATCH 5/5] Fix(analyse,#22932): le golden set de traduction suit le renommage du companion Lean Le registre de traduction pointait encore vers l'ancien nom du companion renomme en ANALYSE-06b : la chaine de traduction lisait un fichier qui n'existe plus. Les deux entrees (fr et en) portent desormais le nouveau chemin ; les entrees du companion Python (ANALYSE-06-...-Lean-Python) sont inchangees. Les quatre chemins ANALYSE-06* du registre existent sur disque apres edition ; le diff est de deux lignes. Co-Authored-By: Claude Sonnet 5.5 --- translations/translation_golden_set.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/translations/translation_golden_set.json b/translations/translation_golden_set.json index 56b8e3e7d32..6da5645b90f 100644 --- a/translations/translation_golden_set.json +++ b/translations/translation_golden_set.json @@ -1808,8 +1808,8 @@ }, { "kind": "notebook", - "fr": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb", - "en": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb", + "fr": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb", + "en": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb", "sha1_fr": "eaf45cfea264a611cbdb5c523da69353249b3477", "sha1_en": "aa7ff661aae1abef4d08ba674296ca350a741fb6", "sources_sha1_fr": "1063a3296c8ff96e92b6c335b36d5fa920aa50cc",