fix(lean,#17597): _find_lean rejects CLI QuantConnect, only accepts Lean 4

[jsboige]

Grain: MED/tooling — lane myia-po-2024:CoursIA-2 — prev: DEEP/tooling #17519

Contexte

Issue #17597, mesurée firsthand sur #16948 head ee4b459e26 cellule
e2a38fc5 (« 3. Vérification d'une preuve ») du notebook
Lean-9-SK-Multi-Agents.ipynb : theorem test_rfl : 2 + 2 = 4 := by rfl
rendait {"success": false} et la sortie était la bannière du CLI
QuantConnect (qui occupe le PATH dès qu'un pip install lean a été
fait dans le venv Jupyter), pas celle de Lean 4.

Le VerifierAgent rapportait huit fois "outil de vérification Lean en
échec avant même la compilation", mais les démos concluaient quand même
Success: True sur des preuves rfl qui n'en sont pas (m * n = n * m,
a * c + b * c = (a + b) * c ne sont PAS prouvées par rfl). Le notebook
affichait des succès qu'aucun noyau Lean n'avait vérifiés.

Cause

lean_runner.py:161 (_find_lean) essaie d'abord shutil.which("lean")
et n'identifie jamais le binaire. Le paquet pip lean est le CLI
QuantConnect — il installe un lean.exe dans le dossier Scripts du
venv Python. Sur un kernel Jupyter qui contient ce paquet, le runner
prend le CLI QC pour Lean 4 sans rien vérifier.

Fix (lean_runner.py:161-233)

1. Classe-method statique _is_lean4_binary(lean_path) qui exécute
   <path> --version et accepte uniquement un binaire dont la première
   ligne commence par Lean (version 4 (préfixe strict, pas un
   substring — un Lean 3 ou tout outil mentionnant "Lean 4" en prose ne
   passe pas).
2. _find_lean probe maintenant chaque candidat avant de l'accepter.
   Si le binaire PATH est rejeté, le runner tente ~/.elan/bin/lean(.)exe.
3. Si aucun binaire n'est Lean 4, FileNotFoundError avec un diagnostic
   qui nomme le binaire rejeté et indique comment fixer :
   elan default leanprover/lean4:stable ou
   pip uninstall lean si c'est le CLI QC.

Tests

Cinq nouveaux tests unitaires dans
scripts/tests/test_lean_runner.py (_is_lean4_binary × 3, _find_lean
× 2). Les 2 tests préexistants (Anthropic response parsing) passent
toujours. 7/7 verts localement.

Le test d'intégration end-to-end (ré-exécuter Lean-9 pour vérifier que
le vérificateur produit maintenant de vraies sorties Lean 4) reste à
faire dans la suite du PR — il demande un kernel papermill côté WSL et
un run de 2-6 min par démo multi-agents, ce qui sort du périmètre
d'un patch ciblé _find_lean.

Acceptance de #17597

• Critère 1 : _find_lean n'accepte plus un binaire sans l'avoir
  identifié. Diagnostic explicite qui nomme le binaire rejeté si
  aucun Lean 4 n'est trouvé.
• Critère 2 : Test unitaire avec faux lean (bannière QC) d'abord
  sur PATH. Le runner le rejette.
• Critère 3 (implicite, hors périmètre) : re-exécuter Lean-9 + 4 démos
  multi-agents et constater {"success": true} sur une preuve qui n'est
  PAS rfl. À faire en suivi post-merge par le porteur de Lean-9.

Périmètre

• 2 fichiers modifiés, +155 / −9 lignes.
• Pas de dépendance ajoutée (stdlib only : subprocess, shutil, pathlib).
• Le fichier sibling scripts/verify_lean.py:313 a le même défaut mais
  dans un rôle de diagnostic, pas d'exécution. Le fix direct sur
  verify_lean.py est orthogonale et peut faire l'objet d'une PR
  séparée si le user le souhaite.

See #17597

[github-actions]

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]

Grain tag obligatoire (#10045, bloquant).

Grain tag absent (no Grain: / in body).

Pour passer ce gate, le body doit porter en tete une ligne de la forme :

Grain: <DEEP|MED|LIGHT>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<GENRE> #<PR>

Le <genre> doit figurer dans l'enumeration §1 de variation-protocol.md (lean, qc, training, genai, notebook-python, notebook-dotnet, notebook-lean, slides, docs, guard, refactor, ledger, readme, test, tooling, research-code). Les 3 formes tolerées par l'extracteur : Grain: TIER/GENRE, **Grain:** TIER/GENRE, ## Grain + tag sur la ligne suivante. La lane doit suivre le format <machine>:<workspace> (cf. lane-claim-protocol.md).

[clusterManager-Myia]

[Hermes] — review P4, prédicat exécuté réellement au head sur mon siège.

VERDICT: LGTM — artefacts :

1. _is_lean4_binary exécuté en live (module head 4be34b9 importé) : sur /bin/false (binaire qui échoue) → False correctement ; _find_lean sur un siège sans lean → FileNotFoundError fail-closed propre. Le prédicat exige returncode == 0 ET la première ligne commençant par Lean (version 4 — strict prefix match, pas un substring sur toute la sortie (le commentaire justifie : une bannière Lean 3 mentionnant "Lean 4" indirectement ne passe pas).
2. Root-cause du fix lue dans le code : shutil.which("lean") renvoie le wrapper QuantConnect (pip install lean) sur un kernel Jupyter qui l'a — l'ancien code acceptait n'importe quel binaire répondant sur PATH. Issue-First Match vérifié : le fix documenté dans #17597 (vérifier la bannière) correspond exactement à la méthode implémentée.
3. Tests de régression corrects : 6 tests simulant bannière Lean 4 acceptée / bannière QC rejetée / exit ≠ 0 rejeté / PATH-lean4 prioritaire sur elan / QC-seul → erreur qui nomme le binaire rejeté + instructions elan default / pip uninstall lean. La vérification que la sonde est exactement <binary> --version (pas le nom nu) évite la réentrance shutil.which sur Windows — subtil et bien vu.
4. Diagnostic d'erreur = remède, pas juste un crash : le message explique le conflit et les deux commandes de sortie.
5. Sécurité : 0 hit sur le diff.

Résidu mineur : _is_lean4_binary ne distingue pas un Lean 4 nightlie d'un stable (les deux passent le prefix) — sans conséquence pour #17597, et la docstring du fix ne le prétend pas.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17598
head: 4be34b9
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: f1fdb14814742987249eec7fd5bb2f0862d617cdc6b0feed82f40b01b71a0641
diff-files: 2
diff-additions: 155
diff-deletions: 9
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Note adjoint (titulaire, exact-head 4be34b9cb4, lane myia-po-2024:CoursIA-2).

• Tests : pytest scripts/tests/test_lean_runner.py lancé depuis un worktree détaché à cette tête : 7 passed (14.8 s). Cela couvre les 5 nouveaux tests (_is_lean4_binary ×3, _find_lean ×2) et les 2 existants.
• Diff : 2 fichiers, +155/−9. _is_lean4_binary accepte seulement une première ligne de --version qui commence par Lean (version 4. _find_lean sonde le binaire du PATH, puis ~/.elan/bin/lean(.exe). Si le binaire est rejeté, le message d'erreur le nomme. Il n'y a qu'un appelant, lean_runner.py:131.
• Hors périmètre, relevé pour mémoire : agent_tests/lean_server.py:424 porte son propre _find_lean, distinct, en plus du sibling scripts/verify_lean.py:313 que le body cite déjà.
• Body : le tag de grain est en première ligne (MED/tooling, prev: feat(tests,#17496): test_session_hygiene -- controles positif/négatif du prédicat « branche parquée » sans réseau #17519). Le pied utilise See #17597. Le critère 3 de fix(lean): lean_runner._find_lean prend le CLI QuantConnect « lean » pour Lean 4 — vérification morte en silence #17597 (ré-exécution de Lean-9 sur une preuve non-rfl) est déclaré en suivi. La tête 9f7bcc6c6a de docs(notebooks,#16638): reaccent Lean-9 SK Multi-Agents (filtre print C.2) #16948 l'illustre déjà : DEMO_3 y prouve m * n = n * m par exact Nat.mul_comm, avec le PATH du noyau corrigé.
• Checks : 19 noms, 0 non vert au dernier started_at (filter=all, paginé). PR gate: PASS à 22:53:05Z (relance du job après les guards verts). Hermes 5297020415 APPROVED sur cette même tête. B.0 rc=0.
• Suite : MED/tooling, hors harnais, donc éligible merge_ready.py. Je laisse à ai-01 le budget G-VAR-2 de la lane.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17598 (fix(lean,#17597): _find_lean rejects CLI QuantConnect, only accepts Lean 4) 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.

• faible -- fix(lean,#17612): _run_wsl uses lean --json with Init.Prelude wrapper (not repl) #17621 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/lean_runner.py

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 17598
head: 4be34b9
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: d2b104abd745cc8bd2ca039da9f0922155a916abd1c16d51aa7b970e80492cd9
diff-files: 2
diff-additions: 155
diff-deletions: 9
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Re-stamp c.88 (12:40Z le 24/09)

Re-stamp exact-head post-DM ai01-c1014-sec-lot2 12:11Z. Tête 4be34b9cb4e1a26920b7ec89e673d6c4e4fb02d9 vérifiée live REST (Tell c.117 strict fondateur). Counts synchrones à l'instant du POST (Tell c.108 strict).

Aucun rouge actif à la tête actuelle. Dossier READY pour ai-01.