Lean-10b — LeanDojo-v2 : du tracage a la recherche de preuve (Pantograph)

Ce carnet approfondit Lean-10 (accrétion b : la base compte comme a). Lean-10 s’arrête au traçage v1 de lean-dojo==2.2.0 : l’intégration aux modèles de langage y reste en pseudo-code (section 10) et l’exercice 3 — « Pipeline LeanDojo → LLM → Lean » — y est un squelette. Ici, nous passons au cadre LeanDojo-v2 : base de théorèmes dynamique (DynamicDatabase), serveur RPC Pantograph, et une recherche de preuve réelle, pas à pas et en preuve entière.

Argument pédagogique : ce contenu sort du chemin principal (le survol canonique 01→37 poursuit sur TorchLean, Sensitivity…) — il approfondit le palier LeanDojo pour qui veut construire un prouveur. D’où une lettre, pas un nouveau numéro.

Position dans la série : Lean-10b vient après Lean-10 et avant Lean-11. Prérequis : avoir exécuté Lean-10 (traçage v1, environnement Dojo).

Prérequis et versions épinglées

Environnement dédié (installé selon la règle F — installer, jamais contourner) :

Composant	Version épinglée	Rôle
`lean-dojo-v2`	`1.0.9` (PyPI)	cadre complet : tracage, base dynamique, provers, agents
`pantograph`	`0.3.15` (depuis `git+.../PyPantograph`)	serveur RPC Lean (tactiques, buts, compilation)
`torch`	`2.14.1`	entraînement/inférence (local, CPU ici)
Lean (elan)	`4.34.1`	outil invoqué par Pantograph
Python	`3.12.3` (WSL)	≥ 3.11 requis par `lean-dojo-v2`

Licence : MIT — métadonnées PyPI (license=MIT) et README du dépôt, mesurées le 2026-10-04 (la discordance Apache-2.0/MIT signalée à la découverte du projet est résolue : les deux sources disent MIT).

Le jeton GITHUB_ACCESS_TOKEN est requis à l’import de lean_dojo_v2 (le tracage interroge l’API GitHub) ; il est chargé depuis un .env gitignored, jamais écrit en dur.

import os
from pathlib import Path

# Pantograph invoque le binaire `lean` d'elan : le rendre visible du kernel.
os.environ["PATH"] = os.path.expanduser("~/.elan/bin") + ":" + os.environ["PATH"]

# Jeton GitHub : requis a l'import de lean_dojo_v2. Lu depuis le .env du repo
# (gitignored) ou sa copie du repertoire de travail -- jamais affiche.
_tests = Path("MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/tests/.env")
for _candidate in (_tests, Path.home() / "leandojo-v2-work" / "tests.env"):
    if _candidate.exists():
        for _line in _candidate.read_text().splitlines():
            if _line.startswith("GITHUB_ACCESS_TOKEN="):
                os.environ["GITHUB_ACCESS_TOKEN"] = _line.split("=", 1)[1].strip()
        break
print("token present:", bool(os.environ.get("GITHUB_ACCESS_TOKEN")))
print("lean on PATH:", bool(os.popen("which lean").read().strip()))

# Repertoire de travail dedie : le tracage ecrit raid/ et dynamic_database.json
# dans le cwd -- on l'envoie hors du depot.
os.chdir(Path.home() / "leandojo-v2-work")
print("repertoire de travail :", Path.cwd().name)

token present: True
lean on PATH: True
repertoire de travail : leandojo-v2-work

import importlib.metadata

import lean_dojo_v2  # noqa: F401 -- l'import lui-meme valide l'environnement

for _pkg in ("lean-dojo-v2", "pantograph"):
    print(_pkg, "==", importlib.metadata.version(_pkg))

_meta = importlib.metadata.metadata("lean-dojo-v2")
print("licence:", _meta.get("License"))

lean-dojo-v2 == 1.0.9
pantograph == 0.3.15
licence: MIT

1. `DynamicDatabase` : le tracage v2, avec mémoire

En v1 (Lean-10), trace() produit un instantané figé d’un dépôt. En v2, la base dynamique garde les dépôts tracés, les théorèmes et leur sorry, et sait trier par difficulté — un curriculum pour l’apprentissage continu. Nous traçons le même petit dépôt lean4-example qu’en Lean-10 pour comparer.

import os
import sys

from lean_dojo_v2.database import DynamicDatabase
from loguru import logger as _loguru

