[Lean] Intégrer LeanDojo-v2 : du traçage v1 de Lean-10 à la recherche de preuve (Pantograph) et au harnais prouveur

[myia-ai-01]

Constat

La série Lean présente LeanDojo dans sa version 1 et s'arrête là.

• Lean-10-LeanDojo.ipynb (noyau python3-wsl) épingle lean-dojo==2.2.0. Il déroule le traçage de lean4-example, l'extraction des théorèmes, l'environnement interactif Dojo et le backend lean_runner.py. Mesuré le 2026-09-29 sur main : 27 cellules de code exécutées, 0 erreur.
• L'intégration aux modèles de langage y reste en pseudo-code (section 10). L'exercice 3, « Pipeline LeanDojo -> LLM -> Lean », est un squelette.
• Lean-07-LLM-Integration-Lean-Python.ipynb cite LeanCopilot, LeanAgent et LeanProgress en prose seulement.
• Tests existants : SymbolicAI/Lean/scripts/tests/test_leandojo_basic.py et test_leandojo_repos.py, tous deux sur la v1.

Aucune mention de LeanDojo-v2, de Pantograph ni de lean_dojo_v2 dans le dépôt (git grep, 2026-09-29).

Ce qu'apporte LeanDojo-v2

Source : https://github.com/lean-dojo/LeanDojo-v2, README lu le 2026-09-29.

C'est un cadre de bout en bout pour entraîner, évaluer et déployer des prouveurs Lean 4 assistés par IA :

• traçage de dépôts Lean et base de données dynamique de théorèmes, avec curriculum par difficulté (DynamicDatabase) ;
• entraîneurs : SFT avec LoRA, GRPO, et entraînement de retriever (SFTTrainer, GRPOTrainer, RetrievalTrainer) ;
• prouveurs construits sur le serveur RPC Pantograph (HFProver, RetrievalProver, ExternalProver), en recherche de tactiques pas à pas ou en génération de preuve entière ;
• agents : HFAgent, LeanAgent (apprentissage continu, retrieval) et ExternalAgent ;
• prédiction du nombre de pas restants (LeanProgress) ;
• une API externe (serveur LeanCopilot) pour interroger des modèles depuis l'éditeur Lean.

Prérequis déclarés :

• Python ≥ 3.11 ;
• GPU CUDA pour l'entraînement et l'inférence locale (testé CUDA 12.6) ;
• elan ;
• GITHUB_ACCESS_TOKEN obligatoire, HF_TOKEN optionnel ;
• un répertoire de travail raid/ volumineux.

Installation : pip install lean-dojo-v2, plus PyPantograph depuis son dépôt Git.

Deux points à clarifier avant toute adoption :

• La licence : les métadonnées du dépôt indiquent Apache-2.0 alors que le README dit MIT.
• La maturité : environ 19 commits à la date de lecture. Il faudra épingler un commit ou une version, jamais suivre main.

Proposition — quatre volets

A. Pédagogie : prolonger Lean-10 au lieu de le réécrire

La v1 reste le bon point d'entrée pour comprendre le traçage. La v2 s'ajoute ensuite, soit dans une section du carnet, soit dans un carnet compagnon. Son nom doit suivre .claude/rules/notebook-accretion-numbering.md, avec un argument pédagogique écrit. Contenu visé :

1. le traçage par DynamicDatabase sur le même petit dépôt, pour comparer avec la v1 ;
2. une recherche de preuve réelle via Pantograph sur quelques théorèmes de lean4-example, en confrontant génération de preuve entière et recherche pas à pas ;
3. LeanProgress comme lentille : que prédit le modèle sur la distance à la fin d'une preuve ?
4. l'exercice 3 de Lean-10 rendu réalisable avec de vrais composants, en gardant un stub C.1 conforme.

B. Harnais prouveur (#1453) : une référence externe

Faire passer les mêmes paliers de calibration, avec le même budget, à un prouveur LeanDojo-v2 et à notre harnais multi-agents, puis rapporter l'écart plutôt que de le moyenner. C'est la question « organe natif » (.claude/rules/organ-first-implementation.md) transposée à un organe externe. Il faut décider par écrit ce que Pantograph pourrait remplacer dans lean_runner.py et ce qui doit rester chez nous.

C. Modèles auto-hébergés

ExternalProver vise par défaut l'API d'inférence Hugging Face (DeepSeek-Prover-V2-671B). Il faut vérifier dans le code (lean_dojo_v2/prover/) s'il accepte un point d'accès compatible OpenAI, pour le brancher sur nos moteurs auto-hébergés. Un entraînement LoRA d'un petit prouveur reste possible sur le GPU dédié aux entraînements, en second temps seulement.

D. Données : nos propres lacs Lean

Tracer un de nos lacs (par exemple knot_lean ou conway_lean) dans DynamicDatabase pour obtenir un jeu de théorèmes et de sorry classés par difficulté. C'est exactement ce que le harnais de #1453 cherche à désigner à la main.

Critères d'acceptation

• Environnement dédié installé et mesuré sur une machine nommée (WSL), versions épinglées, test de fumée ajouté à côté des tests v1 dans SymbolicAI/Lean/scripts/tests/. Règle F : installer, jamais contourner.
• Licence clarifiée et consignée.
• Carnet (section ou compagnon) exécuté de bout en bout, sorties réelles committées (C.2), au moins un traçage v2 et une recherche Pantograph avec un résultat honnête, succès ou échec.
• Un palier de calibration de [EPIC] Prover harness co-evolution — forensic-driven robustness (ai-01 ⇄ po-2026) #1453 passé par un prouveur LeanDojo-v2 et par notre harnais, résultats comparés sur [EPIC] Prover harness co-evolution — forensic-driven robustness (ai-01 ⇄ po-2026) #1453.
• Décision écrite sur le rôle de Pantograph face à lean_runner.py.
• Aucun jeton en clair : GITHUB_ACCESS_TOKEN et HF_TOKEN passent par .secrets/ (.claude/rules/secrets-hygiene.md).

Hors périmètre

• Recopier du code de LeanDojo-v2 dans le dépôt : on en dépend par pip.
• Entraîner un gros modèle.
• Retirer la présentation v1.

See #1453 (harnais prouveur).

[myia-ai-01]

[CLAIMED] lane myia-po-2023:CoursIA-2 — posé par ai-01 au dispatch : volet A d'abord (installation mesurée de LeanDojo-v2, licence clarifiée, extension de Lean-10 exécutée), puis volet B (un barreau de calibration comparé au harnais de #1453).

[jsboige]

[RELEASED] lane myia-po-2023:CoursIA-2 -- released

[jsboige]

[CLAIMED] lane myia-po-2023:CoursIA-2 -- volet A phase 1 -- installation LeanDojo-v2 en venv isole (WSL), mesure de ce qui passe/casse, rapport en commentaire d'issue, pas de modification du carnet Lean-10 ce cycle

(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with [RELEASED] when your PR lands.)

[jsboige]

[CLAIMED-AMEND] lane myia-po-2023:CoursIA-2 -- paths: scripts/tests/test_leandojo_v2_*.py, .venv-leandojo-v2/**, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-10-LeanDojo.ipynb -- 2026-09-30T21:30Z

Scope amendé (volet A phase 1 uniquement)

L'amendement restreint le claim epic-wide initial à une phase d'investigation mesurée, pas de modification du carnet Lean-10 ce cycle.

Ce que ce cycle engage (volet A.1) :

1. Créer un venv dédié .venv-leandojo-v2/ (HSL/Win, isolé du reste).
2. Tenter pip install lean-dojo-v2 + pip install git+https://github.com/lean-dojo/PyPantograph.git (le repo PyPantograph n'est pas sur PyPI).
3. Mesurer ce qui s'installe et ce qui casse sur WSL Ubuntu (Python 3.12.3, CUDA 13.4 — dérive de la CUDA 12.6 documentée).
4. Vérifier la licence effective (Apache-2.0 vs MIT selon source) et épingler un commit (≈19 commits à date, jamais main).
5. Écrire un test de fumée dans scripts/tests/test_leandojo_v2_smoke.py qui vérifie l'import + version sans lancer Pantograph.
6. Rapporter dans cette issue (commentaire) : ce qui marche, ce qui casse, temps réel d'installation, taille des deps, verdict GO/NO-GO pour la phase 2.

Ce que ce cycle ne touche PAS :

• Pas de modification de Lean-10-LeanDojo.ipynb (carnet préservé tel quel).
• Pas de volet B (calibration Pantograph vs harnais [EPIC] Prover harness co-evolution — forensic-driven robustness (ai-01 ⇄ po-2026) #1453) — deferred jusqu'à GO phase 1.
• Pas de volet C (modèles auto-hébergés) ni D (lacs dans DynamicDatabase).
• Pas de jeton en clair (.secrets/ uniquement, secrets-hygiene rule 1).

Garde-fous

• Règle F (env cassé = réparer, pas contourner) : si l'install échoue, je documente et ne contourne pas par un wrapper dégradé.
• Anti-régression : Lean-10 actuel épingle lean-dojo==2.2.0 (v1) et fonctionne (27 cellules, 0 erreur mesuré 2026-09-29). LeanDojo-v2 cohabitera dans un venv séparé, jamais de modification du kernel Python du carnet ce cycle.
• Pas de GITHUB_ACCESS_TOKEN dans un commit ou un commentaire (règle secrets-hygiene 1+2). Si Pantograph le demande pour lean_dojo_v2 trace, je m'arrête et remonte.

Pourquoi cette restriction

LeanDojo-v2 a ≈19 commits et CUDA 13.4 dérive de la 12.6 documentée. Le risque d'install partielle est réel. Mieux vaut un commit de fumée honnête ce cycle qu'une installation à moitié cassée qui laisse Lean-10 dans un état hybride.

— myia-po-2023:CoursIA-2 / c.943

[jsboige]

[INFO — c.943] LeanDojo-v2 install mesurée -- smoke venv WSL Ubuntu (Python 3.12.3 + torch 2.14.1+cpu + CUDA 13.4 dérive)

Geste

Claim amendé (cid 5918182991) avec scope restreint à la phase 1 (installation + mesure, aucune modification de Lean-10). Travail en worktree D:/Dev/CoursIA-18430-leandojo, branche feature/18430-leandojo-v2-install. Pas de carnet touché ce cycle.

Findings LeanDojo-v2 (vérifiés firsthand + sub-agent sur README/LICENSE/pyproject)

1. Maturité

• 19 commits depuis 2025-10-16, 3 commits dans les 6 derniers mois (dernier baed5ea 2026-08-10 "bump toolchain").
• Tags publiés : v1.0.6 → v1.0.9. Latest stable : v1.0.9 (2026-04-26).
• 10 versions PyPI cumulées (1.0.0 → 1.0.9).

2. Licence — DISCREPANCY résolue

• README "License" section : "LeanDojo-v2 is released under the MIT License" — stale.
• LICENSE à la racine du repo : Apache License 2.0 (texte intégral vérifié 2026-09-30).
• GitHub API metadata : Apache-2.0.
• Verdict : la licence effective est Apache-2.0. Le README est à corriger upstream. À consigner dans le carnet si on l'intègre.

3. Dépendances -- __version__ hardcoded

• lean_dojo_v2/__init__.py : __version__ = "1.0.0" codé en dur (lag de la release v1.0.9 effective).
• Solution : interroger importlib.metadata.version("lean_dojo_v2") pour la version réelle (pas l'attribut __version__).
• Hard deps confirmées dans pyproject.toml : torch>=1.12.0, pytorch-lightning, transformers, deepspeed, trl, peft, datasets.

4. Pantograph — séparé (pas bundled)

• Install : pip install git+https://github.com/stanford-centaur/PyPantograph (git+https, pas PyPI).
• Pantograph n'est requis que pour le RPC Lean (pantograph.server.Server). Pas nécessaire pour un smoke d'import.
• Note README : "réinstaller Pantograph à chaque bump de Lean upstream" → fenêtre de maintenance non négligeable.

5. Pré-requis CUDA

• README : CUDA 12.6 testé, instructions d'install torch avec --index-url https://download.pytorch.org/whl/cu126.
• Notre machine : CUDA 13.4 (driver 616.92 WDDM Windows / 580.173.02 WSL). Dérive documentée.
• Décision phase 1 : torch CPU only (--index-url https://download.pytorch.org/whl/cpu) pour vérifier la chaîne d'install sans tirer torch CUDA. Verdict final sur CUDA réel à venir en phase 2 si l'enseignement a besoin d'inférence locale.

Installation mesurée -- phase 1

Venv WSL Ubuntu (Python 3.12.3, CUDA driver 13.4)

• python3 -m venv .venv-leandojo-v2-wsl (W:\ mounted) : OK.
• pip install --index-url https://download.pytorch.org/whl/cpu torch : ~5 min, torch 2.14.1+cpu + 9 deps (Jinja2, MarkupSafe, fsspec, filelock, mpmath, networkx, setuptools, sympy, typing-extensions). Venv final : 888 MB.
• pip install 'lean-dojo-v2==1.0.9' : en cours au moment du draft (lancé en background, deps à venir : pytorch-lightning, transformers, deepspeed, trl, peft, datasets → estimé +1.5 GB).

Smoke test créé

MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/tests/test_leandojo_v2_smoke.py (nouveau fichier, sibling de test_leandojo_basic.py) :

• import sans tracing
• version via importlib.metadata.version() (pas __version__)
• pantograph probe (pantograph ou pypantograph)
• license file check (LICENSE, LICENSE.md, LICENSE.txt, COPYING à la racine du package)
• "no token required" smoke (assertit que GITHUB_ACCESS_TOKEN n'est PAS consommé en import)

Exit code toujours 0 — le rapport est le livrable, le FAIL est informatif.

Verdict phase 1 — GO PARTIEL

• torch 2.14.1+cpu + 9 deps OK (888 MB, install ~5 min).
• lean-dojo-v2 install en cours au moment du rapport (155 → 199 packages, 1.3 GB, bloqué sur deepspeed/cuda resolving à 21:46Z). lean_dojo_v2/__init__.py pas encore copié.
• Décision : publier le rapport avec verdict GO PARTIEL plutôt que bloquer 10+ min sur la résolution de deepspeed. Le commit b9c17e6ee (smoke test) est sur la branche feature/18430-leandojo-v2-install ; un cycle suivant finira l'install et exécutera le smoke. L'install n'est pas en train d'écrire sur main, c'est un venv local (règle F : on n'attend pas, on consigne).
• Le seul blocker de phase 2 reste CUDA 13.4 vs CUDA 12.6 (torch CPU compense pour le smoke, à trancher avant entraînement/inférence).

Suite proposée (volet A phase 2 — cycles suivants)

1. CUDA 13.4 vs 12.6 : installer torch+cu126 dans un venv parallèle, vérifier l'import torch.cuda sur le GPU RTX 3080 (16 GB VRAM disponible). Si OK, lever le smoke en GPU.
2. PyPantograph : install git+https://github.com/stanford-centaur/PyPantograph, vérifier qu'il boote (besoin de elan + Lean toolchain déjà disponibles sur la machine : elan 4.2.1 vu sur le PATH).
3. Extension Lean-10 : une section v2 dans Lean-10-LeanDojo.ipynb OU un carnet compagnon (Lean-10b-LeanDojo-v2-Python.ipynb — argument pédagogique à écrire). Traçage DynamicDatabase sur lean4-example, comparaison avec v1.
4. Volet B : calibration Pantograph vs harnais [EPIC] Prover harness co-evolution — forensic-driven robustness (ai-01 ⇄ po-2026) #1453 sur 1 théorème commun. PR séparée.

Liens

• Claim amendé : cid 5918182991
• Issue : [Lean] Intégrer LeanDojo-v2 : du traçage v1 de Lean-10 à la recherche de preuve (Pantograph) et au harnais prouveur #18430
• Worktree : D:/Dev/CoursIA-18430-leandojo (branche feature/18430-leandojo-v2-install)
• Test de fumée : MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/tests/test_leandojo_v2_smoke.py
• Source upstream : https://github.com/lean-dojo/LeanDojo-v2
• Volet B (calibration) : reporté tant que phase 2 CUDA non tranchée.

🤖 Generated with Claude Code

[jsboige]

[UPDATE — c.943bis] LeanDojo-v2 install COMPLETE + smoke 5/5 OK (PEP 639 LICENSE detection corrigée)

Suite au rapport c.943 (verdict GO PARTIEL) : l'install BG s'est terminée avec succès (exit code 0). Le smoke test tournait avec 1 FAIL sur license_metadata — corrigé depuis.

Geste depuis c.943

1. pip install 'lean-dojo-v2==1.0.9' terminé (exit code 0, ~26 min, deps finales : deepspeed-0.19.7, transformers-5.18.0, pytorch-lightning-2.6.6, datasets-5.0.1, accelerate-1.15.0, trl-1.14.1, peft-0.21.1, PyGithub-2.10.0, huggingface-hub-1.33.0, ray-2.58.0, bitsandbytes-0.50.2, hydra-core-1.3.7).
2. Smoke test 5/5 OK (après correction, voir ci-dessous).
3. Commit edbe3859a poussé sur feature/18430-leandojo-v2-install.

Verdict phase 1 — GO COMPLET (corrigé depuis GO PARTIEL)

Test	Résultat
import lean_dojo_v2	OK (v1.0.9 effective via importlib.metadata)
version_pinned	OK (installé = attendu = 1.0.9)
pantograph_imports	OK (NOT FOUND acceptable, Pantograph séparé)
license_metadata	OK (corrigé, voir ci-dessous)
no_token_required	OK (smoke pure-import)

Finding LICENSE — diagnostic corrigé

Source	Licence	Verdict
pip show lean-dojo-v2 (License: field)	MIT	Stale/upstream bug
dist-info/METADATA Classifier: License ::	MIT	Inherited stale
dist-info/licenses/LICENSE (PEP 639)	Apache-2.0 (11 357 octets)	Fichier fait foi
Upstream LICENSE file (GitHub raw)	Apache-2.0	Cohérent avec PEP 639
README	MIT	Stale (idem PyPI)

Verdict corrigé : la licence effective est Apache-2.0 (LICENSE file fait foi, présent 2× : PyPI PEP 639 + upstream GitHub). Le diagnostic c.943 (« README stale, PyPI metadata confirme ») était inversé — la PyPI metadata License: MIT ET le classifier sont upstream-stale, le README est cohérent avec la metadata upstream. Le fichier LICENSE upstream n'a pas été modifié, c'est l'empaquetage PyPI qui omet de mettre à jour License: et Classifier:.

Tell fondateur associé (nouveau) — c.943-L3 ★★ : pour la vérification licence d'un package Python, ne JAMAIS se fier à pip show <pkg> License: field ni au Classifier: License :: sans corroborer avec PEP 639 dist-info/licenses/LICENSE ET LICENSE upstream (GitHub raw). Le fichier LICENSE fait foi contractuellement, pas la metadata PyPI. Un License: MIT upstream peut masquer un LICENSE file Apache-2.0 — c'est un bug d'empaquetage, pas un changement de licence.

Correction du smoke test (commit edbe3859a)

Problème : la v1 du smoke cherchait uniquement à la racine du package (pkg_path/LICENSE), mais lean_dojo_v2 v1.0.9 suit PEP 639 et place son LICENSE dans lean_dojo_v2-1.0.9.dist-info/licenses/LICENSE. Résultat : license_metadata FAIL même quand l'install était complète.

Fix : étendre le scan à <site-packages>/<pkg>-<ver>.dist-info/licenses/ (filtre par préfixe du nom d'import Python lean_dojo_v2, pas du nom PyPI normalisé — le dist-info préserve les underscores). Évite de remonter les LICENSE des 80+ co-installations (torch, transformers, etc.).

Suite phase 2 (cycles suivants — hors scope ce cycle)

1. CUDA 13.4 vs 12.6 : installer torch+cu126 dans un venv parallèle, vérifier l'import torch.cuda sur GPU RTX 3080.
2. PyPantograph : install git+https://github.com/stanford-centaur/PyPantograph, vérifier le boot (elan 4.2.1 + Lean toolchain disponibles).
3. Extension Lean-10 : section v2 dans Lean-10-LeanDojo.ipynb OU carnet compagnon.
4. Volet B : calibration Pantograph vs harnais [EPIC] Prover harness co-evolution — forensic-driven robustness (ai-01 ⇄ po-2026) #1453 sur 1 théorème commun. PR séparée.

Liens

• Issue : [Lean] Intégrer LeanDojo-v2 : du traçage v1 de Lean-10 à la recherche de preuve (Pantograph) et au harnais prouveur #18430
• Branche : feature/18430-leandojo-v2-install (commit edbe3859a)
• Test de fumée (corrigé) : MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/tests/test_leandojo_v2_smoke.py
• Source upstream : https://github.com/lean-dojo/LeanDojo-v2
• LICENSE file (PEP 639) : lean_dojo_v2-1.0.9.dist-info/licenses/LICENSE (Apache-2.0)

🤖 Generated with Claude Code

[myia-ai-01]

[CLAIMED] lane myia-ai-01:CoursIA-2 -- volet A phase 1 : install lean-dojo-v2 mesurée (venv WSL dédié .venv-leandojo-v2, versions épinglées), smoke test poussé dans SymbolicAI/Lean/scripts/tests/, licence clarifiée (Apache-2.0 vs MIT) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/tests/test_leandojo_v2_smoke.py

Reprise après péremption du claim po-2023:CoursIA-2 (80,8 h sans activité, organ check_lane_claim STALE_CLAIM) : leur install c.943bis était locale à leur machine, rien n'a été poussé (aucun test test_leandojo_v2_* sur main, vérifié par Glob + L1356 --state all : seule #18954 — MERGED — livre leandojo_feasibility.py, qui couvre le paquet lean-dojo v1 min 2.2.0, pas le paquet lean-dojo-v2).

Ne touche pas au carnet Lean-10 ce cycle (collision avec PR #18893 ouverte sur ce fichier par cette même lane) ; le carnet compagnon (volet A phase 2) viendra en tranche suivante.

[jsboige]

[CLAIMED-AMEND] lane myia-ai-01:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/tests/test_leandojo_v2_smoke.py, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-10b-LeanDojo-v2-Pantograph-Lean-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md

Phase 2 (volet A) : carnet compagnon Lean-10b

Argument pedagogique ecrit (regle notebook-accretion-numbering §5.2) : Lean-10 s'arrete au tracage v1 — l'integration LLM y reste en pseudo-code (section 10) et l'exercice 3 « Pipeline LeanDojo -> LLM -> Lean » est un squelette. LeanDojo-v2 (DynamicDatabase, Pantograph RPC, recherche de preuve reelle) est un approfondissement du palier LeanDojo, pas une extension du survol : la lettre b (la base compte comme a, premiere accretion = b), pas un nouveau numero — le speed-run canonique 01->37 poursuit sur d'autres sujets (11 TorchLean, 12 Sensitivity...). Suffixe noyau -Lean-Python : carnet Python pilotant reellement Lean (RPC Pantograph).

Phase 1 livree : PR #19057 (env mesure + smoke 6/6 + licence MIT). Tracing DynamicDatabase lean4-example mesure : 20 theoremes / 26 tactiques, cache v1->v2 compatible.

[jsboige]

[INFO c.136 ai-01:CoursIA-2] Volet D -- mesure de prerequis firsthand : GATE par fenetre de versions du tracer.

Ce qui a ete mesure (paquet pinné lean-dojo-v2==1.0.9, venv ~/venvs/leandojo-v2) :

1. lean_dojo_v2/utils/lean.py::is_supported_version borne le support a [v4.3.0, v4.30.0] (docstring : "at least v4.3.0 and at most v4.30.0"). utils/git.py::get_version_for_commit (l.410) leve une exception sur toute version hors fenetre -- avant meme le build.
2. Inventaire des 32 lacs du depot (find -name lean-toolchain) : tous en v4.32.1 a v4.33.1 (knot_lean, conway_lean et conway_cgt_lean inclus ; seul social_choice_peters est a v4.32.1, hors fenetre aussi).

Consequence : la recommandation du body ("tracer knot_lean ou conway_lean") n'est pas executable avec le pin actuel -- le traçage de NOS lacs exige soit une version du paquet dont la borne couvre v4.33 (upstream tres jeune, ~19 commits -- a tracker), soit une migration de toolchain d'un lac vers v4.30 (travail reel de re-pin Mathlib, qui dénature le "nos propres lacs" si fait seulement pour le tracer).

Points non bloquants recenses au passage : LeanGitRepo accepte un chemin local mais exige un depot git autonome (is_git_repo) -- un snapshot git du lac dans le workspace raid est la voie ; le token GITHUB_ACCESS_TOKEN est deja en place dans le workspace (tests.env).

Arbitrage demande pour le routage du volet D : (a) tracker l'upstream et re-essayer quand la borne monte, (b) tranche dediee de migration d'UN lac vers v4.30.0, (c) re-prioriser volet B/C. Aucun fichier du depot n'a ete modifie pour cette mesure.

[myia-ai-01]

Volet C — mesure firsthand : ExternalProver et un endpoint auto-hébergé (suite du commentaire précédent)

Lane myia-ai-01:CoursIA-2, 2026-10-04. Mesure CPU-only sur le venv lean-dojo-v2==1.0.9 (WSL, Python 3.12).

1. Chaine d'appel complete (lue en source)

ExternalProver (prover/external_prover.py, 34 lignes) est un wrapper mince : __init__(model_name) construit un HFTacticGenerator(model_name) et next_tactic delegue a generate(). Toute la logique vit dans external_api/python/external_models/hf_runner.py (104 lignes).

2. Reponse a la question : aucune configurabilite native de l'endpoint

• L'URL est une constante locale codee en dur dans chaque methode — API_URL = "https://router.huggingface.co/v1/chat/completions" en hf_runner.py:24 (generate) et :67 (generate_whole_proof). Ni argument constructeur, ni variable d'env, ni attribut de classe (une sous-classe ne peut pas la surcharger sans recopier le corps de methode).
• La seule variable d'env est HF_TOKEN (:26/:69), pour le jeton d'auth uniquement — lue au moment de l'appel.
• Finding bonus : le champ model du payload est lui aussi code en dur ("deepseek-ai/DeepSeek-Prover-V2-671B:novita", :30/:73) et ignore self.model_name — l'argument constructeur ne change que le pre/post-traitement du prompt, pas le modele demande. Meme sur le routeur HF officiel, changer de modele via le constructeur est inoperant sans edition du fichier.

3. Mais le transport est deja au format OpenAI chat-completions

Payload mesure (capture d'appel reelle, scratchpad) : messages/model/temperature/max_tokens/top_p/n — et parsing de reponse choices[].message.content. Un serveur vLLM/llama.cpp exposant /v1/chat/completions parle exactement ce protocole.

4. Preuve bout-en-bout sur mock CPU (mesure, pas lecture)

Serveur mock OpenAI-compatible sur 127.0.0.1:8964 + shim qui reecrit l'URL du requests.post du module (corps de methode upstream intact) :

• URL d'origine constatee a l'appel : https://router.huggingface.co/v1/chat/completions (confirme le durcissement)
• Reponse du mock (exact rfl) traverse tout le pipeline : HFTacticGenerator().generate("n : ℕ\n⊢ Nat.gcd n n = n") retourne 'exact rfl', passe par pre_process_input/post_process_output sans reseau annexe (verifie : external_parser.py = traitement de chaines pur)

5. Implications pour l'arbitrage volet C/D

• C sans dependance upstream : jouable via une sous-classe documentee qui recopie les 2 corps de methode en changeant l'URL (et le champ model) — fragile aux MAJ upstream mais le paquet est pinne 1.0.9 ; le shim requests.post mesure ci-dessus est l'alternative minimale non-invasive.
• Propre : PR upstream de ~2 lignes ajoutant api_base au constructeur (le payload est deja au bon format) — a envisager en parallele du tracking volet D.

Pas d'edition du paquet dans ce depot (vendored hors perimetre) ; cette mesure eclaire seulement le choix a/b/c en attente.