EPIC origami : géométrie différentielle en Lean — conjecture de Poincaré et flot de Ricci, par dépendance au dépôt amont

Grain: DEEP/lean

Source

Le dépôt. qinz1yang/differential-geometry, sous licence Apache-2.0, release v0.1.3 du 27/09/2026, sur Lean et Mathlib v4.33.1. Il se présente comme une dépendance amont, à déclarer dans un lake par [[require]] sur git avec un tag.

Ce que son README annonce sans sorry. Les axiomes déclarés sont propext, Classical.choice et Quot.sound. Les résultats annoncés :

Topologie de dimension 3 : la conjecture de Poincaré ; le théorème de Moise.
Flot de Ricci, résultats de Perelman : le théorème du voisinage canonique, le non-effondrement local, la monotonie de l'entropie W et celle du volume réduit.
Flot de Ricci, résultats de Hamilton : le théorème de 1982, la compacité, le pincement de Hamilton–Ivey, l'inégalité de Harnack matricielle.
Estimées : les estimées de Shi.
Géométrie et analyse : Bonnet–Myers, Bochner, Weitzenböck, Lichnerowicz, la cohomologie de de Rham, le lemme de Morse, les principes du maximum paraboliques, Li–Yau.

Ces affirmations sont rapportées : elles ne sont pas encore vérifiées chez nous.

Cadrage — comme Fermat ou Navier-Stokes (Concern user du 28/09)

L'objectif n'est pas d'expliquer la preuve fleuve de millions de lignes, mais d'identifier
les définitions et théorèmes les plus pertinents qui complètent Mathlib et résonnent avec
le dépôt — même approche que pour Fermat ou Navier-Stokes.

Sélection retenue au Pli 1 (livrée #19636, enveloppe differential_lean/ ; témoin
#print axioms mesuré sur les trois têtes : uniquement propext, Classical.choice,
Quot.sound) :

Lemme de Morse (exists_quadratic_chart_of_isLocalMin) — 47 modules / 23,5 k lignes ;
Cohomologie de de Rham (pullbackCohomologyMap_id) — 33 modules / 13 k lignes ;
Bonnet–Myers (bonnet_myers_diameter_le_of_complete_metric) — 383 modules / 181 k lignes.

Poincaré lui-même et les théorèmes de Perelman/Hamilton restent hors sélection : ils
entrent par l'énoncé et ses axiomes (build témoin, Pli 2), jamais par la preuve
expliquée. Le pourquoi de chacun des trois retenus : commentaire du 10/10.

Mesure sur un clone (28/09/2026, commit `7a48598d`)

Le dépôt compte 17 555 modules et 4,7 millions de lignes. Fermeture d'imports par point d'entrée, comptée dans le dépôt seul, hors Mathlib :

Point d'entrée	Modules	Lignes
`Topology/ThreeManifold/Poincare`	14 197	4,0 M
Théorème de Hamilton (1982)	3 051	1,6 M
Monotonie de l'entropie W	1 476	0,7 M
Bonnet–Myers	383	181 k
Cohomologie de de Rham (`Tensor/Exterior/Cochain`)	33	13 k
Lemme de Morse	13	20 k

Leur propre CI compile tout depuis les sources (lake --no-cache build), sur un runner auto-hébergé macOS ARM64.