# Affichage : lean_dojo_v2 journalise via loguru ; le sink par defaut emet
# tout (DEBUG) sur stderr, chemins absolus compris (cache, repertoire de
# travail). On ne garde que WARNING et au-dela. tqdm desactive : ses barres
# de progression n'apportent rien au rendu.
_loguru.remove()
_loguru.add(sys.stderr, level="WARNING")
os.environ["TQDM_DISABLE"] = "1"

url = "https://github.com/durant42040/lean4-example"
commit = "3e23ab0bfdcfdbd5b11ab53c2cd8b5d16492e9c2"

database = DynamicDatabase()
database.trace_repository(url=url, commit=commit, build_deps=False)
print("tracage termine")

 [WARNING]  fp_quantizer compatibility check failed (CUDA_HOME does not exist, unable to compile CUDA op(s)), treating the op as not compatible

 [WARNING]  transformer_inference compatibility check failed (CUDA_HOME does not exist, unable to compile CUDA op(s)), treating the op as not compatible

 [WARNING]  inference_core_ops compatibility check failed (CUDA_HOME does not exist, unable to compile CUDA op(s)), treating the op as not compatible

 [WARNING]  cutlass_ops compatibility check failed (CUDA_HOME does not exist, unable to compile CUDA op(s)), treating the op as not compatible

 [WARNING]  ragged_device_ops compatibility check failed (CUDA_HOME does not exist, unable to compile CUDA op(s)), treating the op as not compatible

 [WARNING]  ragged_ops compatibility check failed (CUDA_HOME does not exist, unable to compile CUDA op(s)), treating the op as not compatible

 [WARNING]  spatial_inference compatibility check failed (CUDA_HOME does not exist, unable to compile CUDA op(s)), treating the op as not compatible

tracage termine

print("depots:", database.repositories)
print("API publique:", [a for a in dir(database) if not a.startswith("_")])

depots: []
API publique: ['SPLIT', 'add_repository', 'delete_repository', 'discover_repositories', 'export_merged_data', 'from_dict', 'from_json', 'get_repository', 'json_path', 'print_database_contents', 'repositories', 'sort_repositories_by_difficulty', 'to_dict', 'to_json', 'trace_repository', 'update_json', 'update_repository']

import json
from pathlib import Path

data_dir = Path.home() / "leandojo-v2-work" / "raid" / "data" / "lean4-example_3e23ab0bfdcfdbd5b11ab53c2cd8b5d16492e9c2"
split = json.loads((data_dir / "random" / "train.json").read_text())
items = split["theorems"] if isinstance(split, dict) else split
print("theoremes (train, split random):", len(items))
first = items[0]
print("premier theoreme  :", first["full_name"])
print("enonce            :", first["theorem_statement"][:90])
print("tactiques tracees :", len(first["traced_tactics"]))

theoremes (train, split random): 12
premier theoreme  : mul_assoc_my_4
enonce            : theorem mul_assoc_my_4 : ∀ a b c : Nat, (a * b) * c = a * (b * c) :=
tactiques tracees : 3

Lecture du résultat : les trois cellules ci-dessus se lisent ensemble. depots: [] n’est pas un échec : trace_repository trace le dépôt et exporte le résultat sur disque, mais n’inscrit pas le dépôt dans le registre en mémoire — c’est le rôle d’add_repository (visible dans l’API publique affichée). Le produit de l’appel vit sous le répertoire de travail choisi à l’installation : raid/data/<dépôt>/ reçoit les splits random/ et novel_premises/, un metadata.json et le manifeste traced_files.jsonl ; le registre sérialisé dynamic_database.json reste vide pour la même raison. Le WARNING ... No traced files found émis pendant l’appel vient de l’export de prémisses (export_premises — corpus.jsonl reste vide ici) ; il ne concerne pas les tactiques tracées, que la relecture du split train montre : 20 théorèmes dont les preuves humaines totalisent 40 pas de tactique (section 3), exportés en jeux train/val/test selon deux stratégies — découpage aléatoire (random) et découpage par prémisses nouvelles (novel_premises : les théorèmes de test utilisent des lemmes absents du train, un vrai test de généralisation). Le témoin établit la provenance immédiate des fichiers : depuis un répertoire de travail vierge (cache conservé), le même appel réécrit tout l’arbre raid/data/<dépôt>/, splits compris — c’est bien lui qui produit ces fichiers. Le tracage initial vit dans le cache préexistant (~/.cache/lean_dojo) : l’origine de son remplissage n’est pas vérifiée par ce carnet, qui réexporte sans retracer. C’est l’API du curriculum qui manquait à la v1 : en Lean-10, il fallait écrire cette plomberie à la main ; l’inscription (add_repository) et le tri par difficulté restent à exécuter (volet D).

