feat(lean): migrer les 27 lakes first-party vers Lean/Mathlib 4.33

[jsboige]

Objectif

Monter l'ensemble des lakes Lean first-party de CoursIA vers Lean/Mathlib 4.33, en prenant comme ancrage initial le pin Mathlib utilisé par anthropics/fermats-last-theorem au commit aa2d8b34692b16c70f699536de0d8e75b9a3e9ef :

• cible cohérente CoursIA : leanprover/lean4:v4.33.0 ;
• Mathlib : db584cd6d46c92f209a44c0f1c829460d327499d, dont le lean-toolchain fixé est v4.33.0 ;
• FLT fixe son projet racine à v4.33.1, mais Lake a vérifié firsthand que ce décalage désactive le cache binaire Mathlib. Nous ne le recopions donc pas sans nécessité.

Cette montée va dans le sens de l'écosystème et doit précéder les ports issus de FLT : nous évitons ainsi d'écrire des shims descendants 4.33 → 4.32 destinés à être jetés.

Précédent

La migration 4.31 → 4.32 a été livrée sans rupture architecturale sous #10986, selon une séquence robuste : pilotes core-only, pilote Mathlib (sensitivity_lean), puis tranches séquentielles. Les adaptations rencontrées étaient bornées (résidus convert/defeq, ambiguïté zero_apply, chemins d'instances), et les caches binaires Mathlib étaient disponibles.

Cette issue reprend cette discipline sans supposer que 4.33 sera automatiquement sans adaptation : chaque lake doit compiler et conserver son intégrité formelle.

Inventaire vérifié au 2026-09-05

git ls-files 'MyIA.AI.Notebooks/**/lean-toolchain', hors .lake/packages et fixture tiers agent_tests/prover/session_state/reference_docs/stable_marriage/upstream :

• 27 lakes first-party ;
• 26 sur leanprover/lean4:v4.32.1 ;
• 1 sur leanprover/lean4:v4.31.0-rc2 : GameTheory/conway_cgt_lean.

Le fixture upstream stable_marriage à 4.25.0 est hors scope. Les dépendances vendored ou téléchargées sous .lake/packages/ sont hors scope comme cibles directes.

Dette formelle de référence, mesurée avec python scripts/lean/count_code_sorry.py --json : 15 distinct_code_sorry, répartis knot_lean=11, decision_theory_lean=2, game_theory_lean=1, conway_lean=1. La migration ne doit jamais augmenter ces comptes.

Plan phasé

1. Phase 0 — environnement et cache
   • installer leanprover/lean4:v4.33.0 ;
   • vérifier la disponibilité du cache Mathlib au pin retenu ;
   • documenter les renommages/API cassés réellement rencontrés, sans créer de shim global avant besoin.
2. Phase 1 — pilotes core-only
   • migrer les lakes sans dépendance Mathlib directe (lean_game_defs, lean_game_defs_ext, finiteness_lean, sous réserve de vérification des lakefiles) ;
   • lake build local complet pour chacun.
3. Phase 2 — pilote Mathlib
   • sensitivity_lean, déjà propre (distinct_code_sorry=0) et doté de CI build/proof-integrity/i18n ;
   • régénérer le manifest avec Lake, traiter les seules adaptations API nécessaires, puis build complet.
4. Phase 3 — pilotes utiles à FLT
   • galois_lean puis grothendieck_lean ;
   • ils servent de sondes aux API 4.33 ciblées par l'étude research(lean): cartographier le dépôt Anthropic FLT pour CoursIA #14771 : extensions cyclotomiques, valuations/corps locaux, sites/faisceaux et géométrie algébrique.
5. Phase 4 — rollout séquentiel
   • migrer les autres lakes par petites tranches cohérentes ;
   • ne pas lancer plusieurs builds Mathlib lourds en concurrence sur la même machine.
6. Phase 5 — cas externe conway_cgt_lean
   • vérifier d'abord une révision de vihdzp/combinatorial-games compatible Lean/Mathlib 4.33 ;
   • ne pas forcer un bump local créant un version-skate avec sa dépendance amont.

