Lean 10 : LeanDojo - ML/LLM Theorem Proving

Navigation : << Lean-09-SK-Multi-Agents-Lean-Python | Index | Lean-10b-LeanDojo-v2 >>

---

Introduction

LeanDojo est une bibliotheque Python revolutionnaire qui permet l’interaction programmatique avec Lean 4 pour le machine learning et la demonstration automatique de théorèmes. Elle a ete introduite a NeurIPS 2023 et constitue aujourd’hui un outil essentiel pour la recherche en IA mathematique.

Pourquoi LeanDojo ?

La demonstration automatique de théorèmes (Automated Theorem Proving) est l’un des defis majeurs de l’IA. LeanDojo permet de :

Capacite	Description	Intérêt pour l’IA
Tracing	Analyse et extraction de metadonnees d’un depot Lean	Dataset d’entrainement
Theorem Extraction	Liste tous les théorèmes avec leurs types et preuves	Supervision pour ML
Dojo Environment	REPL interactif pour exécuter des tactiques	Reinforcement Learning
Tactic State	Acces a l’état de preuve (goals, hypotheses)	Features pour modèles

Architecture de LeanDojo

LeanDojo
├── LeanGitRepo      # Reference a un depot Git Lean
├── trace()          # Analyse le depot et extrait les metadonnees
├── TracedRepo       # Depot analyse avec acces aux théorèmes
│   └── get_theorems()  # Iterateur sur tous les théorèmes
├── Theorem          # Representation d'un théorème
│   ├── full_name    # Nom complet (ex: Nat.add_comm)
│   ├── file_path    # Fichier source
│   └── code         # Code source Lean
└── Dojo             # Environnement interactif pour prouver
    ├── run_tac()    # Exécute une tactique
    └── TacticState  # État après chaque tactique
        ├── goals    # Liste des buts restants
        └── pp       # Pretty-print de l'état

Prerequis

• Python 3.10-3.12 (pas 3.13+ pour l’instant)
• GitHub token pour eviter le rate limiting de l’API
• ~5 Go d’espace disque pour le cache (Mathlib4 est volumineux)
• WSL sur Windows (recommande pour eviter les blocages)

Duree estimée : 45 minutes

Configuration Principale

Cette cellule centralise tous les switches pour contrôler l’exécution du notebook. Modifiez les valeurs selon vos besoins avant de lancer l’exécution.

Opérations et temps estimes

Opération	Switch	Temps (cache)	Temps (1ere fois)	Description
Tracing	ENABLE_TRACING	1-2 min	5-15 min	Compile et trace le depot Lean
Dojo	ENABLE_DOJO_DEMO	1-2 min	30+ min	Exécute des tactiques interactives
Preuve auto	ENABLE_AUTO_PROOF	Rapide	30+ min	Démontre la preuve automatique

Modes d’exécution suggeres

Mode	Config	Temps total	Usage
Rapide	Tout desactive	< 30 sec	Lecture seule
Demo	Tracing ON	2-3 min	Voir extraction théorèmes
Complet	Tout active	5-35 min	Toutes les fonctionnalites

# =============================================================================
# CONFIGURATION PRINCIPALE - MODIFIEZ CES VALEURS
# =============================================================================

import os

# Cap des workers de tracing lean_dojo : NUM_PROCS vaut cpu_count() par defaut
# (20 sur cette machine), ce qui sature la RAM de la VM WSL (8 Go) -> OOM kill
# pendant le tracing. Doit etre fixe AVANT le premier import de lean_dojo.
os.environ.setdefault("NUM_PROCS", "4")

# Ray (utilise par lean_dojo) : desactive le token d'auth local. Au premier
# demarrage, Ray genere un token et loggue le chemin absolu ~/.ray/auth_token
# (fuite du chemin machine dans les sorties) ; RAY_AUTH_MODE=disabled evite
# la generation ET la ligne, sans effet sur un cluster local mono-noeud.
os.environ.setdefault("RAY_AUTH_MODE", "disabled")

# ----- DEPOT A UTILISER -----
# "micro"  : lean4-example, 2 théorèmes utilisateur (RECOMMANDE)
# "small"  : lean4-example, 10 premiers théorèmes
# "medium" : formal-conjectures, ~100 théorèmes (30-60 min 1ere fois)
# "large"  : mathlib4, >100k théorèmes (2-4h 1ere fois)
REPO_SIZE = "micro"

# ----- OPERATIONS A ACTIVER -----
# Mettre True pour activer, False pour skip (mode demo)

ENABLE_TRACING = True      # Tracer le depot et extraire les théorèmes
                           # Temps: 1-2 min (cache) / 5-15 min (1ere fois)

ENABLE_DOJO_DEMO = True    # Ouvrir un Dojo et exécuter des tactiques
                           # Temps: 1-2 min (cache) / 30+ min (peut re-tracer)

ENABLE_AUTO_PROOF = True   # Démontrer la preuve automatique avec LLM pattern
                           # Temps: Rapide si Dojo deja ouvert, sinon 30+ min

# ----- CONFIGURATION AVANCEE -----
TRACING_TIMEOUT_MINUTES = 15    # Timeout pour le tracing
DOJO_TIMEOUT_MINUTES = 45       # Timeout pour le Dojo
MAX_THEOREMS_DISPLAY = 10       # Nombre max de theoremes a afficher

# =============================================================================
# AFFICHAGE DE LA CONFIGURATION
# =============================================================================
print("=" * 70)
print("CONFIGURATION PRINCIPALE DU NOTEBOOK")
print("=" * 70)
print(f"""
  Depot        : {REPO_SIZE}
  
  Operations activees:
    - Tracing       : {'ON' if ENABLE_TRACING else 'OFF (mode demo)'}
    - Dojo demo     : {'ON' if ENABLE_DOJO_DEMO else 'OFF (mode demo)'}
    - Preuve auto   : {'ON' if ENABLE_AUTO_PROOF else 'OFF (mode demo)'}
  
  Timeouts:
    - Tracing       : {TRACING_TIMEOUT_MINUTES} min
    - Dojo          : {DOJO_TIMEOUT_MINUTES} min
""")

# Estimation du temps total
if ENABLE_TRACING and ENABLE_DOJO_DEMO:
    print("  Temps estime : 3-5 min (cache) / 30-60 min (1ere fois)")
elif ENABLE_TRACING:
    print("  Temps estime : 2-3 min (cache) / 5-15 min (1ere fois)")
else:
    print("  Temps estime : < 30 secondes (mode demo)")

print("\n" + "=" * 70)
print("[OK] Configuration prete - continuez l'execution du notebook")
print("=" * 70)

======================================================================
CONFIGURATION PRINCIPALE DU NOTEBOOK
======================================================================

  Depot        : micro

  Operations activees:
    - Tracing       : ON
    - Dojo demo     : ON
    - Preuve auto   : ON

  Timeouts:
    - Tracing       : 15 min
    - Dojo          : 45 min

  Temps estime : 3-5 min (cache) / 30-60 min (1ere fois)

======================================================================
[OK] Configuration prete - continuez l'execution du notebook
======================================================================

Interpretation de la Configuration

La configuration ci-dessus determine le comportement de tout le notebook. Voici ce qui se passe selon vos choix :

Configuration	Impact sur l’exécution	Temps
REPO_SIZE="micro"	Trace uniquement lean4-example (2 théorèmes utilisateur)	1-2 min
ENABLE_TRACING=True	Compile et extrait les metadonnees du depot	5-15 min (1ere fois)
ENABLE_DOJO_DEMO=False	Skip l’environnement interactif (peut re-tracer)	Economise 30+ min
ENABLE_AUTO_PROOF=True	Tente une preuve automatique (necessite Dojo)	Variable

Sortie observee : Le notebook est configure en mode micro avec tracing actif mais sans Dojo. Cela permet une exécution rapide (2-3 min estimees) tout en voyant l’extraction de théorèmes.

Note pratique : Si c’est votre première exécution, mettez tout a False sauf ENABLE_TRACING pour une decouverte progressive.

---

Utilitaire de Timing

La cellule suivante créé une instance de Timer pour mesurer les temps d’exécution de chaque opération. Cela nous permettra de voir quelles étapes sont couteuses.

# =============================================================================
# Utilitaire de timing pour mesurer les temps d'exécution
# =============================================================================
import time
from contextlib import contextmanager
from datetime import datetime

class Timer:
    """Classe pour mesurer et afficher les temps d'exécution."""
    
    def __init__(self):
        self.start_time = None
        self.cell_times = []
        self.notebook_start = time.time()
    
    def start(self, label=""):
        self.start_time = time.time()
        self.current_label = label
        return self
    
    def stop(self):
        if self.start_time:
            elapsed = time.time() - self.start_time
            self.cell_times.append((self.current_label, elapsed))
            return elapsed
        return 0
    
    def elapsed(self):
        if self.start_time:
            return time.time() - self.start_time
        return 0
    
    def format(self, seconds):
        if seconds < 1:
            return f"{seconds*1000:.0f}ms"
        elif seconds < 60:
            return f"{seconds:.1f}s"
        else:
            return f"{seconds/60:.1f}min"
    
    def summary(self):
        total = time.time() - self.notebook_start
        print("" + "=" * 60)
        print("RESUME DES TEMPS D'EXECUTION")
        print("=" * 60)
        for label, t in self.cell_times:
            print(f"  {label}: {self.format(t)}")
        print(f"  TOTAL: {self.format(total)}")
        print("=" * 60)

# Instance globale
timer = Timer()
print(f"[TIMER] Notebook demarre a {datetime.now().strftime('%H:%M:%S')}")

[TIMER] Notebook demarre a 08:46:11

Details sur les Depots

Cette section explique les choix de depot disponibles (configures via REPO_SIZE ci-dessus).

Pourquoi tant de fichiers même pour un petit depot ?

Tout projet Lean 4 inclut la bibliotheque standard (Init/, Std/, etc.) qui represente l’essentiel des fichiers traces. C’est inevitable - LeanDojo doit tracer toutes les dependances pour connaitre les premises utilisables.

Le paramètre user_files_only permet de filtrer les théorèmes pour ne garder que ceux du projet utilisateur (ex: Lean4Example.lean) et ignorer les théorèmes venant de la stdlib.

Qu’est-ce que le Dojo ?

Le Dojo est l’environnement interactif de LeanDojo pour exécuter des tactiques une par une. C’est l’interface ideale pour le Reinforcement Learning et les LLMs.

Note : Le Dojo peut necessiter un re-tracing du depot, ce qui prend du temps. Pour les gros depots, le Dojo est desactive par defaut.

# =============================================================================
# CONFIGURATION DES DEPOTS (utilise REPO_SIZE de la config principale)
# =============================================================================

# Configuration des depots disponibles
# NOTE: Tous les repos Lean 4 incluent ~1500 fichiers de la stdlib.
#       Le paramètre user_files_only filtre les théorèmes APRES le tracing.
#
# IMPORTANT - appariement version LeanDojo <-> toolchain Lean :
# Le commit 4164749e pin lean-toolchain v4.11.0. C'est voulu : l'interaction
# Dojo (REPL in-tactic via stdin) est structurellement cassee sur Lean >= 4.19
# (stdin isole pendant l'elaboration + option --memory retiree), or lean-dojo
# 4.20.0 ne sait tracer QUE les toolchains recentes. La paire fonctionnelle
# est lean-dojo 2.2.0 + toolchain <= v4.11 (voir cellule d'installation).
REPOS = {
    "micro": {
        "url": "https://github.com/yangky11/lean4-example",
        "commit": "4164749e28cd331cb4196a16bf232182da1fa4fe",  # lean-toolchain v4.11.0
        "description": "lean4-example (théorèmes utilisateur seulement)",
        "user_files_only": True,  # Ne garder que Lean4Example.lean
        "user_file_patterns": ["Lean4Example.lean"],  # Fichiers utilisateur
        "theorems_filter": None,  # Pas de limite (2 théorèmes seulement)
        "tracing_time": "< 2 min (depuis cache)",
    },
    "small": {
        "url": "https://github.com/yangky11/lean4-example",
        "commit": "4164749e28cd331cb4196a16bf232182da1fa4fe",  # lean-toolchain v4.11.0
        "description": "lean4-example (utilisateur + quelques stdlib)",
        "user_files_only": False,
        "user_file_patterns": [],
        "theorems_filter": 10,  # Limiter a 10 pour la demo
        "tracing_time": "< 2 min (depuis cache)",
    },
    "medium": {
        "url": "https://github.com/google-deepmind/formal-conjectures",
        "commit": "ce0a081ab74d625948c44da6022992e1f9db070a",
        "description": "formal-conjectures (DeepMind)",
        "user_files_only": False,
        "user_file_patterns": [],
        "theorems_filter": 100,  # Limiter a 100
        "tracing_time": "30-60 min",
    },
    "large": {
        "url": "https://github.com/leanprover-community/mathlib4",
        "commit": "v4.15.0",
        "description": "mathlib4",
        "user_files_only": False,
        "user_file_patterns": [],
        "theorems_filter": 100,  # Limiter a 100 pour la demo
        "tracing_time": "2-4 heures",
    },
}

# Obtenir la configuration selectionnee (REPO_SIZE vient de la config principale)
SELECTED_REPO = REPOS[REPO_SIZE]
USER_FILES_ONLY = SELECTED_REPO.get("user_files_only", False)
USER_FILE_PATTERNS = SELECTED_REPO.get("user_file_patterns", [])

