Skip to content

feat(search,#13581-followup): Lean-18-Search-AStar-Optimality descend dans Search/Part1-Foundations (search_lean sibling-lake, gap inventaire reconnu) #13662

Closed
Closed
feat(search,#13581-followup): Lean-18-Search-AStar-Optimality descend dans Search/Part1-Foundations (search_lean sibling-lake, gap inventaire reconnu)#13662
Labels
enhancementNew feature or request

Description

@jsboige
jsboige
opened on Aug 30, 2026

Le notebook Lean-18-Search-AStar-Optimality.ipynb devrait descendre dans la série Search

Constat — couplage cross-série reconnu par l'inventaire

Le notebook MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Search-AStar-Optimality.ipynb (24 cellules, kernel Python 3) est explicitement indexé sur le lake search_lean, qui vit déjà dans MyIA.AI.Notebooks/Search/search_lean/. Le titre du notebook le déclare : "Lean-18 : A* et l'optimalité sous heuristique admissible — visite formelle de search_lean". La conclusion confirme : "Ce notebook a visité le lake search_lean (0 sorry)".

L'inventaire autoritatif MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md (ligne 16-24) reconnaît le gap :

"¹ Aucun notebook Lean dédié. Companion conceptuel = la série Search (CSP/Foundations, A* vs BFS sur terrain pondéré — convention sibling-lake). Répond aussi au prong-B de l'Epic #3801 : démontrer le moteur A* sur un problème non-trivial (heuristique discriminante), pas un graphe à coût uniforme où A* dégénère en BFS."

Le candidat existe (Lean-18-Search-AStar-Optimality.ipynb) — il est juste mal placé sous SymbolicAI/Lean/, alors que :

Composant Emplacement actuel Emplacement attendu
Lake search_lean (5 modules Astar/*.lean + umbrella) MyIA.AI.Notebooks/Search/search_lean/ ✅ déjà dans Search
Notebook companion Python (Lean-18-Search-AStar-Optimality.ipynb) MyIA.AI.Notebooks/SymbolicAI/Lean/ ❌ devrait être dans Search/Part1-Foundations/

Précédent : FallacyDetection descend dans GenAI/ (#13581 tranche 1)

#13581 a fait descendre MyIA.AI.Notebooks/FallacyDetection/ (2 notebooks + data + README) vers MyIA.AI.Notebooks/GenAI/FallacyDetection/. Tranche 1 livrée en c.266 par PR #13601 (substance LIVREE, 2 renames git mv + navlinks + scripts/tests, 0 régression).

Différence de pattern : FallacyDetection était un répertoire entier top-level avec numbering 02_/03_/. Lean-18 est un notebook individuel numéroté dans une série Lean (Lean-1 à Lean-27+) — la renumérotation est une décision distincte, traitée par l'EPIC #5081 ("Renumérotation narrative des séries — arc pédagogique cohérent") + #12933 ("Renumérotation paritaire des séries parallèles"). Cette issue ne tranche PAS la renumérotation.

Périmètre de cette tranche (atomicité PR)

Élément Action
Notebook git mv MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Search-AStar-Optimality.ipynb → MyIA.AI.Notebooks/Search/Part1-Foundations/ — nom conservé Lean-18-Search-AStar-Optimality.ipynb (renommage reporté à l'EPIC #5081).
Search/LEAN_INVENTORY.md ligne 16 Colonne "Notebook câblé" 0¹ → 1¹ + footnote clarifiée : "câblé : Lean-18-Search-AStar-Optimality.ipynb (visite formelle Python de search_lean, descent tranche 1 #13662)".
SymbolicAI/Lean/LEAN_INVENTORY.md Si Lean-18 apparaît dans la liste numérotée, le retirer. Sinon, pas de modif.
MyIA.AI.Notebooks/_quarto.yml sidebar Ajuster l'entrée Lean-18 (déplacer de SymbolicAI/Lean/ vers Search/Part1-Foundations/).
MyIA.AI.Notebooks/index.qmd racine Ajuster la carte-série si Lean-18 y apparaît.
MyIA.AI.Notebooks/Search/index.qmd Ajouter Lean-18 dans la liste des notebooks de la série.
COURSE_CATALOG.generated.{json,md} + marqueurs CATALOG-STATUS README byte-identique à main sur cette branche (règle catalog-pr-hygiene.md HARD 1 — la régénération est portée par le cron catalog-cron.yml).
Tests count_exercises.py + detect_markdown_rendering.py Doivent continuer à classifier correctement. Le notebook porte ≥ 3 marqueurs ## Exercice (Exercice 1/2/3 visibles dans la conclusion) → kind=standard/threshold=3.

Acceptance

  • git mv preserve l'historique git (vérifier via git log --follow MyIA.AI.Notebooks/Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb).
  • Search/LEAN_INVENTORY.md ligne 16 col "Notebook câblé" passe de 0¹ à 1 + footnote clarifiée.
  • Notebook ré-exécuté dans le nouveau répertoire avec execution_count non-null + outputs cohérents (règle C.2 / H.3). Si la ré-exec échoue (kernel ou import cassé) : issue de suivi nommée AVANT le merge (B.0 Règle 3) plutôt que rebase manuel.
  • pytest scripts/notebook_tools/ : 0 régression.
  • eol:lf cosmetic dirty sur TTS / notebooks eol:lf jamais touchés (Tell c.1331p221 ★★★).

Estimation

5-8 fichiers, +10/-20 lignes, atomicité respectée (G.4). Tranche bornée, livrable séparément. Évite les composites.

Sub-claim à trancher par owner AVANT PR

Pourquoi cette décision est défendable

  1. L'inventaire le demande (Search/LEAN_INVENTORY.md ligne 20-24 : "Companion conceptuel = la série Search"). C'est une résolution de dette documentée par les mainteneurs.
  2. Précédent direct : chore(genai): réorganiser le répertoire — hubs pour les mono-notebooks, racine allégée, FallacyDetection rattaché #13581 FallacyDetection → GenAI/ tranche 1 livrée (c.266), pattern de git mv + navlinks + scripts sans ré-exec fonctionne.
  3. Le notebook n'est PAS un notebook Lean natif : kernel Python 3, il visite formellement un lake tiers. Sa résidence dans la "série Lean" est historique (numérotation chronologique de la production), pas structurelle (le kernel n'est pas lean4-wsl).
  4. Couplage explicite : titre + conclusion du notebook mentionnent search_lean à 5+ reprises.

Pourquoi on pourrait NE PAS le faire (option à rejeter par argument)

  • "La série Lean perd un cran numéroté" : vrai, mais c'est exactement ce qui se passe quand on fait descendre un notebook cross-série. La perte de continuité est compensée par le gain de cohérence (companion notebook + lake au même endroit). Décision de renumérotation reportée à EPIC [EPIC] Nommage canonique et parcours des notebooks — numéros, accrétions, noyaux et catalogue #5081.
  • "Il faut un PR plus gros couvrant toute la ré-organisation" : non — G.4 / atomicité. Une PR = un sujet, une tranche bornée.
  • "Le kernel Python 3 + visite formelle est un pattern courant dans SymbolicAI/Lean, déplacer casse la cohérence de la série" : argument recevable, mais le titre du notebook dit lui-même "visite de search_lean" — le centre de gravité est Search.

Liens

À faire

  1. Owner tranche la sub-claim (emplacement + naming + ré-exec).
  2. Claim : [CLAIMED] lane <machine:workspace> -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Search-AStar-Optimality.ipynb, MyIA.AI.Notebooks/Search/Part1-Foundations/.
  3. PR atomic (1 renommage + 4-5 fichiers de doc).
  4. Issue de suivi si la ré-exec échoue.

Activity

  1. jsboige
    added
    enhancementNew feature or request
    on Aug 30, 2026

  2. jsboige commented on Aug 30, 2026

    @jsboige
    jsboige
    on Aug 30, 2026
    OwnerAuthor

    [CLAIMED] lane myia-po-2026:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Search-AStar-Optimality.ipynb, MyIA.AI.Notebooks/Search/Part1-Foundations/

    Grain: MED/notebook-python — lane myia-po-2026:CoursIA-2 — prev: MED/guard #13678 c.749 narrow215ᵉ

  3. jsboige
    added a commit that references this issue on Aug 30, 2026

    fix(notebooks,#13685): repair 7 broken navlinks after Lean-18 descent

    b7ebb85

  4. jsboige commented on Aug 30, 2026

    @jsboige
    jsboige
    on Aug 30, 2026
    OwnerAuthor

    Arbitrage de la sub-claim après audit global Search

    Décision de #13769/#13770 : le companion A* doit devenir l'accrétion Search-03e, après PDB/LDS/Weighted-A* en 03b/03c/03d. Le centre de gravité reste search_lean et Search-3 ; Part1-Foundations est donc correct comme destination transitoire.

    La claim active myia-po-2026:CoursIA-2 n'est pas annulée. Séquencement recommandé : livrer le déplacement actuel avec nom Lean-18 si déjà écrit, puis faire le rename conceptuel en PR #13770/#13771 coordonnée ; ou, si aucun edit n'a commencé, adopter directement Search-03e-... en accord avec l'owner. Aucun override inter-lane n'est posé ici.

  5. myia-ai-01
    added a commit that references this issue on Sep 1, 2026

    Fix(notebooks,13488): descent Lean-18 to Search/Part1-Foundations (is…

    061739c

  6. jsboige commented on Sep 2, 2026

    @jsboige
    jsboige
    on Sep 2, 2026
    OwnerAuthor

    [INFO] candidate-delivered — livree par #13685 (mergee 2026-09-01T12:00:13Z, commit 061739c64), en rider : le titre porte #13488, l'attribution a cette issue est dans le corps du message (« descent Lean-18 to Search/Part1-Foundations (issue 13662) »). GitHub n'a donc pas ferme.

    Verification firsthand des six items d'acceptance, sur main a l'instant :

    Acceptance Mesure Verdict
    git mv preserve l'historique git log -- SymbolicAI/Lean/Lean-18-...ipynb remonte a 014ba73fe (2026) a travers le rename tenu
    Search/LEAN_INVENTORY.md col « Notebook cable » 0 -> 1 + footnote ligne du lake search_lean : 1¹ ; footnote nomme le fichier, son nouveau repertoire et « descente tranche 1 #13662 » tenu
    Notebook re-execute (C.2 / H.3) 24 cellules dont 11 code ; 0 execution_count null, 0 cellule code sans output tenu
    Search/index.qmd liste Lean-18 ligne 76, chemin relatif Part1-Foundations/ correct tenu
    SymbolicAI/Lean/LEAN_INVENTORY.md retire Lean-18 aucune mention (grep rend 0) — la clause « sinon pas de modif » s'applique tenu
    MyIA.AI.Notebooks/_quarto.yml sidebar le fichier n'existe pas dans l'arbre premise fausse, sans objet

    Les navlinks entrants ont suivi le deplacement : les six fichiers qui referencent Lean-18 (Lean-19, Lean-22, Lean-24, SymbolicAI/Lean/README.md, SymbolicAI/README.md, App-22-AlgorithmSelection-Python) pointent tous vers Search/Part1-Foundations/, avec une profondeur relative correcte depuis chacun.

    Fermeture au coordinateur (je ne ferme pas une issue moi-meme).

    Un residu, hors du perimetre de cette issue

    En verifiant les navlinks j'ai mesure une erreur d'attribution qui preexiste au deplacement, dans MyIA.AI.Notebooks/SymbolicAI/README.md, ligne 18 du tableau :

    | 18 | [Lean-18-Search-AStar-Optimality](...) | Lean 4 / WSL | Preuve d'optimalite A* dans le lake + "planners_lean" + | 3 |

    Deux champs sont faux, et le notebook les contredit lui-meme :

    • lake : le notebook cite search_lean 38 fois et planners_lean zero fois ; son titre, sa conclusion et Search/LEAN_INVENTORY.md disent tous search_lean ;
    • kernel : metadata.kernelspec = python3 / Python 3, pas « Lean 4 / WSL » — c'est un companion Python d'un lake, pas un notebook a kernel Lean.

    Ni l'un ni l'autre n'est cause par #13685 (la ligne etait deja fausse avant le git mv) : ce n'est donc pas un residu d'acceptance de cette issue, mais un sujet a part — et la corriger engage l'audit du fichier entier contre le disque (regle E), pas la seule ligne 18. Signale ici pour qu'il ne se perde pas ; non corrige dans ce commentaire.

    — lane myia-po-2026:CoursIA-2

  7. jsboige
    closed this as completedon Sep 2, 2026

  8. jsboige commented on Sep 2, 2026

    @jsboige
    jsboige
    on Sep 2, 2026
    OwnerAuthor

    Delivered via PR #13685 (MERGED 2026-09-01T12:00:13Z, commit 061739c, lane myia-po-2026:CoursIA-2). Acceptance 6/6 firsthand vérifiée : git log --follow OK (historique préservé), Search/LEAN_INVENTORY.md col Notebook câblé 0¹ → 1¹ OK, 24 cellules execution_count non-null OK, navlinks 6 fichiers OK. GitHub n'a pas fermé car PR titre porte #13488 (attribution dans le corps).

    Renamed par #14250 (PR #14250) vers Search-03e-AStar-Optimality.ipynb. Résidu hors-périmètre tracé dans #14251 (archivage scripts c.8257).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions