rename(#16231): Lean socle -- 12 carnets Lean-01..09b au canon (padding + suffixe de noyau) by myia-ai-01 · Pull Request #18199 · jsboige/CoursIA

myia-ai-01 · 2026-09-28T09:29:22Z

Grain: MED/refactor -- lane myia-ai-01:CoursIA -- prev: MED/tooling #18194

Résumé

Tranche socle de la série Lean (#17545), au canon du chantier #16231 : les douze carnets Lean-1 à Lean-9b reçoivent leur index à deux chiffres et leur suffixe de noyau. Aucun numéro ne change, l'ordre pédagogique 1 → 9 reste celui d'aujourd'hui ; le padding zéro ne compte pas comme une renumérotation (notebook-accretion-numbering §8).

Table de correspondance postée avant la PR, avec la preuve de chaque suffixe lue dans le code : #17545, commentaire 5866513473. Claim sur les 12 chemins dans le même commentaire.

See #17545 (tranche socle ; sous-séries et descentes en dossiers traitées ailleurs, dont #18015). See #16231.

Ordre de merge

Cette PR ne se merge qu'après #18047 (Lean-1) et #18094 (Lean-4), qui modifient deux des carnets renommés. Après leur merge : git merge origin/main (renommage + modification se fusionnent par détection de renommage), puis nouveau dry-run de l'outil sur la table pour attraper toute référence ajoutée entre-temps.

Ce que fait la PR

Commit	Geste
`8e26cb7d3a`	préalable : le hook `fix-hr-separator` réécrit les séparateurs `---` de tout carnet indexé ; il faisait échouer le commit des `git mv`. Appliqué d'abord, aux anciens chemins : 6 carnets, cellules markdown seules (`---` → `***`, même rendu), code et sorties identiques une fois parsés
`2964cd4ce0`	préalable : `encoding="utf-8"` sur un appel de `scripts/lean/smoke_test_epita_is.py` — le hook `check-subprocess-encoding` refuse tout script indexé sans lui, et l'outil y réécrit des chemins
`9875e77da1`	`git mv` purs, 12 carnets, 12 R100
`815b8835d4`	référents réécrits par surface par `rename_notebooks.py` (63 fichiers, dont `docs/reference/rename-ledger.tsv`)
`d5ada0dbb4`	passe manuelle déclarée sur les 3 carnets que l'outil refuse (section suivante)
`61a425fd28`	`verify_lean.py --filter` ignore le padding : `--filter Lean-2` ne trouvait plus `Lean-02-...` (4 tests rouges) ; `Lean-2` et `Lean-02` sélectionnent désormais le même carnet

Outil utilisé : rename_notebooks.py à la tête de #18194. Ses commits de ce matin évitent trois dégâts que la version de main aurait faits ici :

réécrire docs/archive et docs/ledgers ;
toucher au catalogue à la main ;
casser le --self-test de l'organe output-collapse, qui relit le carnet Lean-7b-Examples.ipynb sous son ancien nom au SHA 6b327a9bf.

Fichiers refusés par l'outil — passe manuelle déclarée

rename_notebooks.py refuse un carnet dont une cellule de code cite un ancien nom (I2/I3 : il ne réécrit jamais du code ni une sortie, parce que changer le code impose une ré-exécution). Trois carnets sont dans ce cas :

Carnet	Cellule de code	Texte cité
`Lean-01-Setup-Lean-Python.ipynb`	6, 11	`print(...)` des noms `Lean-2` à `Lean-8` (cellule 6), `Lean-2` (cellule 11)
`Lean-05-Tactics-Lean.ipynb`	62	commentaire Lean `-- ... Lean-6-Mathlib-Essentials.`
`Lean-10-LeanDojo.ipynb`	63	`print("\nVoir Lean-7-LLM-Integration.ipynb ...")`

Leurs cellules markdown et leur metadata ont été mises à jour par un passage ligne à ligne, avec les mêmes gardes que l'outil après coup (sources de code, sorties et execution_count identiques à l'octet près une fois parsés ; 72 remplacements). Le code et les sorties restent inchangés : ce sont des textes affichés, pas des liens, et leur mise à jour exige une ré-exécution. Elle est tracée dans #18197, ouverte avant cette PR.

Preuves

Organe (worktree de la PR)	rc	Base `main`
`check_kernel_suffix_canon`	0 — `canonical=12`	0
`check_duplicate_notebook_index`	0	0
`check_notebook_navlinks --check --tracked-only`	0 — 0 NEW broken navlink (1432 carnets)	0
`check_series_zero_pad`	0	0
`check_output_collapse --self-test`	0 — replay `56d98429a` intact	0
`pytest test_count_exercises + test_scrub_papermill_paths`	144 passed	144 passed
`pytest Lean/scripts/tests/test_verify_lean.py`	59 passed	59 passed
`check_link_label_agreement --fail`	1 — hérité : constats identiques à la base (`tweety-3`)	1
`check_twin_parity --check`	1 — hérité : `157 \| OK=154 DRIFT=3`, mêmes comptes	1

Hooks pre-commit passés sur les 26 carnets et les 63 référents avant l'application (rc=0).

Plus aucun carnet Lean-<chiffre>- à la racine de la série : Lean pourra être déclaré dans zero_pad_series.json (adopted) une fois cette PR mergée — PR séparée, pour ne pas mêler le registre au renommage.

Catalogue

COURSE_CATALOG.generated.{json,md} : 0 fichier dans le diff — il se régénère après merge. L'outil les aurait réécrits à la main, ainsi que docs/archive et docs/ledgers : défaut corrigé dans #18194 (commit 8f6395a6ce) avant cette application.

🤖 Generated with Claude Code

…le notebooks The fix-hr-separator pre-commit hook rewrites decorative '---' openers (yaml_block_open_no_close) in any staged notebook. Staging the socle renames made it fire inside the pure git-mv commit and fail it. Applying it first, at the old paths, keeps the rename commit a pure R100. Markdown cells only ('---' -> '***', same rendered rule): 6 notebooks, 24 lines; code sources and outputs identical once parsed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The check-subprocess-encoding hook (#13140) refuses any staged .py with a text=True subprocess call lacking encoding=. The socle rename rewrites notebook paths in this script, which stages it and would fail the rename's referent commit. Adding encoding="utf-8", errors="replace" is the fix the hook prescribes (#12811: cp1252 hosts crash on UTF-8 payloads). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Table : C:/Users/MYIA/AppData/Local/Temp/claude/d--CoursIA/bc377615-6e5e-40cd-b0b3-99a8ce1ce438/scratchpad/lean_socle.tsv, pilotee par rename_notebooks.py.

Cellules de code citees : jamais reecrites (re-execution C.2 due). Sorties commitees : jamais touchees.

rename_notebooks.py refuses a notebook whose code cells cite an old name (I2/I3: code and outputs are never rewritten, they need a re-execution). Lean-01-Setup (cells 6, 11), Lean-05-Tactics (cell 62) and Lean-10-LeanDojo (cell 63) are in that case. Their markdown cells and top-level metadata are rewritten here line by line, with the tool's structural guard afterwards: code sources, outputs and execution_count identical once parsed (72 replacements). The printed names in code and outputs stay as they are; their update and re-execution are tracked in #18197. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

After the zero-pad rename, `--filter Lean-2` no longer matched Lean-02-Dependent-Types-Lean.ipynb (plain substring test), and four TestFilterNotebooks tests failed. Leading zeros after a hyphen are now ignored on both sides, so Lean-2 and Lean-02 select the same notebook; matching is otherwise unchanged. test_verify_lean: 59 passed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

github-actions · 2026-09-28T09:30:10Z

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

github-actions · 2026-09-28T09:30:17Z

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-ai-01:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-28) :

GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=3 genre=4 cap=1)
NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

github-actions · 2026-09-28T09:31:25Z

Notebook outputs-required (H.4 schema): PASS (every code cell carries an `outputs: list`)

github-actions · 2026-09-28T09:31:27Z

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	5.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	11.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.9s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	7.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	5.7s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.1s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	29.1s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	8.8s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

github-actions · 2026-09-28T09:31:28Z

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

github-actions · 2026-09-28T09:32:11Z

Notebook PR Validation: PASS

Notebooks checked: 14
Code cells validated: 190
Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

github-actions · 2026-09-28T11:54:46Z

Path-collision (organ #13359/#13615)

Cette PR #18199 (rename(#16231): Lean socle -- 12 carnets Lean-01..09b au canon (padding + suffixe de noyau)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

fort -- rename(#16231,#17545): descente ANALYSE en dossier — 4 carnets + referents (pilote CL1) #18015 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md, _quarto.yml, docs/curriculum/ia-symbolique.md, docs/notebook-metadata/production-scope.md, docs/reference/rename-ledger.tsv, scripts/notebook_tools/pedagogy_density_baseline.json, scripts/tests/baseline_nb_nav_chain.json (issues communes : Remise d'aplomb de la nomenclature des notebooks — suffixe noyau, sans-numero, profondeur d'accretion #16231, [Lean] Gradation du chemin principal a partir de Lean-10 + sous-series (Lean et IA, Conway, verification, formalisations) — fille #5081 #17545)
faible -- feat(notebook-lean): rendre visibles cinq modules EffectiveTheory dans SL-1b #18050 partage : MyIA.AI.Notebooks/SymbolicAI/SymbolicLearning/SL-1b-LogicalLearning-Lean-Native.ipynb
faible -- chore(catalog): scheduled auto-regenerate (long-lived PR) #18202 partage : MyIA.AI.Notebooks/GameTheory/README.md, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md, MyIA.AI.Notebooks/SymbolicAI/README.md, docs/curriculum/ia-symbolique.md
faible -- feat(notebook,#16763): Z3-13b — extraction MUS du Z3-13 (arbitrage 2a) + re-exec C.2 #18217 partage : _quarto.yml, docs/curriculum/ia-symbolique.md, docs/curriculum/symbolic-formalization.md, scripts/tests/baseline_nb_nav_chain.json, slides/03-logique/slides.md
faible -- fix(translations,#18355): Z3-17 re-key + pivot refresh + missing ledger row (T1 tranche 17/3) #18363 partage : docs/reference/rename-ledger.tsv
faible -- docs(lean,#18367): citations Borcherds — Leech/Monstre (16a) + styles (15) (chaîne #18286) #18372 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb

jsboige · 2026-09-29T14:53:55Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18199
head: 9e457fa
complete: REPLACE_WITH_true
body: REPLACE_WITH_read
comments-reviewed: 15
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 3a8ae62923f9946c7d327de391bed059939c324cadd8cb016f247be25245c123
diff-files: 67
diff-additions: 922
diff-deletions: 906
checks: REPLACE_WITH_latest-wins-green_OR_BLOCKED
b0: REPLACE_WITH_clear_OR_blocked
scope: REPLACE_WITH_pass_OR_fail
domain: REPLACE_WITH_pass_OR_not-applicable_OR_fail
verdict: REPLACE_WITH_READY_OR_BLOCKED
[/ADJOINT PREFLIGHT]

Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T14:53:18Z -- Re-stamp READY post-fix GH-IDENTITY-line-1. Update-branch deja applique.

Objet : rename Lean socle -- 12 carnets Lean-01..09b au canon (padding + suffixe de noyau), tranche socle [Lean] Gradation du chemin principal a partir de Lean-10 + sous-series (Lean et IA, Conway, verification, formalisations) — fille #5081 #17545.
Tete exacte : 9e457fa3339dbe2201753975f8e77eb38159fd0e.
Crible item 11/12 : B.0 OK rc=0 firsthand (4 commentaires NON EVALUE info) + gate rc=0.
Note : 67 fichiers diff (922 ajouts / 906 suppressions). 12 R100 + 63 referents surface = 75 fichiers logiques, 67 reels -> renames detectes OK.
Geste attendu ai-01 : merge direct ou merge_ready.

jsboige · 2026-09-29T14:56:37Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18199
head: 9e457fa
complete: true
body: read
comments-reviewed: 16
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 2d424880acebb2b83eb0c99a162a805ac3e5fc04cebf3a01c139d01603808327
diff-files: 67
diff-additions: 922
diff-deletions: 906
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T14:55:58Z -- Re-stamp READY post-fix GH-IDENTITY-line-1. Update-branch deja applique.

Objet : rename Lean socle -- 12 carnets Lean-01..09b au canon.
Tete exacte : 9e457fa3339dbe2201753975f8e77eb38159fd0e.
Crible item 11/12 : B.0 OK rc=0 firsthand (4 commentaires NON EVALUE info) + gate rc=0.
Note : 67 fichiers diff (922/906). 12 R100 + 63 referents = renames OK.
Geste attendu ai-01 : merge direct ou merge_ready.

jsboige · 2026-09-29T14:58:43Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18199
head: 9e457fa
complete: true
body: read
comments-reviewed: 17
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: f28b6b0a959a59a8efae345b5e72d07af393fe4f0f19187fbacf17bd1017723d
diff-files: 67
diff-additions: 922
diff-deletions: 906
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T14:58:25Z -- BLOCKED-cancelled : jambe 'Papermill ratchet (base vs PR)' cancelled (timeout 10 min, 10m09s, declared timeout-minutes: 10). Skill item 5 : 'rerun the CHILD run that owns the job (gh run rerun)'.

Objet : rename Lean socle -- 12 carnets Lean-01..09b au canon.
Tete exacte : 9e457fa3339dbe2201753975f8e77eb38159fd0e.
Verdict : BLOCKED-cancelled-checks (verifie a la tete, surfaces OK).
Note : un dossier BLOCKED-cancelled-checks est un livrable valide (skill item 5). Le job cancelled ne se rejoue pas depuis un dossier : il faut gh run rerun <run_id> --job <job_id> par ai-01 ou un signaleur delegue. Le re-stamp peut alors etre refait apres re-run vert.
Geste attendu ai-01 : gh run rerun la jambe Papermill, puis re-stamp par secretaire une fois latest-wins-green.

jsboige · 2026-09-29T16:24:26Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18199
head: 9e457fa
complete: true
body: read
comments-reviewed: 18
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c2398ba4094578fb0a46d345f1d9d2a2562cc5a70890848524e3c7e78ab3fa5d
diff-files: 67
diff-additions: 922
diff-deletions: 906
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T16:24:16Z -- Re-stamp READY post-DWELL-leve (PR gate SUCCESS a 16:22:49Z, rerun ai-01 a 16:21:56Z).

Tete exacte : 9e457fa3339dbe2201753975f8e77eb38159fd0e (inchangee depuis c.318).
Verdict gate : READY.
Note : dossier c.318 (14:58:43Z) BLOCKED-WITH-SUBSTANCE perime par ce re-stamp (item 13 -- la PR change de verdict, le second dossier est l'autorite). Reunion user a 18:00Z, PR sert la presentation.
Geste attendu ai-01 : merge direct avant 18:00Z.

jsboige · 2026-09-29T16:54:38Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 18199
head: 9e457fa
complete: true
body: read
comments-reviewed: 19
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 11625d7a15f5dc9de2a776af785defc4bfca1288a59e0a26c4f1c5a1e5fb1400
diff-files: 67
diff-additions: 922
diff-deletions: 906
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Dossier urgent demande par ai-01 (DM 15:04Z, reunion user 18:00Z). Tete exacte 9e457fa, PR porteuse lane myia-ai-01:CoursIA -- attestation tierce valide. Renommage zero-pad Lean-1..9 -> Lean-01..09 (67 fichiers +922/-906), aucun numero ne change, label translation-override justifie (c.5892197424). Mesures firsthand : fold latest-wins vert, 0 rouge, 0 jambe en cours (le rouge Papermill ratchet etait un timeout checkout 8 min sur runner myia-po-2026-wsl-3, rejeu 15:05Z passe -- ratchet 15/15) ; B.0 rc=0 ; merge-tree mesure par ai-01 sans conflit dans les deux ordres, 0 lien casse sur l arbre combine. mergeable UNKNOWN au releve (flap connu). Merge et lecture finale a ai-01.

…gen (1182) Conflict on _quarto.yml resolved by taking main side then regenerating via scripts/regen_quarto_render.py: 1182 rendered notebooks = previous 1181 (58 hr-unblocked + refresh backlog) + Lean-20 capstone from #18409, with Lean socle renames from #18199 incorporated. See #18421 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…(voie A) (#18455) * fix(lean,#18437): Lean-05 c.62 -- source 'Lean-6' -> 'Lean-06-Mathlib-Essentials-Lean' (alignement post-#18199) Le commentaire source de la cellule 62 de Lean-05-Tactics-Lean.ipynb mentionnait l'ancien nom Lean-6-Mathlib-Essentials (avant #18199, renommage canon de la serie). Le commentaire est corrige vers le nom canon Lean-06-Mathlib-Essentials-Lean. Les sorties HTML alectryon et text/plain de la cellule 62 restent figees sur l'ancien nom jusqu'a re-execution kernel (voie A). Voir issue de suivi #18453. Note : la regle Stop & Repair (regle 6 secrets-hygiene) interdit de hand-editer la sortie figee ; la voie choisie est (a) modifier la source, (b) ouvrir issue de suivi pour la re-execution kernel (voie A) sur machine equipee du kernel lean4 natif. Grain: DEEP/lean -- lane myia-po-2024:CoursIA-2 -- prev: DEEP/lean c.1311 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#18437): re-execute Lean-05 on ai-01 (lean4 kernel, v4.30.0) -- cell 62 output resynced Voie A of #18437, completing this PR: the cell 62 source rename is now matched by its output. Full papermill run on ai-01, kernel lean4 (toolchain pinned to leanprover/lean4:v4.30.0 for the run, the version the repl binary is built against; stable now resolves to v4.34.1, on which repl fails to parse every cell). - 34/34 code cells with integer execution_count, 0 error outputs - cell 62: new name present in output, old name absent - the 33 other code cells: outputs byte-identical to the previous run - metadata.papermill paths normalised to basenames Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

Lean-01 cells 7 and 12 listed the pre-#18199 notebook names (Lean-2..9 without zero-padding or kernel suffix). Re-executed the python3 cells so their outputs reflect the new names (Lean-02..09b), and corrected the single stale reference in Lean-10 cell 63 (Lean-7-LLM-Integration -> Lean-07-LLM-Integration-Lean-Python). Cell 63 was a pseudo-code snippet referencing non-imported Dojo / ProofFinished / LeanError symbols, so it is now rendered as a markdown fenced block rather than a code cell that never executed under python3-wsl. Lean-05 cell 62 still carries the old name in its alectryon HTML output; that cell is only re-generable on a Lean 4 + Mathlib kernel, so the fix is tracked separately in #18437. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

@16

…025) Arbitrage DM ai01-po2023c2-18440-narrow-20261001 @16:12Z 2026-10-01 : > **#18440 reste ouverte et se recentre sur Lean-10.** Concretement : > 1. remettre MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb > a l'etat de origin/main sur ta branche, en un commit dedie Lean-01-Setup-Lean-Python.ipynb retabli a l'identique de origin/main (tete 78cf736 -- post-#18199 Lean rename, sans kernelspec patch ni re-papermill canonique). Le correctif kernelspec + re-papermill canonique est porte par #18669 chez po-2025:CoursIA-2, qui est CLEAN. #18440 ne touche plus que Lean-10-LeanDojo.ipynb. Echeance 02/10 14:00Z : sans geste d'ici la, Lean-10 passe a po-2025:CoursIA et #18440 fermee avec credit (le revert reste par contre, suivi seul). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> Grain: MED/notebook-lean -- lane myia-po-2023:CoursIA-2 -- prev: MED/notebook-lean #18440-orig

… re-exec C.2 (1/2) (#18669) * fix(lean,#18197): Lean-01 cellules 7+12 -- noms post-renumerotation + re-exec C.2 Les 8 references de cellules de code (liste des carnets + boite finale) citent les noms pre-#18199 ; remplacees par le canon zero-padded avec suffixe de noyau. Re-execution papermill end-to-end (kernel python3, 57 s, 8/8 cellules, 0 erreur, exec_counts 1..8) -- les sorties affichent les nouveaux noms. Lean-05 : deja propre (verifie, grep 0) -- hors perimetre. Lean-10 : suit apres reparation d'env (lean_dojo absent du venv WSL). See #18197 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * Fix: re-exec Lean-01 sous Python 3.11 canonique (kernel drift + ratchet output) - kernel python3 (Store 3.13) -> py311-lean 3.11.16, meme major.minor que la base 3.11.9 - venv WSL repare : ligne parasite export PATH en fin d'activate ecrasait le PATH du venv (pip systeme -> PEP 668) ; retiree, backup activate.bak-pathfix-20261001 - sorties regenerees : cellule 22 retrouve [OK] sans banniere ERREUR ni chemin machine Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fix(lean,#18669): re-exec depuis le dossier du notebook + affichage env hors home (review ai-01 5381446402) - Re-execution via batch_reexecute.py --cwd notebook : la cellule ea71e7c2 retrouve scripts/lean4-kernel-wrapper.py au premier cran de remontee depuis Lean/ ([+] Wrapper robuste deploye, [+] Kernel cree), le chemin machine D:/dev/scripts/... disparait de la sortie. - Chaine WSL elan default passee a v4.33.0 (regle F, review pt 2) : la sonde affiche Lean 4.33.0 (4.11.0 absent). - Cellule 981fa813 : l'affichage raccourcit desormais aussi par sys.prefix (env hors home -> ~/nom-env) ; ce run trouve lean4_jupyter sous home (Store python313) -> affiche ~/AppData/... ; C:/ProgramData absent. - Census sorties base->tete : 6152 -> 5865 caracteres (-287) = suppression de la banniere d'echec '[!] Wrapper script not found' ; 0 output erreur. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>

@16

…n-10 seul) (#18440) * fix(lean,#18420): align print references with #18199 Lean rename Lean-01 cells 7 and 12 listed the pre-#18199 notebook names (Lean-2..9 without zero-padding or kernel suffix). Re-executed the python3 cells so their outputs reflect the new names (Lean-02..09b), and corrected the single stale reference in Lean-10 cell 63 (Lean-7-LLM-Integration -> Lean-07-LLM-Integration-Lean-Python). Cell 63 was a pseudo-code snippet referencing non-imported Dojo / ProofFinished / LeanError symbols, so it is now rendered as a markdown fenced block rather than a code cell that never executed under python3-wsl. Lean-05 cell 62 still carries the old name in its alectryon HTML output; that cell is only re-generable on a Lean 4 + Mathlib kernel, so the fix is tracked separately in #18437. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#18440): re-papermill with coursia-ml-training (kernel drift + papermill ratchet) Re-papermilled both Lean-01-Setup-Lean-Python.ipynb and Lean-10-LeanDojo.ipynb via papermill 2.7.0 with the coursia-ml-training kernel (Python 3.11.16). - metadata.papermill block rewrites fresh (BLOCK_MOVED, not STALE_BLOCK) - language_info.version bumps from 3.11.9 to 3.11.16 (patch drift only, #17371) - kernel-suffix-canon-guard: OK - papermill ratchet: 0 regressions (was 2 STALE_BLOCK) Fail-by-design (documented in body, ack reviewer required): - Split-reading ratchet: SECOND_READING on Lean-10 c.63/c.64 (md conversion) - Exec-sequence ratchet: GAP on Lean-10 c.24 (md conversion) - Notebook catalog drift: GitHub checkout error (submodules not init) - PR gate: aggregates above Refs: Tell c.946-L3 ★★ (papermill metadata block rewrite), Tell c.950-L3 ★★ (own-comment auto-flag neutralization) Grain: MED/notebook-lean -- lane myia-po-2023:CoursIA-2 -- prev: LIGHT/cross-lane-signal c.946 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#18440): re-papermill Lean-01+Lean-10 on python3 (3.13.3) to match base kernel Cherry-picked the c.950 commit (381b4bd) which re-papermilled on coursia-ml-training (3.11.16), then re-papermilled both notebooks on python3 (3.13.3) to match the base language_info.version. Fixes kernel-drift guard red on #18440. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#18440): re-papermill Lean-01+Lean-10 on WSL Python 3.12.3 to match base kernel c.953 first pass used python3 (3.13.3) which still triggered guard: Lean base is python3-wsl (3.12.3). Re-papermilled via WSL coursia-venv (Python 3.12.3) so language_info.version matches the base kernel exactly. Lean-01 kernelspec.name patched python3 -> python3-wsl (matches base). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#18440): patch Lean-01 kernelspec.name to python3 (base) + re-papermill on coursia-ml-training (3.11.16, base=3.11.9 patch drift tolere par #17371) Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * Revert: Lean-01 kernelspec + re-papermill (transfere #18669 chez po-2025) Arbitrage DM ai01-po2023c2-18440-narrow-20261001 @16:12Z 2026-10-01 : > **#18440 reste ouverte et se recentre sur Lean-10.** Concretement : > 1. remettre MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb > a l'etat de origin/main sur ta branche, en un commit dedie Lean-01-Setup-Lean-Python.ipynb retabli a l'identique de origin/main (tete 78cf736 -- post-#18199 Lean rename, sans kernelspec patch ni re-papermill canonique). Le correctif kernelspec + re-papermill canonique est porte par #18669 chez po-2025:CoursIA-2, qui est CLEAN. #18440 ne touche plus que Lean-10-LeanDojo.ipynb. Echeance 02/10 14:00Z : sans geste d'ici la, Lean-10 passe a po-2025:CoursIA et #18440 fermee avec credit (le revert reste par contre, suivi seul). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> Grain: MED/notebook-lean -- lane myia-po-2023:CoursIA-2 -- prev: MED/notebook-lean #18440-orig * fix(lean,#18440): carve-out Split-reading -- fusionner pseudo-code + interpretation Pseudo-code dans cell[62] DMai-01 02:40Z (sujet `ai01-po2023c2-18440-splitreading-20261002`) confirme : le rouge split-reading cellule 3bd10c11 (code -> markdown) de PR #18440 est REEL, pas un flake. Echeance 14:00Z. Option 2 choisie : motiver la conversion dans le body et fusionner les lectures 62-64. Application du mandat ('si on rajoute une lecture, on modifie le paragraphe existant') : fusion de cell[62] (intro Exemple Complet) + cell[63] (pseudo-code, ex-c) + cell[64] (interpretation Pseudo-code, ex-c) en une seule cellule markdown. - cellule 63 (ex-3bd10c11, pseudo-code ```python```) stand-alone collapse en markdown dans cell[62] - cellule 64 (ex-pvi42j6do5, Interpretation : Pattern d'Integration LLM) fusionne en markdown dans cell[62] - cellule 62 (id 51a54161, type markdown, intro Exemple Complet) absorbe le contenu des 2 voisines Validation : - 75 -> 73 cells (decrement 2) - Split-reading ratchet attendu vert apres cycle a 3 markdown consecutifs -> merge inferieur - Markdown only change -> C.2 / papermill re-execution N/A (code cell source only) - Anti-regression : aucun code de production (preuves, fonctions) n'est remplace par sorry/stub, aucune cellule code touchee Refs #18440 (split-reading cellule 3bd10c11), DM ai-01 02:40Z, echeance 14:00Z 2026-10-02. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

jsboige and others added 6 commits September 28, 2026 11:10

rename(#16231): git mv purs (12 notebooks)

9875e77

Table : C:/Users/MYIA/AppData/Local/Temp/claude/d--CoursIA/bc377615-6e5e-40cd-b0b3-99a8ce1ce438/scratchpad/lean_socle.tsv, pilotee par rename_notebooks.py.

rename(#16231): referents reecrits par surface (63 fichiers)

815b883

Cellules de code citees : jamais reecrites (re-execution C.2 due). Sorties commitees : jamais touchees.

myia-ai-01 mentioned this pull request Sep 28, 2026

Lean socle : 4 cellules de code citent un ancien nom de carnet après la renumérotation (re-exécution due) #18197

Closed

github-actions Bot added paragraph-length Paragraph > 2000 chars (wall-of-text, #15405). Resorb before merge. markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. labels Sep 28, 2026

myia-ai-01 mentioned this pull request Sep 28, 2026

[Lean] Gradation du chemin principal a partir de Lean-10 + sous-series (Lean et IA, Conway, verification, formalisations) — fille #5081 #17545

Open

github-actions Bot added the consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) label Sep 28, 2026

github-actions Bot added the pr-overlap Advisory: another open PR touches the same files (organ #13615) label Sep 28, 2026

This was referenced Sep 28, 2026

[Audit #17073] Série Lean — partition Hermes #17357

Open

fix(lean,#17357): sweep pin v4.32.1 -> v4.33.0 -- 8 claims d'etat courant, 7 carnets (Famille A) #18235

Merged

myia-ai-01 mentioned this pull request Sep 29, 2026

Lean-01 : deux print de code annoncent les carnets suivants sous leurs anciens noms (résidu de #18199) #18420

Closed

myia-ai-01 merged commit a513438 into main Sep 29, 2026
105 of 111 checks passed

myia-ai-01 mentioned this pull request Sep 29, 2026

[EPIC] Prover harness co-evolution — forensic-driven robustness (ai-01 ⇄ po-2026) #1453

Open

jsboigeEpita mentioned this pull request Sep 29, 2026

Lean-05 cell 62 : Lean-6 → Lean-06 — sortie alectryon figée sur ancien nom (#18199 follow-up) #18437

Closed

3 tasks

This was referenced Sep 29, 2026

docs(lean,#18413): arborescence README Lean -- Search-03e sorti, Lean-12c/20/37 + ANALYSE/Langlands/Serre100 entres #18439

Merged

fix(lean,#18440): align print references with #18199 Lean rename (Lean-10 seul) #18440

Merged

jsboige mentioned this pull request Oct 2, 2026

fix(lean,#18700): conditionner le statut final sur install_ok et test_ok #18721

Closed

myia-ai-01 mentioned this pull request Oct 3, 2026

kernel drift Lean-9 : interpreter d'execution 3.11.9 (base) absent de la flotte -- aligner le pin #17476

Closed

jsboige deleted the rename/lean-socle-zero-pad branch October 16, 2026 12:28

jsboige mentioned this pull request Oct 18, 2026

[TODO #16262] PRs séparées d'environnement pour F4 substitutions : kernel Lean global-3.13, ANTHROPIC_API_KEY, eth_tester, sales_data.csv #16262

Open

Navigation Menu

Repository navigation

rename(#16231): Lean socle -- 12 carnets Lean-01..09b au canon (padding + suffixe de noyau) - #18199

rename(#16231): Lean socle -- 12 carnets Lean-01..09b au canon (padding + suffixe de noyau)#18199
myia-ai-01 merged 10 commits into
mainfrom
rename/lean-socle-zero-pad

myia-ai-01 commented Sep 28, 2026

Uh oh!

github-actions Bot commented Sep 28, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 28, 2026

Uh oh!

github-actions Bot commented Sep 28, 2026

Uh oh!

github-actions Bot commented Sep 28, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 28, 2026

Uh oh!

github-actions Bot commented Sep 28, 2026

Uh oh!

github-actions Bot commented Sep 28, 2026 •

edited

Loading

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

myia-ai-01 commented Sep 28, 2026

Résumé

Ordre de merge

Ce que fait la PR

Fichiers refusés par l'outil — passe manuelle déclarée

Preuves

Catalogue

Uh oh!

github-actions Bot commented Sep 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Sep 28, 2026

Uh oh!

github-actions Bot commented Sep 28, 2026

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

Uh oh!

github-actions Bot commented Sep 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Golden-Set Execution (H.7 P3)

Uh oh!

github-actions Bot commented Sep 28, 2026

Uh oh!

github-actions Bot commented Sep 28, 2026

Notebook PR Validation: PASS

Uh oh!

github-actions Bot commented Sep 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Path-collision (organ #13359/#13615)

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

jsboige commented Sep 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented Sep 28, 2026 •

edited

Loading

Notebook outputs-required (H.4 schema): PASS (every code cell carries an `outputs: list`)

github-actions Bot commented Sep 28, 2026 •

edited

Loading

github-actions Bot commented Sep 28, 2026 •

edited

Loading