print("=" * 60)
print("DEPOT SELECTIONNE")
print("=" * 60)
print(f"Option: {REPO_SIZE}")
print(f"Depot: {SELECTED_REPO['description']}")
print(f"URL: {SELECTED_REPO['url']}")
print(f"Temps de tracing estime: {SELECTED_REPO['tracing_time']}")
print(f"Filtrer theoremes utilisateur: {USER_FILES_ONLY}")

if USER_FILE_PATTERNS:
    print(f"Fichiers utilisateur: {USER_FILE_PATTERNS}")
if SELECTED_REPO.get("theorems_filter"):
    print(f"Limite theoremes: {SELECTED_REPO['theorems_filter']}")

============================================================
DEPOT SELECTIONNE
============================================================
Option: micro
Depot: lean4-example (théorèmes utilisateur seulement)
URL: https://github.com/yangky11/lean4-example
Temps de tracing estime: < 2 min (depuis cache)
Filtrer theoremes utilisateur: True
Fichiers utilisateur: ['Lean4Example.lean']

Interpretation : Depot Selectionne

Résultat : Le notebook utilisera lean4-example avec filtrage des fichiers utilisateur uniquement.

Cela signifie : - Tracing rapide : Le depot est petit (stdlib incluse) - Extraction ciblee : Seuls les théorèmes de Lean4Example.lean seront analyses (2 théorèmes) - Pedagogique : Ideal pour comprendre le fonctionnement sans attendre

Pourquoi tant de fichiers pour un petit depot ?

Tout projet Lean 4 depend de la bibliotheque standard (Init/, Std/, Lean/) qui est automatiquement incluse. LeanDojo doit tracer toutes les dependances pour connaitre les premises (lemmes, définitions) disponibles lors de la preuve.

Le filtrage user_files_only=True n’affecte que l’extraction finale des théorèmes, pas le tracing initial.

1. Vérification de l’Environnement

Avant de commencer, verifions que notre environnement Python est compatible avec LeanDojo.

LeanDojo utilise des fonctionnalites spécifiques de Python qui ne sont pas encore disponibles dans Python 3.13+. Si vous utilisez une version trop recente, vous devrez utiliser un environnement conda ou venv avec Python 3.10-3.12.

# =============================================================================
# Vérification de la version Python
# LeanDojo necessite Python < 3.13 en raison de dependances specifiques
# =============================================================================
timer.start("Verification environnement")
import sys
import platform

print("=" * 60)
print("VERIFICATION DE L'ENVIRONNEMENT")
print("=" * 60)

print(f"\nPython version: {sys.version}")
print(f"Platform: {platform.system()} {platform.release()}")

# Vérification de compatibilite
if sys.version_info >= (3, 13):
    print("\n[WARNING] LeanDojo necessite Python < 3.13")
    print("Solution: conda activate mcp-jupyter-py310")
    print("Ou: Utilisez le kernel 'Python 3 (WSL)' si disponible")
elif sys.version_info < (3, 10):
    print("\n[WARNING] LeanDojo necessite Python >= 3.10")
else:
    print(f"\n[OK] Python {sys.version_info.major}.{sys.version_info.minor} compatible avec LeanDojo")

# Vérification de l'OS
if platform.system() == "Windows":
    print("\n[NOTE] Windows detecte - WSL recommande pour le tracing")
print(f"[TIMER] Verification environnement: {timer.format(timer.stop())}")

============================================================
VERIFICATION DE L'ENVIRONNEMENT
============================================================

Python version: 3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]
Platform: Linux 6.6.87.2-microsoft-standard-WSL2

[OK] Python 3.12 compatible avec LeanDojo
[TIMER] Verification environnement: 0ms

Interpretation : Environnement Vérifié

Résultat : Python 3.12 sous WSL Linux detecte.

Critere	Valeur	Statut
Version Python	3.12.3	Compatible (3.10-3.12)
Système	Linux (WSL)	Optimal pour tracing
Plateforme	WSL2	Evite les blocages Windows

Pourquoi WSL est recommande ?

LeanDojo utilise des subprocess intensifs pour compiler Lean et tracer les depots. Sur Windows natif, ces processus peuvent se bloquer indefiniment sans message d’erreur. WSL (Windows Subsystem for Linux) contourne ce problème en executant dans un environnement Linux véritable.

Note : Si vous voyez “Platform: Windows”, le tracing peut prendre plus de temps ou bloquer. Utilisez le kernel “Python 3 (WSL)” si disponible.

Installation de LeanDojo

Si LeanDojo n’est pas installe, decommentez et executez la cellule suivante.

Note importante : Sur Windows, il est fortement recommande d’installer LeanDojo dans WSL Ubuntu plutot que dans Windows natif, car le tracing peut se bloquer.

# =============================================================================
# Installation de LeanDojo (decommenter si necessaire)
# =============================================================================
# IMPORTANT - version : utilisez lean-dojo 2.2.0, PAS 4.20.0.
#   - lean-dojo 4.20.0 trace les toolchains Lean >= 4.19 mais son Dojo
#     interactif y est casse (Lean >= 4.19 isole stdin pendant l'elaboration
#     et a retire l'option --memory) -> DojoInitError / DojoCrashError.
#   - lean-dojo 2.2.0 trace les toolchains <= v4.11, ou le Dojo fonctionne.
#   - Le requires-python de 2.2.0 est declare "<=3.12" (PEP 440 : cette borne
#     exclut 3.12.1+ par erreur) -> --ignore-requires-python est necessaire
#     avec Python 3.12.x ; le code est compatible 3.12.
# !pip install --ignore-requires-python lean-dojo==2.2.0

# Sur Windows, preferez installer dans WSL:
# wsl -d Ubuntu
# pip install --ignore-requires-python lean-dojo==2.2.0

print("Installation: Decommentez la ligne ci-dessus si necessaire")

Installation: Decommentez la ligne ci-dessus si necessaire

2. Configuration du Token GitHub

LeanDojo utilise l’API GitHub pour acceder aux depots. Sans token, vous etes limite a 60 requêtes par heure, ce qui est insuffisant pour tracer un depot.

Nous allons configurer le token depuis plusieurs sources possibles : 1. Variable d’environnement existante 2. Fichier .env local 3. CLI gh (GitHub CLI) si installe

import os
import sys
from pathlib import Path

# --- Detection robuste du repertoire du notebook ---
# Fonctionne sous Windows, Linux, macOS et WSL (Epic #2314, Issue #2315)
notebook_dir = None

# Strategie 1: Variable environnement LEAN_NOTEBOOK_DIR
if os.getenv("LEAN_NOTEBOOK_DIR"):
    candidate = Path(os.getenv("LEAN_NOTEBOOK_DIR"))
    if candidate.exists() and (candidate / "lean_runner.py").exists():
        notebook_dir = candidate

# Strategie 2: Chercher dans cwd et parents (cross-platform)
if not notebook_dir:
    cwd = Path.cwd().resolve()
    current = cwd
    for _ in range(10):
        candidate = current / "MyIA.AI.Notebooks" / "SymbolicAI" / "Lean"
        if candidate.exists() and (candidate / "lean_runner.py").exists():
            notebook_dir = candidate
            break
        current = current.parent
        if current == current.parent:
            break

# Strategie 3: Recherche dynamique (Epic #2314, Issue #2315)
if not notebook_dir:
    _drive = Path.cwd().resolve().drive
    for _dl in ([_drive[0]] if _drive else ["c", "d"]):
        for _root in [f"{_dl}:/dev/CoursIA", f"{_dl.upper()}/dev/CoursIA"]:
            _cand = Path(_root) / "MyIA.AI.Notebooks" / "SymbolicAI" / "Lean"
            if _cand.exists() and (_cand / "lean_runner.py").exists():
                notebook_dir = _cand
                break
        if notebook_dir:
            break

if notebook_dir:
    # Chemin relatif au repo (machine-independant, pas de chemin absolu dans les sorties)
    try:
        _display_dir = notebook_dir.relative_to(notebook_dir.parents[2])
    except (IndexError, ValueError):
        _display_dir = notebook_dir.name
    print(f"Notebook dir: {_display_dir}")
    sys.path.insert(0, str(notebook_dir))
else:
    print("[!] Repertoire du notebook non trouve.")

Notebook dir: MyIA.AI.Notebooks/SymbolicAI/Lean

Interpretation : Token GitHub Configure

Résultat : Token charge depuis le fichier .env local.

Token: ghp_••••••••••••••••••••
Source: <répertoire_Lean>/.env (GITHUB_TOKEN)

Pourquoi un token GitHub est necessaire ?

LeanDojo doit acceder a l’API GitHub pour : 1. Cloner les depots : lean4-example, mathlib4, etc. 2. Vérifier les commits : S’assurer que le commit existe 3. Télécharger les releases : Binaires Lean pre-compiles

Sans token, vous etes limite a 60 requêtes/heure, ce qui est insuffisant pour tracer un depot moyen (Mathlib4 peut necessiter 500+ requêtes).

Avec token : 5000 requêtes/heure.

Securite : Le token est masque dans l’affichage (ghp_••••••••••••••••••••). Assurez-vous que .env est dans .gitignore.

3. Import des Modules LeanDojo

Maintenant que l’environnement est configure, importons les modules principaux de LeanDojo.

Chaque module a un rôle spécifique : - LeanGitRepo : Reference a un depot Git (ne telecharge rien) - trace : Fonction qui analyse un depot - is_available_in_cache : Vérifie si un depot est déjà trace - Dojo : Environnement interactif de preuve - Theorem / TacticState : Types de données

# =============================================================================
# Import des modules LeanDojo
# =============================================================================
# On neutralise deux sources de fuite du chemin machine dans les sorties :
#   - tqdm emet un TqdmWarning 'IProgress not found' qui contient le chemin
#     absolu de site-packages ;
#   - le logger interne de lean_dojo (loguru) affiche le chemin absolu du
#     depot trace dans ~/.cache/lean_dojo lors du tracing.
import warnings as _warnings
_warnings.filterwarnings("ignore", message="IProgress not found")
# Ray (utilise par lean_dojo) emet une FutureWarning dont la localisation
# contient le chemin absolu du venv ; on la filtre aussi.
_warnings.filterwarnings("ignore", category=FutureWarning, module=r"ray\..*")
try:
    from loguru import logger as _ldj_logger
    _ldj_logger.disable("lean_dojo")
except Exception:
    pass

timer.start("Import LeanDojo")
try:
    import lean_dojo
    print(f"LeanDojo version: {lean_dojo.__version__}")

    from lean_dojo import (
        LeanGitRepo,           # Reference a un depot Lean
        trace,                 # Fonction de tracing
        is_available_in_cache, # Vérifie le cache
        Dojo,                  # Environnement interactif
        Theorem,               # Representation d'un théorème
        TacticState,           # État de preuve (buts restants)
        ProofFinished,         # Résultat: preuve terminee
        LeanError,             # Résultat: tactique invalide
    )

    print("\nModules importes:")
    print("  - LeanGitRepo: Reference a un depot Git")
    print("  - trace: Analyse un depot et extrait les metadonnees")
    print("  - is_available_in_cache: Verifie si deja en cache")
    print("  - Dojo: Environnement interactif de preuve")
    print("  - Theorem, TacticState: Types de donnees")
    print("  - ProofFinished, LeanError: Resultats possibles de run_tac")
    print("\n[OK] Tous les imports reussis")

    LEANDOJO_AVAILABLE = True

except ImportError as e:
    print(f"[ERROR] Import echoue: {e}")
    print("\nFallback: stubs minimaux charges (mode demo sans lean-dojo)")

    # Stubs pour le mode demo (lean-dojo non installe).
    # Imitent l'API minimale utilisee par les cellules suivantes.
    class Dojo:
        """Stub Dojo : environnement interactif minimal pour demo."""
        def __init__(self, theorem):
            self.theorem = theorem
        def __enter__(self):
            class _State:
                pp = "\nObjectif : voir LeanDojo trace + theorem"
            return self, _State()
        def __exit__(self, *args):
            return False
        def run_tac(self, state, tactic):
            return None

    class LeanError(Exception):
        """Stub : tactique invalide retournee par Dojo.run_tac."""
        pass

    class ProofFinished:
        """Stub : preuve terminee (run_tac a ferme tous les buts)."""
        pass

    class TacticState:
        """Stub : etat de preuve avec pretty-print."""
        def __init__(self, pp=""):
            self.pp = pp

    class Theorem:
        """Stub : representation d'un theoreme."""
        def __init__(self, repo=None, commit_hash=None, env=None, name=""):
            self.repo = repo
            self.commit_hash = commit_hash
            self.env = env
            self.name = name

    class LeanGitRepo:
        """Stub : reference a un depot Lean."""
        def __init__(self, url, commit_hash):
            self.url = url
            self.commit_hash = commit_hash

    def trace(*args, **kwargs):
        """Stub : tracing desactive en mode demo."""
        raise RuntimeError("lean_dojo non disponible : tracing desactive en mode demo")

    def is_available_in_cache(*args, **kwargs):
        """Stub : cache check desactive."""
        raise RuntimeError("lean_dojo non disponible : cache check desactive")

    LEANDOJO_AVAILABLE = False
print(f"[TIMER] Import LeanDojo: {timer.format(timer.stop())}")

LeanDojo version: 2.2.0

Modules importes:
  - LeanGitRepo: Reference a un depot Git
  - trace: Analyse un depot et extrait les metadonnees
  - is_available_in_cache: Verifie si deja en cache
  - Dojo: Environnement interactif de preuve
  - Theorem, TacticState: Types de donnees
  - ProofFinished, LeanError: Resultats possibles de run_tac

