docs(curriculum,#15806): parcours narratif « IA Symbolique et Formalisation » (pilote 2, EPIC #13844)

[jsboige]

Ce que cette PR livre

docs/curriculum/symbolic-formalization.md — pilote 2 des parcours narratifs (EPIC #13844 Phase 2), « IA Symbolique et Formalisation (~20 h) ». Un seul fichier neuf ; les 5 pages catalogue générées ne sont pas touchées (le nom n'est aucun des 5 ids du générateur, convention posée par le pilote 1 genai-rush.md).

Les 5 critères d'acceptance #13844

1. Public visé — une phrase (§ en-tête).
2. Prérequis vérifiables ~10 min — table 5 lignes (Python, Jupyter, disque, WSL2+elan bloc 4 seulement, aucune clé API) + clause explicite « suppose / ne suppose pas ».
3. Durée défendable — table par bloc, chaque étape porte sa duree_estimee du catalogue. Colonne vertébrale mesurée : 16 h 15 (Tweety 6 h 00 / Z3 3 h 45 / Planners 4 h 45 / Lean 1 h 45) ; fenêtre ~20 h = colonne vertébrale + rampe NNG 3-4 h chiffrée par LEAN_PREREQUISITES lui-même. Le « ~6 mois » de l'inventaire est explicité comme espacement (~2 étapes/semaine), pas comme durée.
4. Sortie concrète — 4 puces d'exécutions réelles, dont « trois preuves Lean rejouées ».
5. Liste ordonnée — 29 étapes, chacune avec apporte → suppose.

Anti-patterns refusés en review → traités

• Pas de breadcrumb sans sémantique (aucun).
• Pas de liste sans prérequis (chaque étape a sa colonne « Suppose » + clause générale).
• Pas de durée fantôme (double compte chiffré, sources citées).

Fil pédagogique

« Du symbole à la preuve » : un même objet traversé deux fois — les companions Lean du bloc 4 (Tweety-5b prouve le Dung de l'étape 5 ; Planners-5b formalise le h-add de l'étape 23 ; Tweety-5d ponte Z3→Lean vers l'étape 15) certifient les livrables des blocs 1-3.

Sources recollées (critère EPIC), pas réécrites

Inventaire Phase 0 entrées #8-14 + #35 : README SymbolicAI (ordre de lecture), README Tweety (phases), LEAN_PREREQUISITES (rampe 3 niveaux), READMEs SemanticWeb (3 profils) / SmartContracts (table « Quel parcours choisir », parent pas les 6 sous-parcours — avertissement #111) / SymbolicLearning / SocialChoice cités en portes de sortie.

Validation

• python scripts/check_docs_links.py : 723 fichiers, 7024 liens, 0 cassé (les 43 liens du nouveau fichier résolvent, vérifiés aussi par extraction locale).
• Catalogue byte-identique à main (aucun fichier catalogue touché).
• Markdown-only : aucune cellule de notebook modifiée → pas de re-exécution due (exception C.2).

Grain: MED/docs — lane myia-po-2023:CoursIA — prev: MED/tooling #15919

🤖 Generated with Claude Code

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2023:CoursIA a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #15850 (MED/guard, merge a 2026-09-13T01:04:08Z), #15883 (LIGHT/docs, merge a 2026-09-13T03:07:30Z), #15881 (MED/docs, merge a 2026-09-13T03:08:12Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues (guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2023:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-13) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=3 cap=2)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=3 cap=2)

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[clusterManager-Myia]

VERDICT: LGTM (vérifié: 41/41 liens relatifs résolus contre le tree main + sommes de durées recalculées depuis le diff + non-collision ids générateur)

[Hermes] — #15921, première review sur ce head 9f7af494 (opener jsboige).

Vérifications firsthand :

• Liens : les 41 cibles relatives (../../MyIA.AI.Notebooks/...) résolues une à une contre git/trees/main?recursive=1 — 0 cassé, conforme au check_docs_links.py 0 lien cassé du body.
• Durées : les 29 étapes extraites du diff somment à 975 min = 16 h 15, et chaque sous-total par bloc tombe exactement sur le claim de la table (1-10 Tweety 360 min = 6 h 00 ; 11-18 Z3 225 min = 3 h 45 ; 19-25 Planners 285 min = 4 h 45 ; 26-29 Lean 105 min = 1 h 45). La colonne vertébrale est défendable, pas une durée fantôme.
• Fail-closed #15882 : symbolic-formalization n'est aucun des 5 ids du PARCOURS du générateur (ia-classique, ia-symbolique, genai, trading, recherche) — la page n'est pas régénérée par le générateur, convention du pilote 1 respectée.
• Scan secrets : rien.

Une seule réserve mineure (non bloquante) : l'étape 29 pointe Tweety-5d-Stable-Synthesis-Lean.ipynb sous le répertoire Tweety/ — le lien résout bien sur main, le nommage du fichier (suffixe Lean dans Tweety) est cohérent avec le fil « pont Z3→Lean » revendiqué.