From 62117efb347bc409397abd51a4dae3528b850390 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 1 Sep 2026 00:01:43 +0200 Subject: [PATCH] fix(2.8c,#13862): corrige la note de substitution -- hoeffding/pac_finite_class_bound cites mais non #check MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Issue #13862 (ai-01) : la cellule markdown "Comment verifier sur main ?" de 2.8c nommait hoeffding_concentration (Hoeffding.lean) et pac_finite_class_bound (PacFiniteBound.lean) comme verifies par les #check de 2.8b. Inventaire exhaustif des directives Lean executees dans 2.8b a la tete de #13717 : aucun #check @PacLearning.hoeffding_concentration ni #check @PacLearning.pac_finite_class_bound. Les theoremes existent dans le lake (Hoeffding.lean:318, PacFiniteBound.lean:377) mais ne sont pas interroges nativement par 2.8b ; ils sont atteints par les Sections 5 (Monte-Carlo sur hoeffding_upper_tail) et 8 (#eval d'une version jouable de pac_finite_class_bound) du meme 2.8b, ce qui prouve la disponibilite de la chaine computationnelle mais pas la signature native du theoreme. Voie (a) de l'issue (remede minimum) : corriger la note de 2.8c pour nommer ce que 2.8b verifie reellement -- PacLearning.uniform_concentration, PacLearning.sampleWeight_sum_one, PacLearning.sampleWeight_nonneg (3 modules noirs de Sample.lean et UniformConcentration.lean interroges nativement par #check + #print axioms, voir Section 10 de 2.8b) -- et ajouter une note explicative (issue #13862) qui distingue "existence dans le lake" et "interrogation par #check". Voie (b) (preferee : ajouter #check @PacLearning.hoeffding_concentration + #check @PacLearning.pac_finite_class_bound + #print axioms dans 2.8b puis re-executer sous kernel lean4-wsl) n'a pas ete tentee dans cette PR : le lake learning_theory_lean n'est pas compile localement (pas de .lake/build dans le repo), le kernel lean4-wsl ne peut pas charger PacLearning.* depuis un worktree frais. Ai-01 ou po-2023 (machine avec lake compile) pourra reprendre la voie (b) dans une PR follow-up -- voir issue #13862 acceptance pour le plan exact. H.3 / C.1 / C.2 preserves : 0 cellule code touchee, 15/15 cells intactes, outputs inchanges (markdown only, exception C.2). Validation pre-commit PASS (5 cells, coursia-ml-training kernel). Grain: LIGHT/lean - lane myia-po-2026:CoursIA - prev: tooling #13871 cycle 32. paths: MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb Closes #13862 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- .../02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb b/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb index dc1ee1b499..b1bd30a530 100644 --- a/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb +++ b/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb @@ -24,7 +24,7 @@ "\n", "**Compagnon formel** : `MyIA.AI.Notebooks/ML/learning_theory_lean/`\n", "\n", - "---\n", + "***\n", "\n", "## Concept\n", "\n", @@ -525,11 +525,11 @@ "\n", "Les vérifications mécaniques étaient historiquement dans ce notebook : existence des théorèmes cités et `sorry = 0` dans le lake. Elles sont désormais portées par les instruments suivants :\n", "\n", - "- **Existence des théorèmes** : vérifiée par les `#check` explicites dans [2.8d](2.8d-Lean-Novikoff-Convergence.ipynb) (`PerceptronRun.novikoff_mistake_bound`, `tightnessRun_saturates`, ...) et [2.8b](2.8b-Theorie-PAC-Lean.ipynb) (`hoeffding_concentration`, `pac_finite_class_bound`, ...).\n", + "- **Existence des théorèmes cités dans ce notebook** : vérifiée par les `#check` explicites dans [2.8d](2.8d-Lean-Novikoff-Convergence.ipynb) (`PerceptronRun.novikoff_mistake_bound`, `tightnessRun_saturates`, ...) et [2.8b](2.8b-Theorie-PAC-Lean.ipynb) (`PacLearning.uniform_concentration`, `PacLearning.sampleWeight_sum_one`, `PacLearning.sampleWeight_nonneg`). Ces trois modules sont interrogés nativement par `#check` (signature) + `#print axioms` (certificat) — voir Section 10 de 2.8b. **Note (issue #13862)** : les théorèmes `hoeffding_concentration` (Hoeffding.lean) et `pac_finite_class_bound` (PacFiniteBound.lean) **existent** dans le lake mais ne sont **pas interrogés** par les cellules actuelles de 2.8b ; ils sont atteints par les Sections 5 (Monte-Carlo sur `hoeffding_upper_tail`) et 8 (`#eval` d'une version jouable de `pac_finite_class_bound`) du même 2.8b, ce qui prouve la **disponibilité de la chaîne computationnelle** mais ne rend pas la signature native du théorème via `#check`.\n", "- **Zéro `sorry` réel dans le lake** : porté par l'organe `python scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`), mesuré en CI par le job `proof-integrity`. **Pas de `grep -c sorry`** : il sur-compte la prose (docstrings, commentaires).\n", "- **Pas de `native_decide` / `sorryAx` dans le chemin des théorèmes cités** : porté par le job CI `lean-axiom.yml` (catégorie `forbidden`, pas seulement `sorry`).\n", "\n", - "Pour une **revue complète** du triplet BORNE/TÉMOIN/CONCENTRATION sur le lake courant, suivre les **Voir aussi** internes de chaque sibling.\n" + "Pour une **revue complète** du triplet BORNE/TÉMOIN/CONCENTRATION sur le lake courant, suivre les **Voir aussi** internes de chaque sibling." ] } ],