[OK] Tous les imports reussis
[TIMER] Import LeanDojo: 1.4s

Interpretation : Modules LeanDojo Importes

Résultat : L’import depend de la disponibilite de lean_dojo dans l’environnement Python. Les valeurs reelles (succes/echec, version, duree) sont imprimees dynamiquement par la cellule d’import ci-dessus ([OK] Tous les imports reussis / [ERROR] Import echoue, LeanDojo version: X.Y.Z, [TIMER] Import LeanDojo: Ns).

Module	Rôle	Usage
LeanGitRepo	Reference a un depot Git	Ne telecharge rien, juste un pointeur
trace()	Fonction de tracing	Compile le depot et extrait les metadonnees
is_available_in_cache()	Vérification cache	Evite de re-tracer si déjà fait
Dojo	Environnement interactif	REPL pour exécuter des tactiques
Theorem	Type de donnée	Represente un théorème (nom, fichier, code)
TacticState	État de preuve	Contient les buts restants apres une tactique

Notes sur les warnings (visibles uniquement en mode lean_dojo installe) :

• IProgress not found : Concerne les barres de progression Jupyter (widgets). N’affecte pas le fonctionnement.
• Missing packages: ['ipywidgets'] : Meme raison. Vous pouvez installer avec pip install ipywidgets si vous voulez de jolies barres de progression.

Le temps d’import est mesure par la cellule ci-dessus ([TIMER] Import LeanDojo: Ns). En mode lean_dojo present : Ray est initialise pour le tracing parallelise. En mode demo (lean_dojo absent) : aucun import reel, les stubs minimaux sont charges a la place.

4. Creation d’une Reference de Depot

LeanGitRepo represente une reference a un depot Git Lean. Il ne telecharge rien - c’est simplement un pointeur vers un commit spécifique.

Pourquoi un commit spécifique ?

LeanDojo necessite un commit précis (pas une branche) car : 1. Reproductibilite : Le même commit donne toujours les mêmes résultats 2. Cache : Le cache est indexe par commit 3. Compatibilite : Le fichier lean-toolchain determine la version de Lean

Le depot lean4-example

Nous utilisons le depot officiel lean4-example comme exemple. C’est un petit depot (~10 théorèmes) ideal pour tester LeanDojo sans attendre longtemps.

# =============================================================================
# Creation d'une reference de depot
# lean4-example est le depot de test officiel de LeanDojo
# =============================================================================
timer.start("Creation repo reference")

# Utiliser la configuration selectionnee
EXAMPLE_REPO = {
    "url": SELECTED_REPO["url"],
    "commit": SELECTED_REPO["commit"],
    "description": SELECTED_REPO["description"],
}

print("=" * 60)
print("DEPOT DE REFERENCE")
print("=" * 60)

if LEANDOJO_AVAILABLE:
    # Creation de la reference (ne telecharge rien)
    repo = LeanGitRepo(EXAMPLE_REPO["url"], EXAMPLE_REPO["commit"])

    print(f"\nURL: {repo.url}")
    print(f"Commit: {repo.commit[:12]}...")
    print(f"Description: {EXAMPLE_REPO['description']}")

    # Vérifications
    print(f"\nVerifications:")
    print(f"  Existe sur GitHub: {repo.exists()}")
    print(f"  En cache local: {is_available_in_cache(repo)}")
else:
    print("[SKIP] LeanDojo non disponible")
    repo = None
print(f"[TIMER] Creation repo reference: {timer.format(timer.stop())}")

============================================================
DEPOT DE REFERENCE
============================================================

URL: https://github.com/yangky11/lean4-example
Commit: 4164749e28cd...
Description: lean4-example (théorèmes utilisateur seulement)

Verifications:
  Existe sur GitHub: True
  En cache local: True
[TIMER] Creation repo reference: 1.4s

Interpretation : Reference de Depot Créée

Résultat : La cellule de reference au depot utilise SELECTED_REPO (defini par REPO_SIZE = "micro" | "small" | "medium" | "large") pour creer un LeanGitRepo. Les valeurs reelles (URL, commit, Existe sur GitHub, En cache local) sont imprimees dynamiquement par la cellule ci-dessus.

Points cles :

1. Aucun téléchargement a la creation : LeanGitRepo est juste un pointeur. Le depot n’est clone que lors du tracing.
2. Cache detecte en mode lean_dojo : si is_available_in_cache(repo) = True, le depot a deja ete trace precedemment et le tracing sera rapide (1-2 min au lieu de 5-15 min).
3. Mode demo : la cellule imprime [SKIP] LeanDojo non disponible et repo = None (les cellules suivantes basculent en mode demo).
4. Commit hash fixe : LeanDojo exige un commit specifique (pas une branche) car le cache est indexe par commit et la reproductibilite exige un point fixe. Le fichier lean-toolchain du commit determine la version de Lean (ici v4.11.0 : requis pour l’interaction Dojo, cassee sur Lean >= 4.19).

Prochaine étape : Voir la cellule de tracing ci-dessus pour la sortie reelle (cache hit, cache miss, ou SKIP demo).

5. Le Tracing : Coeur de LeanDojo

Le tracing est l’opération centrale de LeanDojo. C’est un processus qui :

1. Clone le depot Git
2. Telecharge les dependances (Mathlib4, Lake, etc.)
3. Compile le projet avec instrumentation
4. Extrait les metadonnees (théorèmes, tactiques, etats)

Temps de tracing estimes

Depot	Premier tracing	Depuis cache
lean4-example	5-15 min	< 1 sec
formal-conjectures	30-60 min	< 5 sec
Mathlib4	2-4 heures	< 30 sec

Problemes connus sur Windows

LeanDojo utilise des subprocess qui peuvent se bloquer sur Windows. Solutions :

1. Kernel WSL : Utilisez le kernel “Python 3 (WSL)” dans Jupyter
2. Mode SKIP : Desactivez le tracing pour la demo
3. Terminal : Lancez le tracing dans un terminal separe pour voir les logs

La cellule suivante permet de configurer le comportement.

# =============================================================================
# CONFIGURATION DU TRACING (utilise ENABLE_TRACING de la config principale)
# =============================================================================
import time
from pathlib import Path

# Derivation depuis la config principale
# ENABLE_TRACING=True  -> SKIP_TRACING=False -> tracing réel
# ENABLE_TRACING=False -> SKIP_TRACING=True  -> mode demo
SKIP_TRACING = not ENABLE_TRACING

print("=" * 60)
print("CONFIGURATION TRACING")
print("=" * 60)
print(f"\nENABLE_TRACING: {ENABLE_TRACING}")
print(f"SKIP_TRACING: {SKIP_TRACING}")
print(f"TRACING_TIMEOUT: {TRACING_TIMEOUT_MINUTES} minutes")

if SKIP_TRACING:
    print("\n[MODE DEMO] Le tracing est desactive.")
    print("Les cellules d'extraction de theoremes afficheront des exemples.")
    print("\nPour activer: mettez ENABLE_TRACING = True dans la config principale.")
else:
    print("\n[TRACING ACTIF] Le depot sera trace.")
    print("Si deja en cache: chargement rapide (1-2 min)")
    print("Sinon: tracing complet (5-15 min pour lean4-example)")

============================================================
CONFIGURATION TRACING
============================================================

ENABLE_TRACING: True
SKIP_TRACING: False
TRACING_TIMEOUT: 15 minutes

[TRACING ACTIF] Le depot sera trace.
Si deja en cache: chargement rapide (1-2 min)
Sinon: tracing complet (5-15 min pour lean4-example)

Vérification du Cache

Avant de lancer un tracing, verifions l’état du cache LeanDojo. Le cache se trouve dans ~/.cache/lean_dojo/ et contient les depots déjà traces.

Si le depot est en cache, le chargement est quasi-instantane.

# =============================================================================
# Vérification du cache LeanDojo
# =============================================================================
timer.start("Verification cache")
print("=" * 60)
print("VERIFICATION DU CACHE")
print("=" * 60)

cache_dir = Path.home() / ".cache" / "lean_dojo"
print(f"\nRepertoire cache: ~/{cache_dir.relative_to(Path.home())}")
print(f"Existe: {cache_dir.exists()}")

if cache_dir.exists():
    try:
        cache_contents = list(cache_dir.iterdir())
        print(f"Contenu: {len(cache_contents)} elements")

        if cache_contents:
            print("\nElements en cache:")
            for item in cache_contents[:5]:
                if item.is_dir():
                    size = sum(f.stat().st_size for f in item.rglob('*') if f.is_file()) / 1024 / 1024
                    print(f"  - {item.name} ({size:.1f} MB)")
                else:
                    print(f"  - {item.name}")
            if len(cache_contents) > 5:
                print(f"  ... et {len(cache_contents) - 5} autres")
    except PermissionError:
        print("  (acces refuse)")
else:
    print("  Cache vide - le premier tracing sera plus long")

# Vérifier si notre repo est en cache
if LEANDOJO_AVAILABLE and repo:
    in_cache = is_available_in_cache(repo)
    print(f"\nlean4-example en cache: {in_cache}")
print(f"[TIMER] Verification cache: {timer.format(timer.stop())}")

============================================================
VERIFICATION DU CACHE
============================================================

Repertoire cache: ~/.cache/lean_dojo
Existe: True
Contenu: 3 elements

Elements en cache:
  - yangky11-lean4-example-4164749e28cd331cb4196a16bf232182da1fa4fe (1169.5 MB)
  - durant42040-lean4-example-3e23ab0bfdcfdbd5b11ab53c2cd8b5d16492e9c2 (2880.0 MB)
  - repos (4049.3 MB)

lean4-example en cache: True
[TIMER] Verification cache: 767ms

Interpretation : État du Cache

Résultat : La cellule de verification du cache inspecte ~/.cache/lean_dojo. Les valeurs reelles (existence du repertoire, nombre d’elements, taille en MB) sont imprimees dynamiquement par la cellule ci-dessus (Existe: True/False, Contenu: N elements, ligne par element avec taille).

Cas de figure (sortie reelle = voir cellule ci-dessus) :

État du cache	Sortie typique	Effet
Cache vide	Existe: False	Premier tracing plus long
Cache peuple	Existe: True + N elements	Tracings subsequents rapides

En mode demo (lean_dojo absent) : la verification du cache n’a pas de sens (aucun tracing n’aura lieu). La cellule imprime Existe: False meme si un cache reel existe sur le disque.

Conseil : Le cache peut grossir rapidement si vous tracez plusieurs depots. Utilisez rm -rf ~/.cache/lean_dojo/ pour nettoyer.

Exécution du Tracing

La cellule suivante exécute le tracing si SKIP_TRACING = False.

Attention : Sur Windows natif, le tracing peut se bloquer. Si ca prend plus de 15 minutes, interrompez le kernel et passez en mode SKIP ou utilisez WSL.

# =============================================================================
# Exécution du tracing
# =============================================================================
timer.start("Tracing")
print("=" * 60)
print("TRACING")
print("=" * 60)

traced_repo = None
theorems = []

# build_deps=False : on ne trace que les fichiers du depot lui-meme (pas ses
# dependances) -> evite un re-build massif et l'OOM sur la VM WSL 8 Go.
TRACE_BUILD_DEPS = False

if not LEANDOJO_AVAILABLE or repo is None:
    print("\n[SKIP] LeanDojo non disponible")

elif SKIP_TRACING:
    print("\n[MODE DEMO] Tracing desactive (SKIP_TRACING=True)")
    print("\nPour activer le tracing reel:")
    print("  1. Mettez SKIP_TRACING = False dans la cellule de configuration")
    print("  2. Sur Windows, utilisez le kernel 'Python 3 (WSL)'")
    print("  3. Relancez les cellules depuis le debut")

elif is_available_in_cache(repo):
    print("\n[CACHE HIT] Depot deja en cache!")
    print("Chargement depuis le cache...")

    start = time.time()
    try:
        traced_repo = trace(repo, build_deps=TRACE_BUILD_DEPS)
        elapsed = time.time() - start
        print(f"\nCharge en {elapsed:.1f}s")
        print(f"Path: ~/{Path(str(traced_repo.root_dir)).relative_to(Path.home())}")
    except Exception as _e:
        print(f"\n[ECHEC] Le tracing depuis le cache a echoue: {type(_e).__name__}: {str(_e)[:200]}")
        print("Bascule en mode demo pour les cellules suivantes.")
        traced_repo = None

else:
    print(f"\n[TRACING] Premier tracing de {repo.url}")
    print(f"Ceci peut prendre 5-15 minutes...")
    print(f"\nSi le tracing se bloque (>15 min), interrompez et:")
    print(f"  - Mettez SKIP_TRACING = True")
    print(f"  - Ou utilisez WSL")

    start = time.time()
    try:
        traced_repo = trace(repo, build_deps=TRACE_BUILD_DEPS)
        elapsed = time.time() - start
        print(f"\nTracing termine en {elapsed/60:.1f} minutes")
        print(f"Path: ~/{Path(str(traced_repo.root_dir)).relative_to(Path.home())}")
    except Exception as _e:
        print(f"\n[ECHEC] Le tracing reel a echoue: {type(_e).__name__}: {str(_e)[:200]}")
        print("Causes possibles: lake build absent, ExtractData.lean incompatible, OOM, timeout reseau.")
        print("Bascule en mode demo pour les cellules suivantes.")
        traced_repo = None