Conséquence : Poincaré dépasse le budget de notre CI Lean, dont les jobs meurent déjà vers 30 min de build (#18100). Les petits points d'entrée y tiennent.

La surface : par dépendance, jamais par copie

Le précédent est GameTheory/social_choice_lean_peters/ : un lake d'enveloppe qui fait require du dépôt amont à une révision épinglée, un fichier de visite (PetersTour.lean et son jumeau _en), et un carnet. On reprend la même forme :

aucune source recopiée, aucun fork, et aucune PR chez eux sans y être invités ;
un tag de release épinglé ;
un lake d'enveloppe qui peut rester en v4.33.1 alors que le parc est en v4.33.0 : c'est une exception documentée, comme pour Peters.

Plis

Chaque pli ne se déplie qu'à la complétion vérifiée du précédent. Le coordinateur crée alors ses sous-issues et poste un commentaire [PLI N DÉPLIÉ] qui les liste. Rien n'est créé d'avance.

Pli 1 — Reconnaissance (actionnable maintenant, porté par cette issue)

Petites fermetures. Créer un lake d'enveloppe minimal épinglé sur v0.1.3. Lancer lake build sur les trois petites fermetures (Morse, de Rham, Bonnet–Myers), puis #print axioms sur un théorème de chacune. Mesurer le temps et la mémoire.
Build témoin de Poincaré, hors CI. Construire la fermeture Poincaré sur une machine forte et relever :
- la durée et la mémoire ;
- la sortie de #print axioms DifferentialGeometry.Topology.poincare_conjecture.
Citer le journal dans le body de la PR. C'est ce build qui décide si Poincaré peut entrer dans un carnet exécuté.
Sources tierces. Vérifier la conformité des sources qu'ils vendorisent (voir leur NOTICE : Schoenflies, TauCeti, DeGiorgi, CanonicalTopology…). Notre enveloppe ne devrait rien redistribuer : à confirmer.
Emplacement. Proposer une place dans le dépôt (sous-série Lean, ou rattachement à une série existante), sans rien renommer. Le choix se fait avec la numérotation Lean en cours (accrétions et sous-séries), selon la règle notebook-accretion-numbering.

Pli 2 — Visite (à déplier)

Un fichier de visite, et un carnet « La conjecture de Poincaré en Lean : ce que dit l'énoncé, ce que la preuve mobilise ». Il couvre :

la lecture de l'énoncé et ses axiomes ;
la structure des dépendances, avec le graphe d'imports traité comme une donnée ;
la chaîne Moise → flot de Ricci avec chirurgie → extinction en temps fini.

Il s'appuie sur le build témoin du pli 1, pas sur une compilation en CI.

Pli 3 — Sous-série (à déplier)

Trois à cinq carnets sur les pièces qui compilent en CI : lemme de Morse, cohomologie de de Rham, Bonnet–Myers, principe du maximum, énoncés de monotonie de Perelman. Chaque carnet est réellement exécuté (règle C.2).

Pli 4 — Résonances (à déplier)

Relier ce travail à nos lakes existants : théorie des nœuds (#2874), Serre 100 (#16334), Grothendieck (#2159), géométrie (#17544). Repérer ce qui, chez nous, pourrait consommer leurs résultats plutôt que les réécrire (règle organ-first-implementation).

Concern: Pour Poincaré et les preuves fleuves, je pense que notre approche doit être similaire à Fermat ou Navier&Stokes. L'objectif n'est pas de tout expliquer la preuve fleuve de millions de loc, mais plutôt d'identifier les définitions et les théorèmes les plus pertinentes qui complètent Mathlib et qui résonnent avec notre Dépôt.

[CLAIMED] lane myia-po-2024:CoursIA-2 -- Pli 1 reconnaissance de #18205 : sub-grains sources tierces (NOTICE + conformite) + emplacement propose -- paths: docs/lean/origami-reconnaissance.md

feat(lean,#18205): Pli 1 reconnaissance -- sources tierces + emplacem…

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

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

[CLAIMED] lane myia-po-2025:CoursIA — tapis central du 06/10 22:46Z, file profonde posee par le coordinateur au dispatch (rang 4/7) : EPIC origami : géométrie différentielle en Lean — conjecture de Poincaré et flot de Ricci,. Premiere etape de la lane : verifier firsthand que l'acceptance n'est pas deja couverte ; sinon [RELEASED] avec le motif.

[CLAIMED-AMEND] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/**, docs/lean/origami-pli1-mesures.md

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #19612

Amendement de mon [CLAIMED] du 2026-10-06T22:47:54Z (rang 4/7 du tapis central). Ce marqueur était epic-wide — aucune clause paths: — donc il bloquait toutes les autres lanes sur #18205 (fail-CLOSED, #11703). Il est restreint ici au seul périmètre que cette lane travaille réellement.

Ce que cette lane prend — Pli 1, sub-grain 1

L'enveloppe lake differential_lean/ (dépendance Lake épinglée sur le tag amont v0.1.3, commit 7a48598d35109aa99d1cc678e2724c213cdf4ff3), le lake build des trois petites fermetures — lemme de Morse, cohomologie de de Rham, Bonnet–Myers — et #print axioms sur un théorème de chacune, avec mesure du temps et de la mémoire.

C'est l'acceptance de Pli 1 non couverte par #18978 (MERGE le 2026-10-03).

Ce que cette lane ne prend pas

Sub-grains 3 et 4 (sources tierces, emplacement) — livrés par feat(lean,#18205): Pli 1 reconnaissance -- sources tierces + emplacement #18978, lane myia-po-2024:CoursIA-2.
Sub-grain 2 (build témoin de Poincaré) — reste ouvert ; machine forte requise, ce n'est pas ce périmètre.
Plis 2, 3, 4 — non dépliés par le coordinateur.

Le reste de l'EPIC est laissé libre.

Premier geste de vérification (exigé par le steer)

L'acceptance de Pli 1 est partiellement couverte, vérifié firsthand :

couvert par feat(lean,#18205): Pli 1 reconnaissance -- sources tierces + emplacement #18978 : sub-grains 3 (sources tierces) et 4 (emplacement) ;
non couvert, déclaré hors périmètre par feat(lean,#18205): Pli 1 reconnaissance -- sources tierces + emplacement #18978 lui-même : sub-grain 1 (« lake trop lourd pour 30 min po-2024 ») et sub-grain 2, tous deux en RECOVERABLE-MACHINE — docs/lean/origami-reconnaissance.md, sections 1 et 4, sur main.

Le grain est donc réel, et non un doublon.

Note de péremption

Le [CLAIMED] de myia-po-2024:CoursIA-2 du 2026-10-03T09:43:14Z (paths docs/lean/origami-reconnaissance.md) est périmé au sens de check_lane_claim.py (86,5 h ≥ seuil 48 h) et son périmètre est déjà livré par #18978 MERGE. Aucune intersection avec le périmètre ci-dessus.

See #18205 · See #18978

🤖 Generated with Claude Code

fix(prose,#19636): retrait des 2 compteurs de prose du README differe…

feat(lean,#18205): enveloppe differential_lean -- 3 fermetures + #pri…

Réponse ai-01 à ton Concern du 28/09. Il est resté sans réponse alors que trois claims l'ont suivi. C'est un manquement.

Ton cadrage : faire comme pour Fermat ou Navier-Stokes. Il ne s'agit pas d'expliquer la preuve fleuve, mais de retenir les définitions et théorèmes les plus pertinents qui complètent Mathlib et résonnent avec le dépôt.

Porteur : la lane myia-po-2025:CoursIA (claim du 06/10, differential_lean + docs/lean/origami-pli1-mesures.md). Dispatch envoyé, en trois temps :

relire l'issue en entier, commentaires compris ;
écrire ici comment le Pli 1 applique ce cadrage, c'est-à-dire quelle sélection de définitions et de théorèmes, et pourquoi ceux-là ;
le reporter dans le body.

Application du cadrage du Concern du 28/09 (comme Fermat ou Navier-Stokes) — Pli 1, livré.

Le cadrage du user : ne pas expliquer la preuve fleuve ; retenir les définitions et théorèmes les plus pertinents qui complètent Mathlib et résonnent avec le dépôt. Voici comment le Pli 1 livré (#19636, enveloppe differential_lean/) l'applique, et pourquoi cette sélection plutôt qu'une autre.

Les trois retenus, et pourquoi eux

Témoignage mesuré : #print axioms interrogé sur chaque théorème-tête, dans les deux siblings — chacun ne dépend que de propext, Classical.choice, Quot.sound (aucun sorryAx, aucun native_decide.*). Temps et mémoire dans le README du lake.

Retenu	Fermeture	Pourquoi celui-là
Lemme de Morse — `exists_quadratic_chart_of_isLocalMin`	47 modules / 23,5 k lignes, build 215 s	La forme locale canonique près d'un point critique : « une fonction lisse y ressemble à une forme quadratique ». C'est l'outil que la série géométrie (#17544) et les carnets d'optimisation peuvent consommer tel quel ; fermeture compacte, tenable en CI.
Cohomologie de de Rham — `pullbackCohomologyMap_id`	33 modules / 13 k lignes, 285 s	Le pont analyse ↔ topologie, et la définition-lingua-franca que les plis suivants citeront. La plus petite fermeture de l'amont : coût d'entrée minimal pour une définition structurante.
Bonnet–Myers — `bonnet_myers_diameter_le_of_complete_metric`	383 modules / 181 k lignes, 1 859 s	Le théorème-emblème « la courbure borne la topologie » (Ricci ≥ (n−1)k > 0 ⇒ diamètre borné, compacité) : la porte d'entrée géométrique du monde flot de Ricci que vise l'EPIC, sans toucher à la preuve fleuve. Le plus lourd des trois — mesuré, tenable en build de visite hors CI.

Ce qui n'est pas retenu, et pourquoi

Poincaré lui-même (14 197 modules, 4,0 M lignes) et les résultats de Perelman/Hamilton (monotonies, non-effondrement, chirurgie) restent dans le build témoin (Pli 1 sub-grain 2, machine forte, hors CI) : les expliquer serait la preuve fleuve, exactement ce que le cadrage exclut. Ils entrent par l'énoncé et ses axiomes (Pli 2), jamais par la preuve.

Les deux axes du tri, explicites

Complétion de Mathlib. Chacun des trois est un résultat que l'amont positionne au-delà de ce que Mathlib porte — positionnement rapporté par leur README, et que notre visite mesure par le témoin d'axiomes plutôt que de le reprendre sur parole.
Résonance avec le dépôt. Morse (géométrie [Epic] Serie SymbolicAI/Geometry — preuve automatique en geometrie, programme gradue (01 figure->equation, 02 Grobner, 03 Wu, 04 DD+AR, 05 pont Lean) #17544, optimisation), de Rham (topologie), Bonnet–Myers (la courbure de Ricci, socle du flot homonyme) : les trois se rattachent à des séries ou lakes existants ; le Pli 4 les recoupera explicitement.

La discipline de preuve reste celle du dépôt

Pour une dépendance externe, l'équivalent du compte de sorry est le témoin #print axioms : mesuré, pas annoncé. C'est la même garde que pour nos lakes propres (trois classes d'axiomes interdites, sorryAx transitif compris) — appliquée au bord de la dépendance.

Le cadrage est reporté dans le body de l'issue (section « Cadrage — comme Fermat ou Navier-Stokes »).

Feat(ci,#20183): filet des Concerns user sans reponse sur les issues (#…

Note de rattachement (carte Lean phase 1, #17545 c.6108479114).

Le lake differential_lean n'a aujourd'hui aucun carnet consommateur : aucun .ipynb du dépôt ne le cite (git grep, main @ 2446fd0ed8). La carte cible Lean le laisse hors de ses tranches.

Son carnet d'exposition appartient donc à cet Epic. Le mainteneur a demandé que chaque escalier commence par une note de conception : l'inventaire des modules et théorèmes avec le carnet qui les expose, l'ordre des marches, puis le capstone. Elle vaut aussi pour le premier carnet de ce lake, quand l'Epic en arrivera là.

[INFO] Pli 1, sub-grain 1 — journal livré — PR #20456 (branche docs/18205-origami-pli1-mesures).

docs/lean/origami-pli1-mesures.md : relevé du run décisif du 2026-10-08 sur myia-po-2025, hors CI. Trois commandes — lake exe cache get rc=0 (3 249 s), lake build rc=0 (10 039 s, Build completed successfully (4223 jobs)), lake env lean DifferentialTour.lean rc=0 (329 s) — et le témoin #print axioms lu deux fois : les trois théorèmes-têtes des deux siblings ne dépendent que de propext, Classical.choice, Quot.sound.

Ce que la mesure décide : la visite reste hors CI — 2 h 47 pour le build complet depuis un .lake froid, 3 h 47 pour la visite, quand les jobs CI meurent vers ~30 min (#18100) ; même le relevé chaud du 07/10 (2 359 s pour les trois fermetures) dépasse le plafond. La contrainte est le temps, ni la mémoire (~5 Go/32) ni le disque (~9,2 Gio de .lake).

Périmètre : sub-grain 1 seulement. Le sub-grain 2 (Poincaré, 14 197 modules, machine forte) reste ouvert, non claimé par cette lane.

🤖 Generated with Claude Code

Fix(#18205): prose-counts -- retirer les compteurs de fichiers de la …

Grain: DEEP/lean -- lane myia-po-2025:CoursIA -- prev: DEEP/genai #20460

[CLAIMED-AMEND] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/**, docs/lean/origami-pli1-mesures.md, docs/lean/origami-poincare-mesures.md -- Pli 1 sub-grain 2 : build temoin de Poincare (machine forte, hors CI, cache .lake du sub-grain 1 chaud 9 Go) + releve #print axioms DifferentialGeometry.Topology.poincare_conjecture + journal. L'ancien marqueur epic-wide SUPERSEDED est libere par le present amend (hygiene #12327). Le build tourne en arriere-plan ; le journal livrera la duree, le rc et les axiomes.

docs(lean,#18205): Pli 1 -- journal du build hors CI de l'enveloppe d…

Navigation Menu

Repository navigation

EPIC origami : géométrie différentielle en Lean — conjecture de Poincaré et flot de Ricci, par dépendance au dépôt amont #18205

Source

Cadrage — comme Fermat ou Navier-Stokes (Concern user du 28/09)

Mesure sur un clone (28/09/2026, commit `7a48598d`)

La surface : par dépendance, jamais par copie

Plis

Pli 1 — Reconnaissance (actionnable maintenant, porté par cette issue)

Pli 2 — Visite (à déplier)

Pli 3 — Sous-série (à déplier)

Pli 4 — Résonances (à déplier)

Ce que cette lane prend — Pli 1, sub-grain 1

Ce que cette lane ne prend pas

Premier geste de vérification (exigé par le steer)

Note de péremption

Les trois retenus, et pourquoi eux

Ce qui n'est pas retenu, et pourquoi

Les deux axes du tri, explicites

La discipline de preuve reste celle du dépôt

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

EPIC origami : géométrie différentielle en Lean — conjecture de Poincaré et flot de Ricci, par dépendance au dépôt amont #18205

Description

Source

Cadrage — comme Fermat ou Navier-Stokes (Concern user du 28/09)

Mesure sur un clone (28/09/2026, commit 7a48598d)

La surface : par dépendance, jamais par copie

Plis

Pli 1 — Reconnaissance (actionnable maintenant, porté par cette issue)

Pli 2 — Visite (à déplier)

Pli 3 — Sous-série (à déplier)

Pli 4 — Résonances (à déplier)

Activity

jsboige commented on Sep 28, 2026

jsboige commented on Oct 3, 2026

jsboige commented on Oct 6, 2026

jsboige commented on Oct 7, 2026

Ce que cette lane prend — Pli 1, sub-grain 1

Ce que cette lane ne prend pas

Premier geste de vérification (exigé par le steer)

Note de péremption

myia-ai-01 commented on Oct 9, 2026

jsboige commented on Oct 9, 2026

Les trois retenus, et pourquoi eux

Ce qui n'est pas retenu, et pourquoi

Les deux axes du tri, explicites

La discipline de preuve reste celle du dépôt

jsboige commented on Oct 11, 2026

jsboige commented on Oct 12, 2026

jsboige commented on Oct 12, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

Mesure sur un clone (28/09/2026, commit `7a48598d`)