2. Pantograph : le RPC Lean

Pantograph est le serveur derrière les provers de LeanDojo-v2. Plutôt que de générer une preuve en aveugle, on dialogue avec Lean : on soumet un but, on applique une tactique, on observe le nouvel état — jusqu’à fermeture. C’est l’interface exacte qu’un LLM piloterait.

Note d’exécution : dans un kernel Jupyter, la boucle d’événements tourne déjà ; on utilise donc l’API asynchrone de Pantograph (restart_async, goal_start_async, goal_tactic_async, check_compile_async) — les enveloppes synchrones lèveraient RuntimeError: This event loop is already running.

from pantograph.server import Server

# API async : voir la note ci-dessus.
server = Server(_sync_init=False)
await server.restart_async()
# r-string : `and` s'ecrit /\ en Lean -- sans le prefixe r, Python traiterait
# l'antislash comme un debut d'escape (SyntaxWarning).
goal = r"forall (p q : Prop), p /\ q -> q /\ p"
state = await server.goal_start_async(goal)
print("but initial :")
print(state)

but initial :

⊢ forall (p q : Prop), p /\ q -> q /\ p

# Recherche PAS A PAS : chaque tactique est appliquee et verifiee par Lean.
# Le but quantifie p, q, puis l'hypothese h : on les introduit d'un seul coup.
state = await server.goal_tactic_async(state, "intro p q h")
print("apres intro p q h :")
print(state)

apres intro p q h :
p : Prop
q : Prop
h : p ∧ q
⊢ q ∧ p

# Fermeture du but : h : p /\ q, le but q /\ p se ferme par la paire <h.2, h.1>.
state = await server.goal_tactic_async(state, "exact ⟨h.2, h.1⟩")
print("etat final :", repr(str(state)))
print("preuve fermee :", str(state).strip() == "")

etat final : ''
preuve fermee : True

Pas à pas vs preuve entière : la version pas à pas expose chaque état intermédiaire — c’est le mode recherche (le modèle propose, Lean vérifie, on recommence) ; la version preuve entière (whole-proof generation) demande au modèle de tout produire d’un coup. Pantograph vérifie les deux : une tactique invalide échoue immédiatement (TacticFailure) au lieu de laisser un fichier .lean cassé.

# PREUVE ENTIERE : on soumet un module complet a la compilation.
# En forme termee (fun _ => ...) l'elaboration echoue ; en forme tactique
# (`by exact ...`), la compilation passe -- mesure c.133.
code_lean = r"theorem and_comm_10b (p q : Prop) (h : p /\ q) : q /\ p := by exact ⟨h.2, h.1⟩"
units = await server.check_compile_async(code_lean)
erreurs = [m for u in units for m in u.messages if m.severity.name == "ERROR"]
print("unites compilees :", len(units))
for _m in erreurs:
    print("severite :", _m.severity, "-", _m.data[:120])
print("compile sans erreur :", not erreurs)

unites compilees : 1
compile sans erreur : True

3. LeanProgress : combien de pas reste-t-il ?

Avant de lancer une recherche coûteuse, un bon prouveur sait estimer la distance à la fin. Le tracage v2 fournit la donnée brute : pour chaque théorème, le nombre de tactiques réellement utilisées par la preuve humaine. C’est l’étiquette exacte qu’entraîne ProgressTrainer (tête de régression sur bert-base-uncased — l’entraînement exige un GPU, hors périmètre de ce carnet CPU ; voir le verdict INTRINSIC-GPU documenté dans agent_tests/prover/integration/leandojo_feasibility.py).

steps = []
for name in ("train", "val", "test"):
    split_data = json.loads((data_dir / "random" / (name + ".json")).read_text())
    entries = split_data["theorems"] if isinstance(split_data, dict) else split_data
    steps.extend(len(t["traced_tactics"]) for t in entries)
print("pas de preuve par theoreme (split random) :", steps)
print("distribution : min", min(steps), "| max", max(steps), "| total", sum(steps))

pas de preuve par theoreme (split random) : [3, 1, 1, 3, 1, 3, 3, 3, 1, 3, 3, 1, 1, 1, 3, 3, 3, 1, 1, 1]
distribution : min 1 | max 3 | total 40