Acceptance par lake

• lean-toolchain = leanprover/lean4:v4.33.0 ;
• pin Mathlib direct ou dépendance héritée résolu vers une combinaison 4.33 cohérente ;
• lake-manifest.json régénéré par Lake, jamais édité à la main ;
• lake build local complet SUCCESS après le dernier changement ;
• distinct_code_sorry inchangé ou en baisse avec l'instrument canonique scripts/lean/count_code_sorry.py ;
• aucun native_decide, sorryAx transitif ou nouvel axiome interdit ;
• proof-integrity ciblée sur les modules modifiés lorsque câblée, sinon B.3 explicitement déclaré non applicable avec vérification manuelle adaptée ;
• parité des siblings FR/EN conservée ;
• une PR atomique par lake ou petite tranche cohérente ; aucun mélange avec les ports de code FLT.

Critères de clôture

• 27/27 lakes first-party migrés, ou exception amont explicitement documentée et trackée séparément ;
• 27/27 builds locaux réussis sur leur cible réelle ;
• dette formelle globale distinct_code_sorry ≤ 15 ;
• tous les jobs CI Lean/proof-integrity/i18n pertinents verts ;
• matrice finale lake → toolchain → pin Mathlib → build → proof-integrity postée dans cette issue ;
• research(lean): cartographier le dépôt Anthropic FLT pour CoursIA #14771 mis à jour pour que les probes et ports FLT ciblent 4.33, sans shim 4.32 par défaut.

Hors scope

• import monolithique du dépôt FLT ;
• copie de ses sources dans la PR de migration ;
• fixture tiers stable_marriage/upstream ;
• packages sous .lake/packages/ ;
• réduction de la dette sorry existante, sauf adaptation nécessaire qui permet honnêtement de la réduire.

Voir #14771 et #10986.

[jsboige]

Probe Phase 0 / #14771 : cinq sources FLT ont été testées sous Lean 4.33.0 + Mathlib db584cd6d46c92f209a44c0f1c829460d327499d; les cinq sont compilables (quatre exactes, une avec réduction de import Mathlib vers Mathlib.RingTheory.Valuation.RamificationGroup).

Deux points de migration à conserver :

1. lake exe cache get a téléchargé 8 690 archives mais leantar n’en a extrait que 7 308 sur cette installation Windows (1 382 échecs). Les imports ciblés restent utilisables ; import Mathlib force ensuite une reconstruction globale fragile. La migration doit privilégier les imports minimaux et ne pas interpréter un échec de création .olean comme une casse API.
2. Le fichier fppf exact échoue sur l’inférence des instances si l’option FLT backward.isDefEq.respectTransparency.types := false est omise, puis compile en 41 s lorsqu’elle est restaurée. Tester cette option au niveau des lakes qui en ont besoin, sans la propager globalement sans mesure.

La synthèse complète et les cinq sous-grains sont publiés sur #14771 : #14771 (comment)

[jsboige]

Grain: MED/lean — lane myia-po-2027:CoursIA-2 — prev: DEEP/notebook-lean #14927