# Resume
print("\n" + "=" * 60)
if traced_repo:
    print("[OK] traced_repo disponible - les cellules suivantes fonctionneront")
else:
    print("[INFO] traced_repo = None - les cellules suivantes seront en mode demo")
print(f"[TIMER] Tracing: {timer.format(timer.stop())}")

============================================================
TRACING
============================================================

[CACHE HIT] Depot deja en cache!
Chargement depuis le cache...

Charge en 13.0s
Path: ~/.cache/lean_dojo/yangky11-lean4-example-4164749e28cd331cb4196a16bf232182da1fa4fe/lean4-example

============================================================
[OK] traced_repo disponible - les cellules suivantes fonctionneront
[TIMER] Tracing: 13.0s

Interpretation : Tracing Complète

Résultat : Depot charge depuis le cache. Le temps de chargement et le debit d’analyse dependent de la machine (CPU, RAM, charge, taille du cache Ray) ; ils sont imprimes dynamiquement par la cellule de tracing ci-dessus (variable elapsed et barre de progression Ray).

[CACHE HIT] Depot deja en cache
Trace en <elapsed_in_machine>s   <-- imprime par la cellule de tracing
Path: ~/.cache/lean_dojo/yangky11-lean4-example-.../lean4-example
traced_repo disponible

Analyse du processus :

1. Detection du cache : is_available_in_cache(repo) = True -> chargement direct
2. Parallelisation Ray : 100%|██████████| N/N [00:54<00:00, X.XXit/s]
   • N fichiers analyses (stdlib Lean + depot utilisateur)
   • X.XX fichiers/seconde (parallelise sur plusieurs cores)
3. Temps total : lu dans la sortie de la cellule ci-dessus ({elapsed:.1f}s)

Pourquoi N fichiers ?

Le depot lean4-example ne contient que les fichiers utilisateur (Lean4Example.lean + lakefile.lean), mais depend de toute la bibliotheque standard Lean 4 :

Composant	Description
Init/	Initialisation Lean
Std/	Bibliotheque standard
Lean/	Compilateur Lean
Utilisateur	Lean4Example.lean

LeanDojo doit tracer toutes les dependances pour connaitre les premises (lemmes, définitions) disponibles lors de la preuve.

Performance : le tracing d’un depot de reference depose dans le cache prend en général quelques dizaines de secondes sur une machine de developpement recente, mais le temps réel depend de la machine. Sans cache, le premier tracing peut prendre plusieurs minutes (compilation incluse) – voir la cellule de tracing pour la valeur mesuree.

6. Extraction des Théorèmes

Une fois le depot trace, nous pouvons extraire tous les théorèmes. Chaque théorème contient :

• full_name : Nom complet (ex: Nat.add_comm)
• file_path : Chemin du fichier source
• code : Code source Lean

Filtrage des théorèmes

Le depot lean4-example trace la stdlib complete : la plupart des théorèmes extraits viennent de la bibliotheque standard Lean (Init/, Std/, etc.).

Avec l’option user_files_only=True, nous filtrons pour ne garder que les théorèmes du fichier utilisateur (Lean4Example.lean), soit 2 théorèmes : hello_world et foo.

Mode	Théorèmes	Description
micro	2	Uniquement Lean4Example.lean
small	10	Premiers théorèmes (mix user + stdlib)
medium/large	100+	Selon depot

# =============================================================================
# Extraction des théorèmes depuis le depot trace
# =============================================================================
timer.start("Extraction theoremes")
print("=" * 60)
print("EXTRACTION DES THEOREMES")
print("=" * 60)

def is_user_file(file_path, patterns):
    """Vérifie si le fichier correspond aux patterns utilisateur."""
    file_str = str(file_path)
    for pattern in patterns:
        if pattern in file_str:
            return True
    return False

def is_stdlib_file(file_path):
    """Vérifie si le fichier fait partie de la stdlib Lean."""
    file_str = str(file_path)
    stdlib_patterns = [
        "src/lean/",      # Lean core
        "Init/",          # Init module
        "Std/",           # Std library
        "Lake/",          # Lake build system
        "Lean/",          # Lean module
        ".lake/",         # Lake cache
    ]
    for pattern in stdlib_patterns:
        if pattern in file_str:
            return True
    return False

if traced_repo is None:
    print("\n[MODE DEMO] Tracing non effectue")
    print("Les theoremes ne sont pas disponibles.")
    print("\nExemple de ce que vous verriez avec un tracing reel:")
    print("  Found 2 user theorems (filtered from 27360)")
    print("  [1] hello_world (Lean4Example.lean)")
    print("  [2] foo (Lean4Example.lean)")

    theorems = []
else:
    # Extraction de TOUS les théorèmes
    all_theorems = list(traced_repo.get_traced_theorems())
    total_count = len(all_theorems)
    
    # Appliquer le filtre utilisateur si demande
    if USER_FILES_ONLY and USER_FILE_PATTERNS:
        print(f"[FILTER] Filtrage par fichiers utilisateur: {USER_FILE_PATTERNS}")
        theorems = [
            thm for thm in all_theorems
            if is_user_file(
                thm.theorem.file_path if hasattr(thm, 'theorem') else getattr(thm, 'file_path', ''),
                USER_FILE_PATTERNS
            )
        ]
        print(f"[OK] {len(theorems)} theoremes utilisateur (sur {total_count} total)")
    elif SELECTED_REPO.get("theorems_filter"):
        # Limiter aux N premiers
        limit = SELECTED_REPO["theorems_filter"]
        theorems = all_theorems[:limit]
        print(f"[OK] {len(theorems)} theoremes (limite a {limit} sur {total_count})")
    else:
        theorems = all_theorems
        print(f"[OK] {len(theorems)} theoremes")
    
    print(f"\n[INFO] Total dans le depot: {total_count} theoremes")
    print(f"[INFO] Dont ~{total_count - 2} de la stdlib Lean (Init/, Std/, etc.)")
    print(f"[INFO] Theoremes selectionnes: {len(theorems)}")

    # Inspecter les attributs du premier théorème
    if theorems:
        sample = theorems[0]
        print(f"\nType: {type(sample).__name__}")
        attrs = [a for a in dir(sample) if not a.startswith('_')]
        print(f"Attributs disponibles: {attrs[:10]}...")

    # Affichage (limiter a 10 pour eviter spam)
    print("\nListe des theoremes selectionnes:")
    for i, thm in enumerate(theorems[:10]):
        # TracedTheorem a un attribut 'theorem' qui contient le Theorem
        if hasattr(thm, 'theorem'):
            name = thm.theorem.full_name if hasattr(thm.theorem, 'full_name') else str(thm.theorem)
            file_path = thm.theorem.file_path if hasattr(thm.theorem, 'file_path') else 'N/A'
        else:
            name = getattr(thm, 'full_name', getattr(thm, 'name', str(thm)))
            file_path = getattr(thm, 'file_path', 'N/A')
        print(f"  [{i+1}] {name}")
        print(f"      Fichier: {file_path}")

    if len(theorems) > 10:
        print(f"  ... et {len(theorems) - 10} autres")
print(f"[TIMER] Extraction theoremes: {timer.format(timer.stop())}")

============================================================
EXTRACTION DES THEOREMES
============================================================
[FILTER] Filtrage par fichiers utilisateur: ['Lean4Example.lean']
[OK] 2 theoremes utilisateur (sur 2 total)

[INFO] Total dans le depot: 2 theoremes
[INFO] Dont ~0 de la stdlib Lean (Init/, Std/, etc.)
[INFO] Theoremes selectionnes: 2

Type: TracedTheorem
Attributs disponibles: ['ast', 'comments', 'end', 'file_path', 'get_num_tactics', 'get_premise_full_names', 'get_proof_node', 'get_tactic_proof', 'get_theorem_statement', 'get_traced_tactics']...

Liste des theoremes selectionnes:
  [1] hello_world
      Fichier: Lean4Example.lean
  [2] foo
      Fichier: Lean4Example.lean
[TIMER] Extraction theoremes: 1ms

Interpretation : Théorèmes Extraits

Résultat : L’extraction des theoremes depend de l’etat du tracing. La sortie reelle est imprimee dynamiquement par la cellule ci-dessus.

Trois cas de figure (sortie reelle = voir cellule ci-dessus) :

Mode	Sortie typique	Theorie accessible
lean_dojo + tracing reussi	Found N user theorems (filtered from M total)	Theorems extraits du depot
lean_dojo + cache hit	meme format, plus rapide	Theorems depuis le cache
Demo (lean_dojo absent)	[MODE DEMO] Tracing non effectue / Les theoremes ne sont pas disponibles. + bloc “Exemple de ce que vous verriez”	Aucune, seulement un apercu

Pourquoi plusieurs milliers de theorems en mode lean_dojo ?

La bibliotheque standard Lean 4 contient des milliers de lemmes et theoremes fondamentaux : - Arithmetique : Nat.add_comm, Nat.mul_assoc, etc. - Listes : List.append_nil, List.reverse_reverse, etc. - Logique : And.intro, Or.elim, Exists.intro, etc.

Le filtrage user_files_only=True permet de se concentrer uniquement sur les theoremes que nous avons definis dans Lean4Example.lean (en mode micro : 2 theoremes hello_world et foo – valeurs reelles dans la sortie dynamique de la cellule ci-dessus).

Structure d’un TracedTheorem (en mode lean_dojo) :

L’objet retourne est un TracedTheorem qui contient : - theorem : L’objet Theorem interne (nom, fichier, code) - get_traced_tactics() : Liste des tactiques utilisees dans la preuve - get_premise_full_names() : Lemmes utilises comme premises - ast : Arbre syntaxique abstrait (AST)

Temps d’extraction : affiche dans [TIMER] Extraction theoremes: Ns de la cellule ci-dessus (mode lean_dojo uniquement).

Details d’un Théorème

Examinons de plus pres un théorème. L’objet Theorem contient toutes les informations necessaires pour travailler avec ce théorème dans un Dojo.

# =============================================================================
# Exploration d'un théorème en detail
# =============================================================================
timer.start("Details theoreme")
print("=" * 60)
print("DETAILS D'UN THEOREME")
print("=" * 60)

if not theorems:
    print("\n[MODE DEMO] Pas de theoremes disponibles")
    print("\nExemple de structure d'un theoreme:")
    print('''
    Theorem: Nat.add_comm
    File: Mathlib/Nat/Basic.lean
    Module: Nat.Basic

    Code:
    theorem add_comm (n m : Nat) : n + m = m + n := by
      induction n with
      | zero => simp
      | succ n ih => simp [Nat.succ_add, ih]
    ''')
else:
    traced_thm = theorems[0]
    
    # TracedTheorem wraps Theorem - get the inner theorem
    thm = traced_thm.theorem if hasattr(traced_thm, 'theorem') else traced_thm
    name = thm.full_name if hasattr(thm, 'full_name') else str(thm)
    file_path = thm.file_path if hasattr(thm, 'file_path') else 'N/A'

    print(f"\nTheoreme: {name}")
    print(f"Fichier: {file_path}")
    if hasattr(file_path, 'stem'):
        print(f"Module: {file_path.stem}")

    # Attributs disponibles sur TracedTheorem
    print(f"\nAttributs TracedTheorem: {[a for a in dir(traced_thm) if not a.startswith('_')][:8]}")

    # Code source (si disponible)
    if hasattr(thm, 'code') and thm.code:
        print(f"\nCode source:")
        print("-" * 40)
        print(thm.code[:500])
        print("-" * 40)
print(f"[TIMER] Details theoreme: {timer.format(timer.stop())}")

============================================================
DETAILS D'UN THEOREME
============================================================

Theoreme: hello_world
Fichier: Lean4Example.lean
Module: Lean4Example

Attributs TracedTheorem: ['ast', 'comments', 'end', 'file_path', 'get_num_tactics', 'get_premise_full_names', 'get_proof_node', 'get_tactic_proof']
[TIMER] Details theoreme: 0ms

Interpretation : Inspection du Théorème

Résultat : L’inspection d’un theoreme depend de l’etat du tracing. La sortie reelle (nom, fichier, attributs TracedTheorem) est imprimee dynamiquement par la cellule ci-dessus.

Trois cas de figure (sortie reelle = voir cellule ci-dessus) :

Mode	Sortie typique
lean_dojo + theorems extraits	Theoreme: hello_world / Fichier: Lean4Example.lean + attributs TracedTheorem reels
lean_dojo + cache	meme format
Demo	[MODE DEMO] Pas de theoremes disponibles + bloc “Exemple de structure d’un theoreme” avec Nat.add_comm

En mode lean_dojo : les attributs TracedTheorem disponibles sont :

['ast', 'comments', 'end', 'file_path', 'get_num_tactics',
 'get_premise_full_names', 'get_proof_node', 'get_tactic_proof']

Methodes utiles (mode lean_dojo) :

Méthode	Description	Exemple d’usage
get_num_tactics()	Nombre de tactiques dans la preuve	RL : complexite de la preuve
get_premise_full_names()	Lemmes utilises	Dataset : quelles premises sont necessaires
get_tactic_proof()	Preuve au format liste de tactiques	Apprentissage supervise
get_proof_node()	Arbre de preuve (AST)	Analyse structurelle

Pour voir le code source complet :

Il faut lire le fichier .lean directement :

file_path = traced_thm.file_path  # 'Lean4Example.lean'
# Ouvrir et lire le fichier dans traced_repo.root_dir

Ou utiliser get_theorem_statement() pour obtenir juste la signature.

Exercice 1 : Exploration des théorèmes extraits

