Lean i18n — inventaire FR/EN et proposition de convention (cycle 38, See #4980)

Source : décision user 2026-07-02 (verbatim body #4980) — « je ne parlais pas des readme qui doivent tous etre traduits comme les autres, mais des fichiers lean eux-memes dont certains sont en fr et d’autres en en. Je serais pour les harmoniser en francais et les traduire au moins en anglais, comme les readme. »

Scope cycle 38 : (a) inventaire FR/EN par lake (tableau evidence-cited) + (b) proposition de convention. Hors scope cycle 38 : PR pilote de traduction (cycle 39+).

Note (mise à jour 2026-07-14) — données d’inventaire SUPERSEDED. Le tableau par lake ci-dessous (état 2026-07-04) est périmé : les 4 lakes marqués « backlog EN-dominant » (cooperative_games_lean, social_choice_lean, stable_marriage_lean, decision_theory_lean) sont tous migrés FR-first + EN sibling ou absorbés par la consolidation #4365 (vérifié firsthand : cooperative_games_lean 9 fichiers avec _en, decision_theory_lean 25 fichiers avec _en, social_choice_lean/stable_marriage_lean résiduels absorbés dans game_theory_lean). La convention Option A est ratifiée (codifiée dans .claude/rules/code-style.md §Lean i18n) et le pilote est livré (PR #5883 CooperativeGames.lean FR-first + EN sibling). Pour l’état de couverture courant, voir l’inventaire live I18N_INVENTORY.md (rafraîchi 2026-07-14). Ce fichier reste la référence pour la proposition de convention (Options A/B/C, méthodologie, justification).

Méthode d’inventaire

  • Population : 208 fichiers *.lean dans MyIA.AI.Notebooks/*/*lean*/ (hors .lake/packages/ qui sont des dépendances tierces Mathlib/aesop/etc., non modifiables par nous).
  • Détection : grep -rE "^/-- " (première ligne d’un bloc docstring /-- ... -/).
  • Heuristique langue :
    • FR = présence d’un mot français typique sur la même ligne (que|une|des|les|est|sont|pour|dans|avec|nous|ou|si).
    • EN = présence d’un mot anglais typique (the|is|of|for|with|that|this|are).
  • Biais connu : les regex sur première ligne sous-estiment les docstrings multi-lignes (les -- ... -/ lignes suivantes ne sont pas scannées par grep -E "^/-- "). L’inventaire est indicatif, pas exhaustif ; un audit complet passerait par parsing AST Lean (lean --print-resolution) ou grep étendu multi-ligne.

Tableau par lake (état 2026-07-04)

Lake .lean own Docstrings FR ≈ EN ≈ Dominant Hypothèse cycle
GameTheory/cooperative_games_lean 5 133 1 96 EN cycle early (Bondareva-Shapley #3954)
GameTheory/social_choice_lean 10 120 16 90 EN cycle early (Arrow/Sen)
GameTheory/stable_marriage_lean 7 51 2 30 EN cycle early
GameTheory/repeated_games_lean 6 16 8 5 mixte mixte avéré
GameTheory/minimax_lean 5 21 14 0 FR pivot FR cycle ~16-18
ML/learning_theory_lean 19 101 66 2 FR pivot FR (Novikoff perceptron 0 sorry #4140)
Probas/decision_theory_lean 13 67 15 35 EN mixte (VNM #4049 + Coherence #4050 cycles 24-26)
QuantConnect/kelly_lean 4 24 9 0 FR FR-first natif (Kelly critère)
Search/astar_lean 6 19 13 2 FR FR-first natif (lake phare #4048, A* P1/P2/P4/P5)
Sudoku/sudoku_lean 5 24 21 2 FR FR-first natif (preuve 0-sorry)
Total 80 576 165 262 EN global —

Observations :

  1. Pattern dominant = par lake, pas mélangé : aucun lake ne montre un ratio FR/EN proche de 50/50 dans ses docstrings — c’est un choix d’auteur/cycle, pas un drift accidentel. Bonne nouvelle : la convention peut s’appuyer sur l’existant sans imposer une migration disruptive.

  2. Minorité EN majoritaire (snapshot 2026-07-04, depuis superseded) : 3 lakes EN (cooperative, social_choice, stable_marriage) + decision_theory_lean (mixte 35 EN). 6 lakes déjà FR ou FR-dominants.

  3. EN majoritaire au global (262 vs 165) mais FR-first est la trajectoire récente : les lakes créés cycle 16+ (astar, learning_theory, sudoku, kelly) sont tous FR-first. La convention proposée doit acter cette trajectoire plutôt qu’imposer un revert.

Proposition de convention (recommandation Option A)

Option A — FR-first canonique + EN optionnel pour publication (recommandée)

Règle : - Docstrings en français par défaut dans tous les *.lean own. - Une traduction anglaise est optionnelle pour les lakes destinés à une audience externe (publication, papier, dépôt public). - Si EN présent, deux blocs /-- ... -/ consécutifs : français d’abord, anglais ensuite, séparés par -- EN -- sur une ligne de commentaire seule. - Justification : aligne avec CLAUDE.md .claude/rules/readme-french-first.md Règle HARD 1 (FR d’abord, EN préservé en .en.md companion) ; acte la trajectoire récente 6/11 lakes ; minimise le coût de maintenance (pas de double-docstring obligatoire).

Migration des 4 lakes EN-dominants : proposition — ai-01 dispatcher la traduction vers po-2026 (Lean builders, lake build disponible, partition native). Hors scope ce cycle (depuis : tous migrés/absorbés, cf. note de mise à jour ci-dessus).

Option B — Docstring bilingue obligatoire (rejetée)

Règle : tout *.lean porte deux docstrings (FR + EN), traduction automatique assistée puis revue manuelle.

Rejetée pour : - Coût double : maintenance × 2 par lake, drift FR/EN inévitable sur les cycles suivants. - Pas d’alignement readme-first : CLAUDE.md readme-french-first.md autorise la préservation EN en .en.md séparé, pas en docstring bilingue. - Biais qualité : traduction automatique même assistée dégrade la précision mathématique (notation formelle, références Mathlib).

Option C — Status quo (rejetée)

Règle : ne rien faire, accepter la dispersion FR/EN par lake.

Rejetée pour : ne résout pas la demande user 2026-07-02 explicite. La dispersion actuelle crée une friction cognitive pour les lecteurs (lake X en FR, lake Y en EN, lake Z mixte).

Suite cycle 39+ (état actualisé 2026-07-14)

  • PR pilote traduction — LIVRÉ : CooperativeGames.lean FR-first + EN sibling (PR #5883, 2026-07-10), root aggregator bilingue. Le candidat initial Sudoku/sudoku_lean a été devancé par le pilote CooperativeGames.
  • Backlog 4 lakes EN-dominants — DRAINED : cooperative_games_lean et decision_theory_lean migrés FR-first + EN sibling (vérifié firsthand : fichiers _en présents) ; social_choice_lean et stable_marriage_lean absorbés dans game_theory_lean par la consolidation #4365 (ne sont plus des lakes standalone). Aucun backlog EN-dominant restant sur les own-lakes.
  • Convention ratifiée — FAIT : Option A codifiée dans .claude/rules/code-style.md §Lean i18n (FR-first canonique + EN sibling Foo_en.lean, namespace _en, drift-CI byte-identity). État de couverture courant : I18N_INVENTORY.md.
  • Hot-zones restantes (multi-cycle) : Conway (Hashlife 543L, MacroCell 794L), Grothendieck (fichiers EN-mono volumineux), knot (actif c.420-c.425) — cf. inventaire live.

Conformité et leçons appliquées

  • R1-R4 catalog-pr-hygiene : ce fichier est dans docs/lean/, pas dans le catalogue → R1 PASS (catalogue intact), R2 PASS (rebase frais git checkout origin/main -b leçon c31), R3 PASS (1 fichier ajouté, +X/-0 lignes, atomic), R4 PASS (See #4980 + See #1650 Phase 0.5 + Part of #4208 axe E).
  • G.9 firsthand verify : 11 lakes inventoriés firsthand via find + grep -rE ; chiffres FR/EN indicatifs, méthodologie documentée (biais première-ligne explicité).
  • H.1 : pas de notebook touché, livrable *.md only.
  • Anti-régression D : pas de code Lean touché, juste inventaire read-only.
  • Pas de CJK : 0 parasite vérifié.
  • Pas d’emoji : 0 emoji (mandat user, code-style §E).
  • FR-first : prose FR, aligns avec CLAUDE.md.
  • C205-HARD-P : warnings MD060/MD032/MD037 cosmétiques tolérés.

Liens

  • Issue #4980 — i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote
  • Issue #1650 — traduction multilingue Phase 0.5 (backfill manuel)
  • Issue #4208 — Roadmap Lean (axe E i18n)
  • EPIC #3801 — SOTA ledger (cadrage registration pré-existant)
  • .claude/rules/readme-french-first.md — convention FR d’abord pour les docs markdown, transposeable au Lean
  • .claude/rules/code-style.md — code style global (cible pour la sous-section Lean i18n à venir)
  • Mémoires liées : [[c201-5291-planners-feuille-remediation]] (leçon c201-CRIT 8e cycle), [[c203-5294-argument-analysis-feuille]] (leçon c31 8e cycle)
  • Branche : feat/4980-lean-i18n-inventory
  • Commit : à venir (atomique 1 fichier docs/lean/i18n-inventory-cycle-38.md)

🤖 Generated with Claude Code

État du rollout i18n (déporté de .claude/rules/code-style.md, 2026-08-21)

Rollout : fleet DRAINED (c.505, firsthand check_i18n_siblings.py --all : 168 paires, 166 byte-identical + 2 OK-CONSUMER, 0 drift / 0 orphan, 1 « unbuilt » = Peters v4.27 INTRINSIC exception #7081). L’ancien backlog « 4 lakes EN-dominants » (cooperative_games_lean, social_choice_lean, stable_marriage_lean, decision_theory_lean) est obsolète post-#4365 (GT 6→2) : cooperative_games_lean/stable_marriage_lean absorbés dans game_theory_lean/ (leaves ont _en), social_choice_lean vide (absorbé), decision_theory_lean done (12/12). sudoku_lean pilote done (4/4). « Pas de _en sibling » ≠ « gap i18n » : les root aggregators (ex. CooperativeGames.lean, Grothendieck.lean, Finiteness.lean — imports-only + docstring FR, 0 déclaration) sont FR-only by design (#5883), les leaves _en étant auto-découverts par globs. Source de vérité = le checker canonique, pas une liste statique.

Retour au sommet