[CLAIMED] lane myia-po-2027:CoursIA-2 — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/**

Sous-grain Phase 3 de #14773 : migrer uniquement galois_lean de Lean/Mathlib 4.32.1 vers la cible mesurée 4.33.0 / db584cd6d46c92f209a44c0f1c829460d327499d, régénérer le manifest avec Lake, adapter seulement les ruptures API réellement rencontrées, puis obtenir lake build complet, compte distinct_code_sorry non croissant, proof-integrity ciblée et parité FR/EN vertes. Aucun port FLT dans cette PR de migration.

Plateau vérifié : issue OPEN, aucun claim concurrent, aucune PR ouverte galois/4.33 touchant ce lake. Cette migration lève la dépendance explicite de #14783 ; après merge, la même lane enchaîne la tranche des complétions adiques locales sous une claim distincte.

[jsboige]

[DELIVERY] PR #14953 — galois_lean migré vers Lean/Mathlib 4.33.0 (db584cd6). See #14773 (Phase 3, sous-grain) — PR #14953 ne close PAS l'umbrella.

• lake build Galois SUCCESS (1342 jobs), source M23Lean4Web.lean byte-identique à main (aucune rupture API).
• distinct_code_sorry = 0 (avant/après).
• #print axioms (card/simple_M22/M23) = [propext, Classical.choice, Quot.sound] — whitelist §B, aucun sorryAx/native_decide.
• i18n : sans objet (aucun sibling _en).

lane myia-po-2027:CoursIA-2. Après merge, la même lane enchaîne #14783 sous claim distincte (cf dispatch).

[jsboige]

[CLAIMED] lane myia-po-2027:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/**

Sous-grain Phase 3 de #14773 (suite du séquencement galois -> grothendieck) : migrer uniquement grothendieck_lean de Lean/Mathlib 4.32.1 vers la cible mesurée 4.33.0 / db584cd6d46c92f209a44c0f1c829460d327499d, régénérer le manifest avec Lake, adapter seulement les ruptures API réellement rencontrées, puis lake build complet, distinct_code_sorry non croissant (baseline grothendieck = 0), proof-integrity ciblée et parité FR/EN (pattern globs Grothendieck.* i18n #4980) vertes. Aucun port FLT dans cette PR de migration. PR atomique pour ce lake (pas de mélange avec les autres lakes).

[jsboige]

[CLAIMED] lane myia-po-2027:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/** -- migration atomique sensitivity_lean vers Lean 4.33.0 / Mathlib db584cd6 (Phase 2 pilote Mathlib de #14773). Plateau verifie: issue OPEN, lakes galois/grothendieck/formal_groups/hecke deja a 4.33 sur main, aucune PR ouverte ni claim concurrent sur sensitivity_lean.

[jsboige]

[CLAIMED] lane myia-po-2027:CoursIA-2 -- paths: MyIA.AI.Notebooks/Sudoku/sudoku_lean/** -- migration atomique sudoku_lean vers Lean/Mathlib 4.33.0 (db584cd6d46c92f209a44c0f1c829460d327499d), sous-grain #14773 (rollout). Plateau verifie: issue OPEN, aucun claim concurrent sur sudoku_lean, aucune PR ouverte touchant ce lake (0 par gh pr list --search).

[jsboige]

Grain: MED/lean — lane myia-po-2024:CoursIA-2 — prev: MED/notebook-python #14902

[CLAIMED] lane myia-po-2024:CoursIA-2 — paths: MyIA.AI.Notebooks/GameTheory/assignment_lean/**

Sous-grain atomique du rollout #14773 : migrer uniquement assignment_lean de Lean/Mathlib 4.32.1 vers leanprover/lean4:v4.33.0 et Mathlib db584cd6d46c92f209a44c0f1c829460d327499d. Régénérer lake-manifest.json avec Lake, adapter seulement les ruptures API réellement rencontrées, puis obtenir lake build complet, compte canonique distinct_code_sorry non croissant, contrôle des axiomes/proof-integrity ciblé et parité FR/EN verte.

Plateau vérifié sur origin/main 401ed7de7 : lake encore sur 4.32.1 / Mathlib v4.32.1, aucune PR assignment_lean 14773, aucune PR ouverte touchant ce lake. Scope disjoint de la claim active MyIA.AI.Notebooks/Sudoku/sudoku_lean/** de po-2027:CoursIA-2. Aucun port FLT ni autre lake dans cette PR.

[jsboige]

[RELEASED] lane myia-po-2024:CoursIA-2 — paths: MyIA.AI.Notebooks/GameTheory/assignment_lean/** — claim retirée sans dispatch ni édition : le checker local classe le glob �mpty_scope et continue de bloquer sur la claim sudoku_lean existante. Aucun travail assignment_lean n'a démarré.

[jsboige]

[CLAIMED-AMEND] lane myia-po-2027:CoursIA-2 -- paths: MyIA.AI.Notebooks/Search/search_lean/** (migration 4.33, suite du rollout #14773 — sudoku livré PR #15012)