Difficulte : Debutant | Duree estimée : 10 minutes

Vous avez vu comment LeanDojo extrait les théorèmes d’un depot Lean. Explorez maintenant ces théorèmes pour identifier les meilleurs candidats pour le theorem proving automatique.

Competences visees : - Naviguer dans les données extraites par LeanDojo - Analyser la complexite des théorèmes via le nombre de premises - Identifier les candidats pour l’automatisation

# === EXERCICE 1 : Exploration des théorèmes extraits ===
#
# Objectif : Explorer les théorèmes extraits par LeanDojo et identifier
# des candidats interessants pour le theorem proving automatique.
#
# Instructions :
# 1. A partir de traced_repo (si disponible) ou des données de demo,
#    lister les 10 premiers théorèmes extraits avec leur nom complet
#    et le nombre de premises (dependances) de chacun.
#
# 2. Filtrer les théorèmes qui ont MOINS de 5 premises
#    (ce sont les candidats les plus simples pour l'automatisation).
#
# 3. Pour le théorème le plus simple (moins de premises),
#    afficher son enonce complet et ses premises.
#
# 4. (Bonus) Calculer la distribution du nombre de premises :
#    combien de théorèmes ont 0-2 premises, 3-5, 6-10, 10+ ?
#
# Indices :
# - Si traced_repo est disponible : traced_repo.get_theorems() donne un iterateur
# - Chaque théorème a : .full_name, .file_path, .num_premises
# - Si traced_repo n'est pas disponible, travaillez avec les exemples
#   affiches dans les cellules precedentes (mode demo)

# Exercice: Votre code ici
pass  # Exercice: completez cet exercice

print("Exercice 1 a completer : exploration des theoremes extraits par LeanDojo")

Exercice 1 a completer : exploration des theoremes extraits par LeanDojo

7. Environnement Dojo : Preuves Interactives

Le Dojo est l’environnement interactif de LeanDojo. C’est l’interface ideale pour :

• Les LLMs qui generent des preuves tactique par tactique
• Le Reinforcement Learning ou chaque tactique est une action
• L’exploration manuelle de preuves

Fonctionnement du Dojo

with Dojo(theorem) as (dojo, initial_state):
    # initial_state contient le but initial

    # Exécuter une tactique
    result = dojo.run_tac(current_state, "intro")

    # isinstance(result, LeanError)     -> tactique invalide
    # isinstance(result, TacticState)   -> il reste des buts a prouver
    # isinstance(result, ProofFinished) -> preuve terminee

Etats de Preuve (TacticState)

Un TacticState contient : - goals : Liste des buts restants a prouver - pp : Pretty-print de l’état (format lisible)

run_tac retourne une union de types (jamais None) : TacticState (la tactique a avance), ProofFinished (plus de buts), LeanError (tactique invalide pour ce but).

Note (juin 2026) : appariement version LeanDojo <-> toolchain Lean

Le Dojo interactif de lean_dojo est structurellement casse sur les toolchains Lean >= 4.19 : 1. Le flag --memory=N passe a lean est rejete (unknown configuration option 'max_memory') — l’option a ete retiree de Lean. 2. Lean >= 4.19 isole stdin pendant l’elaboration : le REPL tactic (lean_dojo_repl dans Lean4Repl.lean) ne recoit plus les commandes envoyees par le pipe -> DojoInitError: Unexpected EOF.

Or lean-dojo 4.20.0 ne sait tracer que les toolchains recentes (>= 4.19) : aucun commit de lean4-example ne fonctionne de bout en bout avec 4.20.0 (les commits anciens ne se tracent pas, les recents ne s’interagissent pas).

Resolution appliquee dans ce notebook : pin lean-dojo==2.2.0 (installe avec --ignore-requires-python, cf. cellule d’installation) + commit 4164749e de lean4-example (lean-toolchain v4.11.0). Avec cette paire, le tracing ET l’interaction Dojo fonctionnent. L’API 2.2.0 de run_tac retourne une union de types (TacticState / ProofFinished / LeanError), geree par isinstance dans les cellules suivantes.

Issue de suivi : #2789

# =============================================================================
# Ouverture d'un Dojo pour un théorème
# Utilise ENABLE_DOJO_DEMO de la config principale
# =============================================================================
timer.start("Dojo ouverture")
print("=" * 60)
print("ENVIRONNEMENT DOJO")
print("=" * 60)

# Derivation depuis la config principale
SKIP_DOJO = not ENABLE_DOJO_DEMO

print(f"\nENABLE_DOJO_DEMO: {ENABLE_DOJO_DEMO}")
print(f"SKIP_DOJO: {SKIP_DOJO}")

if not theorems:
    print("\n[MODE DEMO] Pas de theoremes disponibles")
    print("Raison: Tracing desactive (ENABLE_TRACING=False)")
    print("\nExemple d'utilisation du Dojo:")
    print('''
    with Dojo(theorem) as (dojo, init_state):
        print(f"Goals: {len(init_state.goals)}")
        print(f"Goal 0: {init_state.goals[0]}")

        # État pretty-print
        print(init_state.pp)
        # Output: n m : Nat
        #         |- n + m = m + n
    ''')
elif SKIP_DOJO:
    print("\n[MODE DEMO] Dojo desactive (ENABLE_DOJO_DEMO=False)")
    print("Raison: Le Dojo peut re-tracer le repo (~30 minutes)")
    print("\nPour activer: mettez ENABLE_DOJO_DEMO = True dans la config principale.")
    
    traced_thm = theorems[0]
    thm = traced_thm.theorem if hasattr(traced_thm, 'theorem') else traced_thm
    name = thm.full_name if hasattr(thm, 'full_name') else str(thm)
    print(f"\nTheoreme qui serait utilise: {name}")
    
    print("\nExemple de sortie attendue:")
    print("  Etat initial:")
    print("    Nombre de buts: 1")
    print("    But 0: |- 1 + 1 = 2")
else:
    traced_thm = theorems[0]
    thm = traced_thm.theorem if hasattr(traced_thm, 'theorem') else traced_thm
    # Re-ancrage sur le depot GitHub (cle de cache)
    if getattr(thm.repo, 'url', None) != repo.url:
        thm = Theorem(repo, thm.file_path, thm.full_name)
    name = thm.full_name if hasattr(thm, 'full_name') else str(thm)
    print(f"\n[DOJO ACTIF] Ouverture pour: {name}")
    print("[INFO] Ceci peut prendre quelques minutes (possible re-tracing)")

    with Dojo(thm) as (dojo, init_state):
        print(f"\nEtat initial:")
        print(f"  Nombre de buts: {len(init_state.goals)}")

        if init_state.goals:
            print(f"  But 0: {init_state.goals[0]}")

        pp_state = getattr(init_state, 'pp', str(init_state))
        print(f"\n  Pretty-print:")
        for line in str(pp_state).split('\n'):
            print(f"    {line}")
        
        # Sauvegarder le dojo et l'état pour les cellules suivantes
        DOJO_INSTANCE = dojo
        DOJO_INITIAL_STATE = init_state
        
print(f"\n[TIMER] Dojo ouverture: {timer.format(timer.stop())}")

============================================================
ENVIRONNEMENT DOJO
============================================================

ENABLE_DOJO_DEMO: True
SKIP_DOJO: False

[DOJO ACTIF] Ouverture pour: hello_world
[INFO] Ceci peut prendre quelques minutes (possible re-tracing)

Etat initial:
  Nombre de buts: 1
  But 0: Goal(assumptions=[Declaration(ident='a', lean_type='Nat'), Declaration(ident='b', lean_type='Nat'), Declaration(ident='c', lean_type='Nat')], conclusion='a + b + c = a + c + b')

  Pretty-print:
    a b c : Nat
    ⊢ a + b + c = a + c + b

[TIMER] Dojo ouverture: 1.5s

Interpretation : Dojo Actif

Résultat : L’ouverture du Dojo depend de la disponibilite de theorems (donc du tracing). La sortie reelle est imprimee dynamiquement par la cellule ci-dessus.

Quatre cas de figure (sortie reelle = voir cellule ci-dessus) :

Mode	Sortie typique
lean_dojo + theorems + Dojo ON	[DOJO ACTIF] Ouverture pour: hello_world + etat initial + pretty-print
lean_dojo + theorems + Dojo OFF	[MODE DEMO] Dojo desactive (ENABLE_DOJO_DEMO=False) + theoreme qui serait utilise
lean_dojo absent	[MODE DEMO] Pas de theoremes disponibles + bloc “Exemple d’utilisation”
Theorems absents (autre cause)	idem ligne precedente

Points cles de la cellule d’ouverture (mode lean_dojo) :

1. Re-ancrage du théorème : les theoremes extraits du tracing referencent le depot par son chemin local dans le cache. On reconstruit un Theorem pointant vers l’URL GitHub d’origine pour obtenir un cache hit direct (sans cela, le Dojo re-tracerait tout le depot).
2. init_state est un TacticState : il expose goals (liste des buts) et pp (pretty-print lisible, identique a ce qu’afficherait VS Code).

Vérifier le résultat d’une tactique :

with Dojo(theorem) as (dojo, init_state):
    print(f"Buts initiaux: {len(init_state.goals)}")

    result = dojo.run_tac(init_state, "intro")

    if isinstance(result, LeanError):
        print("Tactique invalide")
    elif isinstance(result, ProofFinished):
        print("Preuve terminee!")
    else:  # TacticState
        print(f"Buts restants: {len(result.goals)}")

Cas d’usage du Dojo :

Application	Description
LLM Prompting	Envoyer l’etat au LLM, recevoir une tactique, executer
Reinforcement Learning	Agent apprend a choisir les tactiques (reward = preuve reussie)
Exploration manuelle	Tester des sequences de tactiques interactivement

Note : sur un gros depot non encore trace, l’ouverture du Dojo peut declencher un tracing complet (30+ min). Pour sauter cette section, mettez ENABLE_DOJO_DEMO = False dans la configuration principale.

Exécution de Tactiques

Dans un Dojo, nous pouvons exécuter des tactiques une par une et observer l’evolution de l’état de preuve.

Une tactique peut : - Reussir : Retourne un nouvel état - Echouer : Retourne None - Terminer la preuve : Retourne un état avec goals == []

# =============================================================================
# Exécution de tactiques dans un Dojo
# Utilise ENABLE_DOJO_DEMO de la config principale
# =============================================================================
timer.start("Execution tactiques")
print("=" * 60)
print("EXECUTION DE TACTIQUES")
print("=" * 60)

# SKIP_DOJO est deja defini dans la cellule precedente

if not theorems:
    print("\n[MODE DEMO] Pas de theoremes disponibles")
    print("Raison: Tracing desactive (ENABLE_TRACING=False)")
    print("\nExemple d'execution de tactiques:")
    print('''
    Theorem: Nat.add_comm
    Initial goals: 1

    'intro n' succeeded:
      Goals remaining: 1
      New goal: |- forall m, n + m = m + n
    ''')
elif SKIP_DOJO:
    print("\n[MODE DEMO] Execution tactiques desactivee (ENABLE_DOJO_DEMO=False)")
    print("\nExemple de sortie attendue:")
    print('''
    Theorem: hello_world
    Buts initiaux: 1

    'rfl' [OK]
      Buts restants: 0
    
    [OK] Preuve terminee!
    ''')
else:
    traced_thm = theorems[0]
    thm = traced_thm.theorem if hasattr(traced_thm, 'theorem') else traced_thm
    # Les théorèmes extraits referencent le depot par son chemin local dans le
    # cache (pas l'URL GitHub) : la cle de cache differe et le Dojo re-tracerait
    # tout le depot AVEC ses dependances (build_deps=True par defaut) -> OOM
    # sur une VM WSL a 8 Go. On re-ancre le théorème sur le depot d'origine
    # (cache hit direct) et on borne tout re-tracing eventuel a noDeps.
    if getattr(thm.repo, 'url', None) != repo.url:
        thm = Theorem(repo, thm.file_path, thm.full_name)

    name = thm.full_name if hasattr(thm, 'full_name') else str(thm)
    print(f"\nTheoreme: {name}")

    with Dojo(thm) as (dojo, init_state):
        print(f"Buts initiaux: {len(init_state.goals)}")

        tactics_to_try = ["intro", "intros", "rfl", "simp", "trivial", "omega"]
        current_state = init_state

        for tactic in tactics_to_try:
            if isinstance(current_state, ProofFinished):
                break

            result = dojo.run_tac(current_state, tactic)

            if isinstance(result, ProofFinished):
                print(f"\n'{tactic}' [OK]")
                print(f"  Buts restants: 0")
                print(f"\n[OK] Preuve terminee!")
                current_state = result
            elif isinstance(result, TacticState):
                print(f"\n'{tactic}' [OK]")
                print(f"  Buts restants: {len(result.goals)}")
                goal_str = str(result.goals[0])[:60]
                print(f"  Nouveau but: {goal_str}...")
                current_state = result
            else:
                # LeanError: la tactique ne s'applique pas a ce but
                print(f"'{tactic}' [FAIL] (tactique invalide)")
                
print(f"\n[TIMER] Execution tactiques: {timer.format(timer.stop())}")

============================================================
EXECUTION DE TACTIQUES
============================================================

Theoreme: hello_world
Buts initiaux: 1
'intro' [FAIL] (tactique invalide)