4. L’exercice 3 de Lean-10, enfin réalisable : le pipeline complet

Le pipeline « LeanDojo → LLM → Lean » tient en trois briques réelles : (1) le tracage fournit les théorèmes d’entraînement, (2) une politique propose une tactique pour chaque état de but, (3) Pantograph applique et vérifie. Ici, la politique est une table déterministe (l’objectif est de montrer la tuyauterie, pas le modèle) : chaque proposition passe quand même par la vérification Lean.

POLITIQUE = {
    r"forall (p q : Prop), p /\ q -> q /\ p": ["intro p q h", "exact ⟨h.2, h.1⟩"],
}

async def preuve_par_politique(server, enonce, tactiques):
    state = await server.goal_start_async(enonce)
    trace = []
    for tac in tactiques:
        state = await server.goal_tactic_async(state, tac)
        trace.append((tac, str(state).strip().replace("\n", " | ")[:80]))
    return trace

for enonce, tacs in POLITIQUE.items():
    for etape in await preuve_par_politique(server, enonce, tacs):
        print(etape)

('intro p q h', 'p : Prop | q : Prop | h : p ∧ q | ⊢ q ∧ p')
('exact ⟨h.2, h.1⟩', '')

Exercices

Exercice 1 — Remplacer la table par un vrai modèle. La fonction choose_tactic doit interroger un LLM (API locale ou distante) avec l’état du but et rendre une tactique. La boucle de vérification Pantograph reste inchangée — c’est tout l’intérêt du pipeline.

Exercice 2 — Tracer un autre dépôt. Reprendre la cellule de tracage avec le dépôt https://github.com/lean-dojo/lean4-example (le dépôt historique de la v1) et comparer les théorèmes extraits.

Exercice 3 — Recherche en largeur. Écrire une recherche best-first : depuis un état de but, essayer une liste de tactiques candidates, ne garder que celles qui passent, itérer jusqu’à fermeture ou budget épuisé.

# Exercice 1 -- a completer
def choose_tactic(goal_state_text: str) -> str:
    # TODO etudiant : interroger un LLM avec goal_state_text et rendre une tactique
    # Indice : le format d'appel est libre ; la securite vient de Pantograph (TacticFailure)
    print("Exercice a completer")
    return None  # TODO etudiant

# Appel temoin : la signature est valide telle quelle (stub C.1, sans erreur).
print(choose_tactic("p : Prop, q : Prop, h : p ∧ q ; but : q ∧ p"))

Exercice a completer
None

# Exercice 2 -- a completer
def tracer_autre_depot(url: str, commit: str):
    # TODO etudiant : tracer avec DynamicDatabase et rendre le nombre de theoremes
    # Etape 1 : creer la base ; Etape 2 : trace_repository ; Etape 3 : compter
    print("Exercice a completer")
    return None  # TODO etudiant

# Appel temoin.
print(tracer_autre_depot("https://github.com/lean-dojo/lean4-example", "a27d9"))

Exercice a completer
None

# Exercice 3 -- a completer
async def recherche_best_first(server, enonce, candidates, budget: int = 10):
    # TODO etudiant : exploration best-first sur goal_tactic_async
    # Indice : une tactique qui ne passe pas leve une exception -- l'echec est informatif
    print("Exercice a completer")
    return None  # TODO etudiant

# Appel temoin.
print(await recherche_best_first(server, goal, []))

Exercice a completer
None

Conclusion| | Lean-10 (v1) | ce carnet (v2) ||—|—|—|| Tracage | instantané figé (`trace`) | `DynamicDatabase` : base dynamique et curriculum par difficulté disponibles par API (inscription non exercée dans ce carnet) || Interaction Lean | `Dojo` (fork du process) | serveur RPC Pantograph (buts, tactiques, compilation) || Intégration LLM | pseudo-code (section 10) | pipeline réel vérifié (politique → `goal_tactic_async`) || Exercice 3 | squelette | réalisable : table remplacée par un modèle (exercice 1) |Ouvertures (issue #18430) : volet B — faire passer les mêmes paliers de calibration à un prover v2 et à notre harnais multi-agents ; volet C — brancher `ExternalProver` sur nos moteurs auto-hébergés (point d’accès compatible OpenAI ?) ; volet D — tracer nos propres lacs (`knot_lean`, `conway_lean`) pour obtenir un jeu de `sorry` classés par difficulté.

Navigation : << Lean-10-LeanDojo | Index | Lean-11-TorchLean >>

Retour au sommet