Cadrage: rendre comestible et visible le travail Grothendieck du depot (narration + visuels + gradation)

Cadrage : rendre comestible et visible le travail Grothendieck du dépôt

Issue de cadrage demandée par le user sur #17970 (c. 16:14Z, 26/09) :

« le Notebook ne fait pas vraiment honneur à tout le travail qu'on a accomplis. Si on est en Python, alors ça n'est pas pour montrer des blocs de lean qui seraient mieux affichés sous Kernel Lean, ou bien des stats qui parlent peu. Etre en Python, c'est être libre de faire ce qu'on fait sous Kernel Lean et d'autres choses. [...] il faudrait une belle narration avec des visuels, qui montre des choses, qui donne l'intuition des abstractions qu'on touche du doigt. Certaines représentations géométriques ne seront pas triviales, mais elles n'ont pas besoin d'être parfaites. Des schémas même un peu grossiers peuvent faire beaucoup pour la gradation pédagogique. »

Périmètre concerné

Tout le corpus Grothendieck accumulé dans le dépôt :

notebooks Lean-15 (fragilités, marée montante Lean-15: fragilites de Grothendieck -- trois lecons pour le depot (distill Serre-Connes) #17970), Serre100 01/07 (contre-exemples)
épic Epic Langlands : formes modulaires, fonctions L et Monstrous Moonshine — parcours pedagogique depuis la preuve formalisee de Fermat (2026) #17969 Langlands (7 grains), notes de vision
Greffe Sheydvasser Art 0/1/2 (Distiller la série « Surviving proofs » (S. Sheydvasser) : où ses quatre leçons sur la recherche de preuves éclairent nos notebooks #17888/feat(geometry,#17888): greffe Sheydvasser Art 0/1/2 sur 2 cells pivots (Geo-02) #17912, Geo-02)

Questions de cadrage

Narration : quel fil raconte le corpus — la « lentille grothendieckienne » (réutiliser l'esprit des cellules repliées de Lean-15) comme colonne vertébrale transverse ?
Visuels : quelles représentations géométriques privilégier (schémas grossiers acceptés) pour donner l'intuition des abstractions ? Python = liberté de faire ce que Lean fait ET plus — pas des blocs Lean collés ni des stats sèches.
Gradation pédagogique : comment ordonner les acquis (contre-exemple → fragilité → généralisation) pour un lecteur qui découvre ?
Forme : enrichissement des notebooks existants vs nouveau notebook de synthèse « visite guidée » ?

Acceptance (propositions à arbitrer)

Un document/livre de visite (notebook(s) + README de série) qui présente le corpus en narration continue, avec au moins N visuels géométriques (même grossiers).
Chaque brique du corpus référencée depuis cette visite (le travail devient visible depuis un point d'entrée unique).
Décision user sur le fil narratif retenu avant ouverture des grains d'exécution.

See #17970 (levée du Concern user c.16:14Z). Portage : à dispatcher par le coordinateur.

Grain: DEEP/notebook-python — lane myia-po-2027:CoursIA-2 — prev: MED/research-code #18396

[CLAIMED] lane myia-po-2027:CoursIA-2 — tranche 1 du cadrage : notebook de visite guidee visuelle Lean-15d-Lean-Grothendieck-Visuel-Python.ipynb, materialisant les abstractions (categories/foncteurs, cribles, topologie de Grothendieck, faisceaux, Yoneda, site de Zariski) en figures Python autonomes, sans dependance au lake.

Raison de cette forme plutot qu'un document de cadrage : les trois carnets existants du corpus couvrent le catalogue de code (Lean-15), l'atelier d'exercices (Lean-15b) et le companion formel (Lean-15c) -- aucun ne montre les abstractions, qui est la demande explicite du user (« une belle narration avec des visuels, qui montre des choses, qui donne l'intuition des abstractions »).

paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15d-Lean-Grothendieck-Visuel-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md

fix(notebook,#17978): nav Lean-15c/15d + retrait du compteur en prose (…

feat(lean,#17978): Lean-15d -- visite guidee visuelle des abstraction…

fix(closure-dossier,#15578): lire body PR depuis timeline au lieu de …

Urne delivered : pas encore livre, je la rends au tapis (ai-01, verifie sur origin/main le 05/10)

La visite Lean-15d-Lean-Grothendieck-Visuel est livree, executee et presentee dans le README de la serie (#18522, mergee le 30/09).

Il reste deux criteres :

la visite ne reference pas encore les autres briques du corpus : Serre100, Langlands, la greffe Sheydvasser/Geo-02 (Distiller la série « Surviving proofs » (S. Sheydvasser) : où ses quatre leçons sur la recherche de preuves éclairent nos notebooks #17888, feat(geometry,#17888): greffe Sheydvasser Art 0/1/2 sur 2 cells pivots (Geo-02) #17912) ;
le fil narratif retenu n'a pas ete tranche.

Prochain geste : ajouter ces references a la visite, puis proposer le fil narratif dans le fil de cette issue.

[CLAIMED] lane myia-po-2023:CoursIA-2 -- referencer depuis Lean-15d les briques restantes du corpus (Serre100, Langlands, greffe Sheydvasser/Geo-02) et proposer le fil narratif (pose par ai-01 au dispatch, file profonde du 05/10). paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15d-*.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md

docs(consolidation,#16473): acceptance 2 lot 6 (axe E, 60 orphelines #…

Enrich(notebook,#17978): Lean-15d references Serre100, Langlands, Geo…

docs(consolidation,#16473): acceptance 2 lots 1+3+4+5+6 (axes B/A/C/D…

feat(iit,#19333-G): pont cusp <-> trefle -- la cubique cuspidale en p…

Navigation Menu

Repository navigation

Cadrage: rendre comestible et visible le travail Grothendieck du depot (narration + visuels + gradation) #17978

Cadrage : rendre comestible et visible le travail Grothendieck du dépôt

Périmètre concerné

Questions de cadrage

Acceptance (propositions à arbitrer)

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Cadrage: rendre comestible et visible le travail Grothendieck du depot (narration + visuels + gradation) #17978

Description

Cadrage : rendre comestible et visible le travail Grothendieck du dépôt

Périmètre concerné

Questions de cadrage

Acceptance (propositions à arbitrer)

Activity

jsboige commented on Sep 29, 2026

myia-ai-01 commented on Oct 5, 2026

myia-ai-01 commented on Oct 5, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions