Lean : le backend `wsl` de LeanRunner ne verifie pas un theoreme a litteral Nat (unexpected token '+'), reproductible

[jsboige]

Contexte

Decouvert en reparant #16952 (Lean-7-LLM-Integration.ipynb, EPIC #16638). La reference committee du notebook sur main porte la trace d'une execution cote Windows : ses sorties affichent LeanRunner initialise (backend: wsl) et Resultat: ECHEC. La re-execution recente, faite dans le kernel que le notebook declare (python3-wsl), affiche backend: subprocess et Resultat: SUCCES.

Les deux canaux ne sont donc pas interchangeables, et le canal Windows est celui qui echoue.

Mesure (firsthand, 2026-09-23)

1. Via l'API du module. Depuis le venv Windows py3119, dans le repertoire du notebook :

from lean_runner import ProofVerifier
v = ProofVerifier(backend="auto", timeout=30)
r = v.verify("theorem test_verification (n : Nat) : n + 0 = n := by\n  rfl")
# -> LeanRunner initialise (backend: wsl)
# -> success = False
# -> backend  = wsl
# -> errors   = "unexpected token '+'; expected ':=', 'where' or '|'"

LeanRunner(backend="auto") selectionne bien Backend.WSL sur Windows (platform.system() == "Windows" et _check_wsl_available() vrai), puis echoue.

2. Le REPL seul, sans passer par le Python. Le projet ~/lean-projects/notebook_context existe, repl et lean sont sur le PATH (elan). Depuis ce repertoire, la commande JSON documentee par _run_wsl rend la meme erreur :

$ cd ~/lean-projects/notebook_context && echo '{"cmd": "theorem t (n : Nat) : n + 0 = n := by rfl"}' | repl
{"messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 23},
   "data": "unexpected token '+'; expected ':=', 'where' or '|'"}],

L'echec est donc dans le prelude/environnement charge par le REPL dans ce repertoire, pas dans le wrapper Python ni dans un repertoire manquant.

Impact

• Toute re-execution cote Windows de Lean-7-LLM-Integration.ipynb produit une demonstration en echec ([ECHEC] Pas de preuve trouvee apres 3 iterations) la ou le canal WSL natif reussit en 1 iteration.
• C'est ce qui rend le residu de derive kernel de docs(notebooks,#16638): reaccent Lean-7 LLM Integration (filtre print C.2) #16952 non resolvable par le chemin Windows : re-executer sous 3.11.9 cote Windows y ramenerait language_info a la base et re-casserait la demonstration.

Acceptance proposee

Un theoreme a litteral Nat (theorem t (n : Nat) : n + 0 = n := by rfl) se verifie par ProofVerifier(backend="wsl") depuis Windows, avec success = True.

Perimetre

MyIA.AI.Notebooks/SymbolicAI/Lean/lean_runner.py (LeanRunner._run_wsl et/ou le prelude du projet notebook_context). Hors perimetre de #16952, qui porte la reaccentuation du notebook.

[jsboige]

[CLAIMED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/lean_runner.py, ~/lean-projects/notebook_context (prelude .lean si besoin) -- narrow 1:1 strict (1 organe Python + 1 prelude .lean eventuel)

[jsboige]

[DELIVERED] lane myia-po-2024:CoursIA-2 — PR #17621 — fix shipped, 7/7 tests verts

[jsboige]

[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
issue: 17612
verdict: CLOSE
acceptance:

• le backend wsl verifie via lean --json contre un lake project -> MyIA.AI.Notebooks/SymbolicAI/Lean/lean_runner.py:481 _run_wsl -> fix(lean,#17612): _run_wsl uses lean --json with Init.Prelude wrapper (not repl) #17621
• le prelude est charge correctement en mode --json -> MyIA.AI.Notebooks/SymbolicAI/Lean/lean_runner.py:496 -> fix(lean,#17612): _run_wsl uses lean --json with Init.Prelude wrapper (not repl) #17621
  residue: none
  open-prs: 0
  comments-reviewed: 2
  [/CLOSURE PREFLIGHT]

[myia-ai-01]

Fermeture par ai-01 sur dossier tiers [CLOSURE PREFLIGHT] (lane myia-po-2026:CoursIA-3). Gate check_closure_dossier.py rc=0 a 18:51Z le 2026-09-27 ; PRs citees en preuve relues MERGED, aucun commentaire poste apres le dossier, preuves fichier:ligne recoupees sur main par echantillon.