'intros' [OK]
  Buts restants: 1
  Nouveau but: Goal(assumptions=[Declaration(ident='a', lean_type='Nat'), D...
'rfl' [FAIL] (tactique invalide)
'simp' [FAIL] (tactique invalide)
'trivial' [FAIL] (tactique invalide)

'omega' [OK]
  Buts restants: 0

[OK] Preuve terminee!

[TIMER] Execution tactiques: 960ms

8. Interface Simplifiee : lean_runner.py

Le module lean_runner.py fourni dans ce repertoire offre une interface simplifiee pour LeanDojo.

Fonctionnalites

Méthode	Description
trace_repo(url, commit)	Trace un depot Git
get_theorems()	Retourne la liste des théorèmes
prove_with_tactics(thm, tactics)	Tente de prouver avec une sequence

Backend LeanDojo

Le runner peut utiliser LeanDojo comme backend pour les opérations avancees.

# Initialisation du LeanRunner (backend LeanDojo).
# RUNNER_AVAILABLE est consomme par les cellules suivantes pour skipper
# proprement les sections lean_runner si l'import echoue.
try:
    from lean_runner import LeanRunner

    runner = LeanRunner(backend="leandojo")
    RUNNER_AVAILABLE = True
    print(f"[OK] LeanRunner initialise")
    print(f"Backend: {runner.backend}")
except Exception as e:
    runner = None
    RUNNER_AVAILABLE = False
    print(f"[SKIP] LeanRunner indisponible: {e}")

[OK] LeanRunner initialise
Backend: Backend.LEANDOJO

Interpretation : LeanRunner Initialise

Résultat : L’initialisation de LeanRunner (backend "leandojo") depend de la disponibilite du module lean_runner ET de lean_dojo. La sortie reelle est imprimee dynamiquement par la cellule ci-dessus (succes ou message d’erreur avec la raison).

En mode lean_dojo present : la cellule affiche [OK] LeanRunner initialise suivi du backend selectionne (l’un des Backend.LEANDOJO / Backend.SUBPROCESS / Backend.REPL, selon la disponibilite).

En mode demo (lean_dojo absent ou erreur d’import) : la cellule affiche [SKIP] LeanRunner indisponible: LeanDojo not available. Install with: pip install lean-dojo. Requires Python < 3.13.

Qu’est-ce que LeanRunner ?

LeanRunner est une interface simplifiee developpee pour ce cours qui encapsule LeanDojo. Elle offre :

Méthode	Description	Avantage
trace_repo(url, commit)	Trace un depot	Gestion d’erreurs simplifiee
get_theorems()	Liste les theoremes	Filtrage automatique
prove_with_tactics(thm, tacs)	Tente une preuve	Retour JSON structure

Backends supportes (selection dynamique selon disponibilite) :

1. Backend leandojo : Interface complete avec Dojo (necessite pip install lean-dojo).
2. Backend subprocess : Appel direct a lean (plus simple mais moins de metadonnees).
3. Backend repl : Communication via stdin/stdout (experimental).

Pourquoi une interface simplifiee ?

LeanDojo est puissant mais complexe. LeanRunner cache : - La gestion des exceptions (timeouts, erreurs de compilation) - Les conversions de types (TracedTheorem -> dict) - La configuration du cache - Les logs verbeux

Note : Dans ce notebook, nous utilisons principalement LeanDojo directement pour montrer les concepts fondamentaux. LeanRunner est utile pour des scripts batch ou des pipelines ML.

Tracing via lean_runner

Le runner utilise le cache LeanDojo, donc si le depot est déjà trace, c’est instantane.

# =============================================================================
# Tracing via lean_runner
# NOTE: Section optionnelle - on a deja trace via LeanDojo directement
# =============================================================================
print("=" * 60)
print("TRACING VIA LEAN_RUNNER")
print("=" * 60)

# Le tracing a deja ete fait via LeanDojo directement (section 5)
# Cette section montre comment le faire via lean_runner

if not RUNNER_AVAILABLE:
    print("\n[SKIP] LeanRunner non disponible")
    print("Le tracing a deja ete effectue via LeanDojo directement.")
else:
    print("\n[INFO] LeanRunner disponible")
    print("Le tracing a deja ete effectue dans la section 5.")
    print(f"traced_repo disponible: {traced_repo is not None}")
    
    if traced_repo:
        print(f"Path: ~/{Path(str(traced_repo.root_dir)).relative_to(Path.home())}")
        print(f"Theoremes selectionnes: {len(theorems)}")
        if USER_FILES_ONLY:
            print(f"Mode: Fichiers utilisateur uniquement ({USER_FILE_PATTERNS})")

============================================================
TRACING VIA LEAN_RUNNER
============================================================

[INFO] LeanRunner disponible
Le tracing a deja ete effectue dans la section 5.
traced_repo disponible: True
Path: ~/.cache/lean_dojo/yangky11-lean4-example-4164749e28cd331cb4196a16bf232182da1fa4fe/lean4-example
Theoremes selectionnes: 2
Mode: Fichiers utilisateur uniquement (['Lean4Example.lean'])

Extraction et Preuve via lean_runner

Une fois le depot trace, nous pouvons extraire les théorèmes et tenter des preuves.

# =============================================================================
# Extraction des théorèmes via lean_runner
# NOTE: Section optionnelle - les théorèmes sont deja disponibles via traced_repo
# =============================================================================
timer.start("Extraction theoremes lean_runner")
print("=" * 60)
print("THEOREMES VIA LEAN_RUNNER")
print("=" * 60)

# Cette section est optionnelle car on a deja les théorèmes via traced_repo
# Le lean_runner offre une interface simplifiee mais n'est pas necessaire

if not RUNNER_AVAILABLE:
    print("\n[SKIP] LeanRunner non disponible")
    print("Ce n'est pas grave - les theoremes sont deja extraits via traced_repo")
    thms = []
else:
    print("\n[INFO] LeanRunner disponible mais non utilise ici")
    print("Les theoremes sont deja disponibles via la variable 'theorems'")
    print(f"Nombre de theoremes selectionnes: {len(theorems) if theorems else 0}")
    if USER_FILES_ONLY and theorems:
        print(f"Mode: Fichiers utilisateur uniquement")
    thms = []  # On utilise 'theorems' directement, pas besoin de thms

print(f"\n[TIMER] Extraction theoremes lean_runner: {timer.format(timer.stop())}")

============================================================
THEOREMES VIA LEAN_RUNNER
============================================================

[INFO] LeanRunner disponible mais non utilise ici
Les theoremes sont deja disponibles via la variable 'theorems'
Nombre de theoremes selectionnes: 2
Mode: Fichiers utilisateur uniquement

[TIMER] Extraction theoremes lean_runner: 0ms

Tentative de Preuve Automatique

La méthode prove_with_tactics essaie une sequence de tactiques et retourne le résultat.

# =============================================================================
# Preuve automatique avec une sequence de tactiques
# Utilise ENABLE_AUTO_PROOF de la config principale
# =============================================================================
timer.start("Preuve automatique")
print("=" * 60)
print("PREUVE AUTOMATIQUE")
print("=" * 60)

print(f"\nENABLE_AUTO_PROOF: {ENABLE_AUTO_PROOF}")

# La preuve automatique necessite le Dojo
SKIP_AUTO_PROOF = not ENABLE_AUTO_PROOF or not theorems or SKIP_DOJO

if not ENABLE_AUTO_PROOF:
    print("\n[MODE DEMO] Preuve automatique desactivee (ENABLE_AUTO_PROOF=False)")
    print("\nPour activer: mettez ENABLE_AUTO_PROOF = True dans la config principale.")
elif not theorems:
    print("\n[MODE DEMO] Pas de theoremes disponibles")
    print("Raison: Tracing desactive (ENABLE_TRACING=False)")
elif SKIP_DOJO:
    print("\n[MODE DEMO] Preuve automatique desactivee (ENABLE_DOJO_DEMO=False)")
    print("Raison: Le Dojo est necessaire pour la preuve automatique")

if SKIP_AUTO_PROOF:
    print("\nPattern de preuve automatique avec LeanRunner:")
    print('''
    # Avec LeanRunner et Dojo actif:
    result = runner.prove_with_tactics(
        theorem,
        ["intro", "intros", "rfl", "simp", "omega"]
    )
    
    print(f"Succes: {result['success']}")
    for step in result['steps']:
        print(f"  {step['tactic']}: {'OK' if step['success'] else 'FAIL'}")
    ''')
    
    print("\nExemple de sortie attendue:")
    print('''
    Theorem: hello_world
    Succes: True
    Steps: 1
      rfl: OK
    ''')
else:
    # Exécution réelle de la preuve automatique
    traced_thm = theorems[0]
    thm = traced_thm.theorem if hasattr(traced_thm, 'theorem') else traced_thm
    # Les théorèmes extraits referencent le depot par son chemin local dans le
    # cache (pas l'URL GitHub) : la cle de cache differe et le Dojo re-tracerait
    # tout le depot AVEC ses dependances (build_deps=True par defaut) -> OOM
    # sur une VM WSL a 8 Go. On re-ancre le théorème sur le depot d'origine
    # (cache hit direct) et on borne tout re-tracing eventuel a noDeps.
    if getattr(thm.repo, 'url', None) != repo.url:
        thm = Theorem(repo, thm.file_path, thm.full_name)

    name = thm.full_name if hasattr(thm, 'full_name') else str(thm)
    print(f"\n[PREUVE ACTIVE] Theoreme: {name}")
    
    tactics_sequence = ["intro", "intros", "rfl", "simp", "trivial", "omega", "decide"]
    
    with Dojo(thm) as (dojo, init_state):
        print(f"Buts initiaux: {len(init_state.goals)}")
        
        current_state = init_state
        proof_steps = []
        
        for tactic in tactics_sequence:
            if isinstance(current_state, ProofFinished):
                break
                
            result = dojo.run_tac(current_state, tactic)
            success = isinstance(result, (TacticState, ProofFinished))
            proof_steps.append({"tactic": tactic, "success": success})
            
            if success:
                current_state = result
        
        # Afficher le résultat
        proof_complete = isinstance(current_state, ProofFinished)
        print(f"\nSucces: {proof_complete}")
        print(f"Steps executees: {len(proof_steps)}")
        for step in proof_steps:
            status = "OK" if step["success"] else "FAIL"
            print(f"  {step['tactic']}: {status}")
            
print(f"\n[TIMER] Preuve automatique: {timer.format(timer.stop())}")

============================================================
PREUVE AUTOMATIQUE
============================================================

ENABLE_AUTO_PROOF: True

[PREUVE ACTIVE] Theoreme: hello_world
Buts initiaux: 1

Succes: True
Steps executees: 6
  intro: FAIL
  intros: OK
  rfl: FAIL
  simp: FAIL
  trivial: FAIL
  omega: OK

[TIMER] Preuve automatique: 1.1s

Interpretation : Preuve Automatique Executee

Résultat : La preuve automatique est executee conditionnellement par SKIP_AUTO_PROOF = not ENABLE_AUTO_PROOF or not theorems or SKIP_DOJO. La sortie reelle est imprimee dynamiquement par la cellule ci-dessus.

Quatre cas de figure (sortie reelle = voir cellule ci-dessus) :

Mode	Sortie typique
lean_dojo + theorems + Dojo + AutoProof ON	[PREUVE ACTIVE] Theoreme: hello_world / Succes: True/False / Steps executees: N
ENABLE_AUTO_PROOF = False	[MODE DEMO] Preuve automatique desactivee (ENABLE_AUTO_PROOF=False)
Theorems absents	[MODE DEMO] Pas de theoremes disponibles / Raison: Tracing desactive (lean_dojo absent)
SKIP_DOJO	[MODE DEMO] Preuve automatique desactivee (ENABLE_DOJO_DEMO=False)

Mode SKIP_AUTO_PROFF (demo) : la cellule imprime le pattern de preuve et un exemple de sortie attendue.

Lecture de la sortie en mode lean_dojo : chaque tactique de la sequence est tentee dans l’ordre. - Une tactique qui ne s’applique pas au but retourne LeanError -> marquee FAIL, on essaie la suivante (l’etat de preuve n’est pas modifie). - Une tactique qui ferme tous les buts retourne ProofFinished -> Succes: True.

C’est le prouveur automatique le plus simple possible : une sequence fixe de tactiques candidates. Le pattern general :

tactics_sequence = ["intro", "intros", "rfl", "simp", "trivial", "omega", "decide"]

with Dojo(thm) as (dojo, state):
    for tactic in tactics_sequence:
        if isinstance(state, ProofFinished):
            break  # Preuve terminee

        result = dojo.run_tac(state, tactic)
        if isinstance(result, LeanError):
            continue  # Tactique invalide, essayer la suivante

        state = result  # TacticState (progres) ou ProofFinished

Strategies de recherche :

Strategie	Description	Efficacite
Sequence fixe	Liste predeterminee (montre ici)	Rapide mais limitee
Beam search	Garde les k meilleurs etats	Bon compromis
Monte Carlo Tree Search	Explore l’arbre de preuves	Tres efficace mais lent
LLM-guided	Demande au LLM a chaque etape	State-of-the-art 2025

9. Depots Avances

LeanDojo peut tracer des depots plus complexes. Voici quelques exemples notables :

formal-conjectures (Google DeepMind)

Conjectures mathematiques formalisees par l’équipe DeepMind. Contient des problemes ouverts et resolus.

Mathlib4

La bibliotheque mathematique principale de Lean 4. Le tracing complet prend plusieurs heures.

Note : Ces depots sont volumineux. Le premier tracing peut prendre 30 minutes a plusieurs heures.

# =============================================================================
# Depots avances disponibles
# =============================================================================
timer.start("Depots avances")
print("=" * 60)
print("DEPOTS AVANCES")
print("=" * 60)

ADVANCED_REPOS = {
    "formal-conjectures": {
        "url": "https://github.com/google-deepmind/formal-conjectures",
        "commit": "ce0a081ab74d625948c44da6022992e1f9db070a",
        "lean_version": "4.22.0",
        "description": "Google DeepMind formalized conjectures",
        "tracing_time": "30-60 min",
    },
    "mathlib4": {
        "url": "https://github.com/leanprover-community/mathlib4",
        "commit": "v4.15.0",
        "lean_version": "4.15.0",
        "description": "Bibliotheque mathematique Lean 4 (~4M lignes)",
        "tracing_time": "2-4 heures",
    },
}

print("\nDepots disponibles pour tests avances:")
print()

for name, info in ADVANCED_REPOS.items():
    print(f"  {name}")
    print(f"    Description: {info['description']}")
    print(f"    Lean version: {info['lean_version']}")
    print(f"    Temps de tracing: {info['tracing_time']}")
    print()
print(f"[TIMER] Depots avances: {timer.format(timer.stop())}")

============================================================
DEPOTS AVANCES
============================================================

Depots disponibles pour tests avances:

  formal-conjectures
    Description: Google DeepMind formalized conjectures
    Lean version: 4.22.0
    Temps de tracing: 30-60 min

  mathlib4
    Description: Bibliotheque mathematique Lean 4 (~4M lignes)
    Lean version: 4.15.0
    Temps de tracing: 2-4 heures

[TIMER] Depots avances: 0ms

Interpretation : Depots Avances Listes

Résultat : Deux depots avances sont configures pour experimentation.

Comparaison des depots :

Depot	Taille	Lean	Temps tracing	Complexite	Usage recommande
lean4-example	~2 théorèmes user	4.x	1-2 min (cache)	Pedagogique	Apprendre LeanDojo
formal-conjectures	~100 théorèmes	4.22.0	30-60 min	Recherche	Benchmarks DeepMind
mathlib4	bibliotheque tres etendue	4.15.0	2-4 heures	Production	Mathematiques formelles

formal-conjectures :

Depot de Google DeepMind contenant des conjectures mathematiques formalisees : - Problemes ouverts (non resolus) - Problemes resolus (avec preuves) - Ideal pour tester des prouveurs automatiques

Mathlib4 :

La bibliotheque mathematique de reference pour Lean 4 : - Utilisee par Terry Tao (medaille Fields) - plusieurs millions de lignes de code - Couvre : algebre, analyse, topologie, théorie des nombres, etc.

Conseil : Ne tracez Mathlib4 que si vous avez : - Une bonne connexion internet (~1 Go de téléchargement) - 10+ Go d’espace disque libre - 2-4 heures de temps libre - Un bon CPU (le tracing parallele utilise tous les cores)

Exemple : Tracing de formal-conjectures

Le code ci-dessous montre comment tracer le depot formal-conjectures.

Attention : Ce tracing telecharge Mathlib4 (~1 Go) et prend 30-60 minutes la première fois.

# =============================================================================
# Exemple avec formal-conjectures (decommenter pour exécuter)
# =============================================================================
print("=" * 60)
print("EXEMPLE FORMAL-CONJECTURES")
print("=" * 60)

print("\n[CODE COMMENTE] Decommentez pour executer")
print("\nCe code effectue les operations suivantes:")
print("  1. Cree une reference au depot formal-conjectures")
print("  2. Trace le depot (telecharge Mathlib4, ~1 Go)")
print("  3. Extrait les theoremes/conjectures")
print("\nTemps estime: 30-60 minutes (premiere fois)")

# Decommentez le code ci-dessous pour exécuter:
#
# if LEANDOJO_AVAILABLE:
#     deepmind_repo = LeanGitRepo(
#         ADVANCED_REPOS["formal-conjectures"]["url"],
#         ADVANCED_REPOS["formal-conjectures"]["commit"]
#     )
#
#     print(f"Tracing formal-conjectures...")
#     traced_deepmind = trace(deepmind_repo)
#
#     conjectures = list(traced_deepmind.get_traced_theorems())
#     print(f"Found {len(conjectures)} theorems/conjectures")
#
#     for c in conjectures[:10]:
#         # Handle TracedTheorem wrapper
#         inner = c.theorem if hasattr(c, 'theorem') else c
#         name = inner.full_name if hasattr(inner, 'full_name') else str(inner)
#         print(f"  - {name}")

============================================================
EXEMPLE FORMAL-CONJECTURES
============================================================

[CODE COMMENTE] Decommentez pour executer

Ce code effectue les operations suivantes:
  1. Cree une reference au depot formal-conjectures
  2. Trace le depot (telecharge Mathlib4, ~1 Go)
  3. Extrait les theoremes/conjectures

Temps estime: 30-60 minutes (premiere fois)

10. Integration avec les LLMs

LeanDojo est concu pour l’integration avec des LLMs. Le workflow typique est :

1. Extraire les théorèmes d'un depot
2. Ouvrir un Dojo pour un théorème
3. Formater l'état pour le LLM
4. Envoyer au LLM pour obtenir une tactique
5. Exécuter la tactique dans le Dojo
6. Repeter jusqu'a ce que la preuve soit complète ou echoue

Format du Prompt

Le LLM recoit l’état de preuve en format Lean et doit retourner une tactique valide.

# =============================================================================
# Formattage de l'état de preuve pour un LLM
# =============================================================================
timer.start("Integration LLM")
print("=" * 60)
print("INTEGRATION LLM")
print("=" * 60)

def format_state_for_llm(state):
    """
    Formate l'état de preuve pour envoi a un LLM.

    Le format est concu pour etre clair et non-ambigu :
    - Affiche l'état Lean en bloc de code
    - Demande une seule tactique en reponse

    Args:
        state: TacticState de LeanDojo ou objet avec attribut 'pp'

    Returns:
        str: Prompt formate pour le LLM
    """
    prompt = "Given the following Lean 4 proof state:\n\n"

    # Extraire le pretty-print
    pp_state = getattr(state, 'pp', str(state))
    prompt += f"```lean\n{pp_state}\n```\n\n"

    prompt += "Suggest the next tactic to apply. "
    prompt += "Respond with ONLY the tactic, no explanation."

    return prompt

# Demonstration
print("\nExemple de prompt pour un LLM:")
print("-" * 40)

# Creer un état mock pour la demo
class MockState:
    pp = """n m : Nat
h : n > 0
⊢ n + m = m + n"""

print(format_state_for_llm(MockState()))
print("-" * 40)

print("\nReponse attendue du LLM: 'omega' ou 'ring' ou 'simp [Nat.add_comm]'")
print(f"[TIMER] Integration LLM: {timer.format(timer.stop())}")

============================================================
INTEGRATION LLM
============================================================

Exemple de prompt pour un LLM:
----------------------------------------
Given the following Lean 4 proof state:

```lean
n m : Nat
h : n > 0
⊢ n + m = m + n
```

Suggest the next tactic to apply. Respond with ONLY the tactic, no explanation.
----------------------------------------

Reponse attendue du LLM: 'omega' ou 'ring' ou 'simp [Nat.add_comm]'
[TIMER] Integration LLM: 0ms

Interpretation : Prompt LLM Formate

Résultat : Demonstration du formatage d’un état de preuve pour un LLM.

Exemple de prompt genere :

Given the following Lean 4 proof state:

```lean
n m : Nat
h : n > 0
⊢ n + m = m + n

Suggest the next tactic to apply. Respond with ONLY the tactic, no explanation.

**Anatomie d'un état de preuve** :

| Élément | Signification | Exemple |
|---------|---------------|---------|
| `n m : Nat` | Hypotheses (variables) | Variables de type `Nat` |
| `h : n > 0` | Hypotheses (propositions) | Contrainte sur `n` |
| `⊢` | Turnstile (symbole de deduction) | "On doit prouver..." |
| `n + m = m + n` | But (goal) | Proposition a démontrer |

**Reponse attendue du LLM** :

Un LLM entraine sur Lean pourrait repondre :
- `omega` (décideur arithmetique)
- `ring` (tactique algébrique)
- `simp [Nat.add_comm]` (simplification avec lemme)

**Design du prompt** :

1. **Format Lean en bloc de code** : Aide le LLM a comprendre que c'est du code formel
2. **Instruction claire** : "ONLY the tactic, no explanation" evite les sorties verbeuses
3. **Pas de few-shot** : Pour un vrai système, ajoutez 3-5 exemples de (état, tactique) reussies

**Ameliorations possibles** :

- Ajouter les premises disponibles (lemmes de la stdlib)
- Inclure l'historique des tactiques déjà appliquees
- Donner des hints sur le type de problème (arithmetique, logique, etc.)

### Exemple Complet avec LLM (Pseudo-code)

Le code ci-dessous montre le pattern complet d'integration. Dans un cas réel, vous utiliseriez l'API OpenAI ou Anthropic.

```python
# =============================================================================
# Pattern d'integration LLM (pseudo-code)
# =============================================================================
print("=" * 60)
print("PATTERN D'INTEGRATION LLM")
print("=" * 60)

def prove_with_llm(theorem, max_steps=10):
    """
    Pseudo-code pour prouver un théorème avec un LLM.

    En pratique, remplacez call_llm() par un appel OpenAI/Anthropic.
    """
    proof_steps = []

    with Dojo(theorem) as (dojo, state):
        for step in range(max_steps):
            # 1. Vérifier si la preuve est terminee
            if isinstance(state, ProofFinished):
                return {"success": True, "steps": proof_steps}

            # 2. Formater l'état pour le LLM
            prompt = format_state_for_llm(state)

            # 3. Appeler le LLM (pseudo-code)
            # tactic = call_llm(prompt)  # OpenAI/Anthropic
            tactic = "simp"  # Placeholder

            # 4. Exécuter la tactique
            new_state = dojo.run_tac(state, tactic)

            # 5. Enregistrer le résultat
            proof_steps.append({
                "tactic": tactic,
                "success": not isinstance(new_state, LeanError)
            })

            # 6. Gerer l'echec
            if isinstance(new_state, LeanError):
                return {"success": False, "steps": proof_steps, "error": f"Invalid tactic: {tactic}"}

            state = new_state

    return {"success": False, "steps": proof_steps, "error": "Max steps reached"}

print("\nPattern prove_with_llm() defini.")
print("\nWorkflow:")
print("  1. Ouvrir Dojo")
print("  2. Boucle:")
print("     a. Formater etat -> LLM")
print("     b. LLM -> tactique")
print("     c. Executer tactique")
print("     d. Si echec ou succes, sortir")
print("  3. Retourner resultat")
print("\nVoir Lean-07-LLM-Integration-Lean-Python.ipynb pour implementation reelle")

Résultat : Pseudo-code du pattern complet de preuve avec LLM.

Workflow detaille :

Théorème non prouve
    ↓
Ouvrir Dojo
    ↓
État initial (goals, hypotheses)
    ↓
┌──────────────────────┐
│ Boucle de preuve     │
│  (max 10 steps)      │
├──────────────────────┤
│ 1. Buts restants ?   │──→ Non → SUCCES
│    ↓ Oui             │
│ 2. Formater état     │
│    ↓                 │
│ 3. Appel LLM         │──→ Obtenir tactique
│    ↓                 │
│ 4. Exécuter tactique │
│    ↓                 │
│ 5. Tactique valide ? │──→ Non → ECHEC
│    ↓ Oui             │
│ 6. Mettre a jour état│
│    ↓                 │
│ Retour au debut      │
└──────────────────────┘
    ↓
Résultat final

Metriques importantes :

Metrique	Description	Utilite
Taux de succes	% de théorèmes prouves	Performance globale
Nombre de steps moyen	Longueur moyenne des preuves	Efficacite
Temps par step	Latence LLM + Dojo	Optimisation
Tactiques invalides	% d’echecs de tactiques	Qualite du LLM

Comparaison avec un vrai système :

Le pseudo-code montre le pattern de base. Un système réel (comme ReProver ou LeanCopilot) ajoute : - Premises retrieval : Rechercher les lemmes pertinents dans Mathlib - Beam search : Essayer plusieurs tactiques en parallele - Backtracking : Revenir en arriere si une branche echoue - Fine-tuning : LLM entraine specifiquement sur Lean

Reference : Voir Lean-07-LLM-Integration-Lean-Python.ipynb et Lean-08-Agentic-Proving-Python.ipynb pour des implémentations réelles avec OpenAI/Anthropic.

Exercice 2 : Prompt LLM a partir de données LeanDojo

Difficulte : Intermediaire | Duree estimée : 15 minutes

LeanDojo extrait les théorèmes ET leurs premises (lemmes utilises dans la preuve). Utilisez ces informations pour construire un prompt LLM enrichi qui guide le modèle vers la bonne preuve.

Competences visees : - Exploiter les premises extraites par LeanDojo pour le prompting - Construire un prompt enrichi par les données de tracing - Comprendre le lien entre extraction de données et generation de preuves

# === EXERCICE 2 : Prompt LLM a partir de données LeanDojo ===
#
# Objectif : Construire un prompt LLM structure a partir des informations
# extraites par LeanDojo pour tenter de prouver un théorème automatiquement.
#
# Instructions :
# 1. Choisir un théorème simple parmi ceux extraits (ou utiliser un exemple) :
#    theorem_name = "Nat.add_comm"
#    theorem_statement = "theorem Nat.add_comm (n m : Nat) : n + m = m + n"
#    premises = ["Nat.add_zero", "Nat.succ_add", "Nat.zero_add"]
#
# 2. Construire un prompt qui inclut :
#    - Le théorème a prouver
#    - Les premises disponibles (lemmes utilisables)
#    - Une instruction pour utiliser les tactiques Lean 4
#    - Le format de sortie attendu (code Lean entre ```lean ... ```)
#
# 3. Afficher le prompt genere et estimer sa qualite :
#    - Contient-il le contexte complet ?
#    - Les premises sont-elles bien formatees ?
#    - Le format de sortie est-il clair pour le LLM ?
#
# 4. (Bonus) Si une API LLM est configuree, envoyer le prompt et vérifier
#    la reponse avec ProofVerifier (importe dans les cellules precedentes
#    si vous avez exécute Lean-7).
#
# Indices :
# - Les premises donnent au LLM les lemmes qu'il peut utiliser (exact, apply, rw)
# - Un bon prompt specifie Lean 4, pas Lean 3 (syntaxe différente)
# - Formater les premises comme : "Lemmes disponibles: Nat.add_zero, Nat.succ_add..."

# Exercice: Votre code ici
pass  # Exercice: completez cet exercice

print("Exercice 2 a completer : construire un prompt LLM depuis LeanDojo")

Exercice 2 a completer : construire un prompt LLM depuis LeanDojo

11. Bonnes Pratiques et Limitations

Bonnes Pratiques

Pratique	Raison
Utilisez le cache	Le tracing est couteux, le cache accelere les exécutions
Commit spécifique	Utilisez toujours un hash, jamais une branche
GitHub token	Evitez le rate limiting (60 req/h sans token)
WSL sur Windows	Le tracing natif Windows peut se bloquer
Python 3.10-3.12	LeanDojo n’est pas compatible avec Python 3.13+

Limitations Connues

Limitation	Impact	Contournement
Lean 4 only	LeanDojo 4.x ne supporte pas Lean 3	Utiliser LeanDojo 1.x pour Lean 3
lean-toolchain	Le depot doit avoir ce fichier	Ajouter manuellement si manquant
Python < 3.13	Dependances incompatibles	Utiliser conda/venv
Espace disque	Mathlib4 ~5 Go	Prevoir de l’espace
Windows natif	Tracing peut bloquer	Utiliser WSL

References

• LeanDojo Documentation
• LeanDojo Paper (NeurIPS 2023)
• lean4-example Repository
• ReProver - Theorem prover base sur LeanDojo

Resume

Dans ce notebook, nous avons couvert :

Section	Contenu
1-3	Installation, configuration, imports
4	Creation de references de depot (LeanGitRepo)
5	Tracing et cache
6	Extraction des théorèmes
7	Environnement Dojo et exécution de tactiques
8	Interface simplifiee lean_runner.py
9	Depots avances (formal-conjectures, Mathlib4)
10	Integration avec les LLMs

Points cles a retenir

1. LeanDojo permet l’interaction programmatique avec Lean 4
2. Le tracing est l’opération centrale (compile et extrait les metadonnees)
3. Le Dojo permet d’exécuter des tactiques une par une
4. Le cache (~/.cache/lean_dojo/) accelere les exécutions suivantes
5. Sur Windows, utilisez WSL pour eviter les blocages

Prochaines étapes

• Lean-07-LLM-Integration-Lean-Python.ipynb : Patterns d’integration LLM-Lean avec vraies APIs
• Lean-08-Agentic-Proving-Python.ipynb : Agents autonomes pour la preuve de théorèmes

12. Resume des Temps d’Exécution

Cette cellule affiche un resume de tous les temps mesures pendant l’exécution du notebook.

# =============================================================================
# Resume des temps d'exécution
# =============================================================================
timer.summary()

============================================================
RESUME DES TEMPS D'EXECUTION
============================================================
  Verification environnement: 0ms
  Import LeanDojo: 1.4s
  Creation repo reference: 1.4s
  Verification cache: 767ms
  Tracing: 13.0s
  Extraction theoremes: 1ms
  Details theoreme: 0ms
  Dojo ouverture: 1.5s
  Execution tactiques: 960ms
  Extraction theoremes lean_runner: 0ms
  Preuve automatique: 1.1s
  Depots avances: 0ms
  Integration LLM: 0ms
  TOTAL: 22.7s
============================================================

Interpretation : Resume des Temps

Résultat : La cellule ci-dessus (timer.summary()) imprime le detail des temps d’exécution sur la machine courante. Les valeurs absolues dependent de la machine (CPU, charge, cache, taille du depot, etc.) ; le tableau ci-dessous est une decomposition structurelle qualitative de ce que la cellule dynamique affiche.

Decomposition structurelle (les valeurs réelles sont dans la sortie de la cellule ci-dessus) :

Opération	Note structurelle
Tracing	Etape dominante (~90% du temps total en mode demo cache-hit, charge les metadonnees du depot et de ses dependances stdlib Lean 4)
Extraction théorèmes	Tres rapide (filtrage sur les metadonnees deja chargees)
Import LeanDojo	Rapide (initialisation Ray)
Autres	Negligeable (vérification env, config, etc.)

Analyse de performance :

1. Le tracing domine : il represente l’essentiel du temps total en mode cache-hit.

   • Sans cache, le premier tracing peut prendre plusieurs minutes (compilation + extraction).
   • Avec cache, le tracing est rapide mais reste l’etape la plus lourde – voir la sortie de la cellule ci-dessus pour la valeur mesuree.

2. Opérations rapides : les etapes de preparation (vérification environnement, configuration, lecture .env, scan du cache) sont chacune de l’ordre de la milliseconde a la seconde ; voir la sortie dynamique pour les valeurs exactes.

3. Dojo/Preuve skippees : en mode demo, les etapes Dojo interactif et preuve automatique sont desactivees ; en mode complet elles ajouteraient plusieurs dizaines de minutes.

Optimisations possibles (gains mesures sur la machine de l’auteur, susceptibles de varier) :

Optimisation	Effet attendu	Difficulte
Lazy loading des théorèmes	Reduit la phase d’extraction	Facile
Cache Ray pre-initialise	Reduit l’etape d’import LeanDojo	Moyen
Tracing incrementiel	Reduit la recompilation quand le depot a deja ete trace	Difficile
Parallelisation Dojo	Variable selon la structure des preuves	Tres difficile

Conclusion : ce notebook s’exécute en quelques minutes en mode demo, ce qui est ideal pour l’apprentissage. Pour une exécution complète avec Dojo interactif, voir la cellule finale pour le temps réel sur la machine courante et la note de duree estimée en en-tete du notebook.

Exercice 3 : Synthese - Pipeline LeanDojo -> LLM -> Lean

Difficulte : Avance | Duree estimée : 30-45 minutes

Vous avez decouvert les briques individuelles : extraction LeanDojo (Exercice 1), prompting LLM (Exercice 2), et exécution interactive via Dojo (sections 7-8). Cet exercice les combine en un pipeline complet, non resolu : c’est a vous de l’implementer.

Objectif : Construire un pipeline end-to-end qui, etant donne un théorème cible et un depot trace, tente de prouver automatiquement le théorème via un LLM, avec une boucle d’itération sur les echecs.

Pourquoi cet exercice : - C’est exactement le pattern utilise par les systèmes de recherche en theorem proving (ReProver, LeanCopilot) - Il combine données + LLM + validation formelle : trois piliers de l’AI4Math moderne - Comprendre ce pipeline est prerequis pour contribuer a ces projets de recherche

Architecture cible

[théorème cible]
       |
       v
[LeanDojo.trace + extract premises]
       |
       v
[Construction prompt LLM enrichi]   <----+
       |                                 |
       v                                 |
[LLM genere preuve candidate]            |
       |                                 |
       v                                 |
[Dojo exécute la preuve]                 |
       |                                 |
       +-- succes --> retourner la preuve|
       |                                 |
       +-- echec --> reformuler prompt --+ (max N itérations)

Squelette de fonction a completer

Implementez la fonction pipeline_leandojo_llm ci-dessous. Les briques (tracing, LLM, Dojo) sont déjà disponibles dans le notebook au-dessus.

def pipeline_leandojo_llm(target_theorem_name: str, traced_repo, max_iterations: int = 3):
    """
    Pipeline LeanDojo -> LLM -> Lean : prouve un théorème via boucle LLM iterative.

    Args:
        target_theorem_name: Nom du théorème a prouver (ex: "Nat.add_comm")
        traced_repo: Résultat de LeanDojo.trace() (ou objet mock)
        max_iterations: Nombre max d'itérations en cas d'echec

    Returns:
        dict avec keys :
          - success (bool)
          - final_proof (str, preuve Lean valide si success=True)
          - itérations (int, nombre d'itérations consommees)
          - error_history (list[str], erreurs rencontrees a chaque iter)
    """
    # TODO étudiant : implementer les 6 étapes
    # 1. Localiser le théorème dans traced_repo (filtrer par nom)
    # 2. Extraire les premises (premise_set ou theorem.premises)
    # 3. Construire le prompt enrichi (reutiliser le pattern Exercice 2)
    # 4. Boucle (max_iterations) :
    #    a. Appeler le LLM (mock dict simple OU openai/anthropic si keys dispo)
    #    b. Parser la preuve generee (extraire le bloc 'by ...' ou tactique)
    #    c. Tenter la validation via Dojo.run_tac(s) ou lean_runner.prove(...)
    #    d. Si succes : retourner. Si echec : capturer l'erreur, reformuler prompt
    # 5. Si toutes itérations consommees sans succes : retourner success=False
    return None  # TODO étudiant

Test de votre pipeline

# A exécuter après avoir implemente pipeline_leandojo_llm :
#
# result = pipeline_leandojo_llm(
#     target_theorem_name="Nat.add_zero",
#     traced_repo=traced_repo,  # disponible si vous avez exécute le tracing au-dessus
#     max_iterations=3
# )
# print(result)
#
# Sortie attendue (success case) :
# {
#   'success': True,
#   'final_proof': 'by simp',
#   'itérations': 1,
#   'error_history': []
# }

Variantes / extensions

Une fois le pipeline de base fonctionnel :

1. Multi-modèles : comparer GPT-4 vs Claude vs Qwen sur le même théorème. Lequel propose le plus souvent une preuve correcte au premier coup ?
2. Premises filtering : limiter les premises envoyees au LLM aux 5 plus pertinentes (TF-IDF, embeddings). Effet sur le taux de succes ?
3. Tactic-level vs proof-level : demander au LLM une tactique a la fois (et iterer dans le Dojo après chaque) plutot qu’une preuve complète. Quel pattern marche mieux ?
4. Erreur-aware prompting : a l’itération N+1, inclure l’erreur compilateur de l’itération N dans le prompt. Mesurer le gain.

Pour aller plus loin

Cet exercice est la base du papier ReProver (NeurIPS 2023). Comparez votre implémentation avec leur code (https://github.com/lean-dojo/ReProver) pour identifier les optimisations productives utilisees en recherche.

---

# === EXERCICE 3 : Pipeline LeanDojo -> LLM -> Lean ===
#
# Objectif : Construire un pipeline end-to-end qui, etant donné un théorème
# cible et un depot trace, tente de prouver le théorème via un LLM,
# avec une boucle d'iteration sur les echecs.
#
# Architecture :
#   [théorème cible] -> [LeanDojo trace + extract premises]
#   -> [Prompt LLM enrichi] -> [LLM genere preuve candidate]
#   -> [Dojo exécute] -> succes/echec -> (iteration si echec)

def pipeline_leandojo_llm(target_theorem_name: str, traced_repo, max_iterations: int = 3):
    """
    Pipeline LeanDojo -> LLM -> Lean : prouve un théorème via boucle LLM iterative.

    Args:
        target_theorem_name: Nom du théorème a prouver (ex: "Nat.add_comm")
        traced_repo: Résultat de LeanDojo.trace() (ou objet mock)
        max_iterations: Nombre max d'iterations en cas d'echec

    Returns:
        dict avec keys :
          - success (bool)
          - final_proof (str, preuve Lean valide si success=True)
          - iterations (int, nombre d'iterations consommees)
          - error_history (list[str], erreurs rencontrees a chaque iter)
    """
    # TODO étudiant : implementer les 6 etapes
    # Etape 1 : Localiser le théorème dans traced_repo (filtrer par nom)
    # Etape 2 : Extraire les premises (premise_set ou theorem.premises)
    # Etape 3 : Construire le prompt enrichi (reutiliser le pattern Exercice 2)
    # Etape 4 : Boucle (max_iterations) :
    #   a. Appeler le LLM (mock dict simple OU openai/anthropic si keys dispo)
    #   b. Parser la preuve generee (extraire le bloc 'by ...' ou tactique)
    #   c. Tenter la validation via Dojo.run_tac(s) ou lean_runner.prove(...)
    #   d. Si succes : retourner. Si echec : capturer l'erreur, reformuler prompt
    # Etape 5 : Si toutes iterations consommees sans succes : retourner success=False
    return None  # TODO etudiant : remplacer par l'implementation

print("Exercice 3 a completer : pipeline LeanDojo -> LLM -> Lean avec boucle iterative")

Exercice 3 a completer : pipeline LeanDojo -> LLM -> Lean avec boucle iterative

---

Navigation : << Lean-09-SK-Multi-Agents-Lean-Python | Index | Lean-10b-LeanDojo-v2 >>