Part of #11703 (visibilité des lakes Lean dans les notebooks).
Demandée par le mainteneur sur #19439 (commentaire du 2026-10-06T08:23:01Z) :
« Il me semble que le format de ces annexes interminables a fait son temps. Ca mériterait une issue de réorganisation narrative qui consolide proprement toutes ces annexes en enrichissant le markdown dans une progression pédagogique plus structurée, avec plus de profondeur (descendre d'un niveau de sous-titres dans la structuration) »
Constat
Les annexes produites par le chantier de visibilité lakes (#11703) s'empilent en queue de carnet comme des sections plates ## Annexe — <sujet>, sans progression narrative ni transition avec le corps du cours. Le geste rend les modules noirs visibles — le défaut est narratif.
Périmètre mesuré au 2026-10-06
Inventaire exhaustif repo-wide des headings Annexe : seuls 2 carnets portent le pattern du chantier :
| Carnet |
Sections |
Détail |
SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb |
6 |
## Annexe — SheafCondition (#11703) · Du crible fermé à la faisceautisation Plus · Les tiges (stalks) (#11703) · Des ouverts au préfaisceau gratte-ciel (#11703) · Faisceaux flasques et résolution de Godement (#11703) · Sites, topologies et comparaisons (#11703) |
Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb |
1 |
## Annexe — ErdosSpencer/Moments : la machinerie des moments (#11703) |
Hors périmètre, mesuré (annexes pédagogiques préexistantes, motifs distincts — ne pas toucher) : Lean-16b (Annexes A-G), Lean-22 (A-B), Lean-31 (A-D), SW-11 Python/C# (A-C kglab/OWLReady2), SC-07c (preuve exo 2), SL-1b (solutions), Lean-36 (« Annexe A de Tegmark » = référence au livre).
Modèle cible déjà dans le dépôt : le format « ## Annexes — approfondissements optionnels + ### Annexe A/B/C… » de Lean-16b et Lean-31 — un chapitre continu, lettré, un niveau de sous-titres plus bas. La consolidation de Lean-15c peut reprendre cette forme.
Travail demandé
- Consolider : replacer chaque annexe dans la progression pédagogique du carnet — section markdown enrichie au fil du cours plutôt qu'empilement final ; regrouper les annexes d'un même thème mathématique en un chapitre continu (modèle Lean-16b/31).
- Enrichir : plus de profondeur narrative — le pourquoi mathématique avant le
#check, la lecture APRÈS la sortie, transitions avec le corps existant.
- Préserver le contenu factuel : les déclarations citées et leurs liens ne se perdent pas — reformatage narratif, pas une purge.
- Une PR par carnet ; markdown-only ou cellules déplacées sans modification de code → re-exécution due seulement si une cellule source code bouge (C.2/C.3).
Critères d'acceptation
Sans parent supplémentaire : fille directe de l'EPIC #11703.
Part of #11703 (visibilité des lakes Lean dans les notebooks).
Demandée par le mainteneur sur #19439 (commentaire du 2026-10-06T08:23:01Z) :
Constat
Les annexes produites par le chantier de visibilité lakes (#11703) s'empilent en queue de carnet comme des sections plates
## Annexe — <sujet>, sans progression narrative ni transition avec le corps du cours. Le geste rend les modules noirs visibles — le défaut est narratif.Périmètre mesuré au 2026-10-06
Inventaire exhaustif repo-wide des headings
Annexe: seuls 2 carnets portent le pattern du chantier :SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb## Annexe — SheafCondition(#11703) ·Du crible fermé à la faisceautisation Plus·Les tiges (stalks)(#11703) ·Des ouverts au préfaisceau gratte-ciel(#11703) ·Faisceaux flasques et résolution de Godement(#11703) ·Sites, topologies et comparaisons(#11703)Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb## Annexe — ErdosSpencer/Moments : la machinerie des moments(#11703)Hors périmètre, mesuré (annexes pédagogiques préexistantes, motifs distincts — ne pas toucher) :
Lean-16b(Annexes A-G),Lean-22(A-B),Lean-31(A-D),SW-11Python/C# (A-C kglab/OWLReady2),SC-07c(preuve exo 2),SL-1b(solutions),Lean-36(« Annexe A de Tegmark » = référence au livre).Modèle cible déjà dans le dépôt : le format «
## Annexes — approfondissements optionnels+### Annexe A/B/C…» deLean-16betLean-31— un chapitre continu, lettré, un niveau de sous-titres plus bas. La consolidation deLean-15cpeut reprendre cette forme.Travail demandé
#check, la lecture APRÈS la sortie, transitions avec le corps existant.Critères d'acceptation
Lean-15crestructuré (carnet pilote, le plus chargé) — plus aucun## Annexe —orphelin en queue ; contenu intégré sous chapitres thématiques.Discrepancy-02traité.#11703+lake).Sans parent supplémentaire : fille directe de l'EPIC #11703.