Lean 7 - Integration des LLMs pour l’Assistance aux Preuves

Navigation : ← Lean-06-Mathlib-Essentials-Lean | Index | Lean-08-Agentic-Proving-Python →

Introduction

L’annee 2024-2026 a marque un tournant decisif dans l’histoire des mathematiques formelles. Les Large Language Models (LLMs) ont commence a prouver des théorèmes de maniere autonome, avec des succes spectaculaires qui ont bouleverse la communaute mathematique :

  • AlphaProof (DeepMind) : Medaille d’argent aux Olympiades Internationales de Mathematiques 2024, publie dans Nature en novembre 2025
  • Harmonic Aristotle (Harmonic, Palo Alto, fondation 2023 Vlad Tenev + Tudor Achim) : Medaille d’or IMO 2025 (5/6 problemes resolus, arXiv:2510.01346)
  • DeepSeek-Prover (DeepSeek) : Système specialise theorem proving Lean 4 (papers 2024-2025), pas de resolution Erdos numerotee vérifiée en source primaire
  • LeanCopilot (LeanDojo) : Automatisation de 74.2% des étapes de preuves sur le textbook “Mathematics in Lean” (eval hors-Mathlib), papier Song, Yang, Anandkumar (arXiv:2404.12534)
  • LeanAgent : Apprentissage lifelong pour theorem proving, papier ICLR 2025

Ce notebook explore comment utiliser les LLMs pour accelerer et assister la construction de preuves Lean, en s’appuyant sur ces avancees recentes.

Objectifs pedagogiques

  1. Comprendre les percees recentes en theorem proving assiste par LLM
  2. Decouvrir LeanCopilot, LeanProgress et l’ecosysteme LeanDojo
  3. Maitriser les patterns de collaboration humain-LLM-Lean
  4. Experimenter le prompting efficace pour generer des preuves
  5. Comprendre les architectures d’AlphaProof, APOLLO et LeanAgent

Prerequis

  • Notebooks Lean-1 a Lean-6 completes
  • Cle API OpenAI ou Anthropic (optionnel pour les exercices pratiques)

Duree estimée : 50-55 minutes

L’Ere des LLMs en Mathematiques Formelles

Timeline des percees majeures

Date Système Accomplissement
Juillet 2024 AlphaProof Medaille d’argent IMO 2024 (4 problemes sur 6, 28/42 points)
Octobre 2024 LeanCopilot Papier “Lean Copilot” (arXiv:2404.12534), 74.2% automatisation Textbook “Mathematics in Lean” (eval hors-Mathlib)
Novembre 2025 AlphaProof Publication dans Nature, details sur 100M problemes d’entrainement
Decembre 2025 Harmonic Aristotle API publique post-Series A (75M Sequoia Cap, Sept 2024)
Janvier 2026 LeanAgent Papier ICLR 2025 sur apprentissage lifelong
Janvier 2026 LeanProgress Papier TMLR 2025 sur prediction de progression
Janvier 2026 Lean4Lean Presentation POPL 2026, bootstrap de Lean en Lean
Juillet 2025 Harmonic Aristotle Medaille d’or IMO 2025

1. AlphaProof : L’Architecture de DeepMind

1.1 Vue d’ensemble (Nature, Novembre 2025)

AlphaProof est le premier système d’IA a atteindre le niveau medaille aux Olympiades Internationales de Mathematiques. Publie dans Nature en novembre 2025, il combine plusieurs innovations :

  1. Fine-tuning de Gemini sur des preuves formelles Lean
  2. Apprentissage par renforcement (AlphaZero-style) pour guider la recherche de preuves
  3. Generation de 100 millions de théorèmes synthetiques pour l’entrainement
  4. Vérification formelle systématique avec Lean comme oracle de verite

1.2 Résultats IMO 2024

Problème Difficulte Points Temps
P1 Facile 7/7 Minutes
P2 Moyen 7/7 Heures
P3 Difficile 0/7 Timeout
P4 Moyen 7/7 Heures
P5 Difficile 0/7 Non resolu
P6 Très difficile 7/7 3 jours
Total 28/42 Medaille Argent

Note : P6, le problème le plus difficile (seulement 5 participants humains l’ont resolu), a ete resolu en 3 jours par AlphaProof.

1.3 Le cycle AlphaProof

flowchart TD
    E["Enoncé (langage naturel)"] --> F["Formalisation en Lean (modèle Gemini fine-tuné)"]
    F --> G["Génération de tactiques (LLM + MCTS) — recherche guidée par valeur, équilibre exploration/exploitation"]
    G --> V{"Vérification Lean"}
    V -- "Succès" --> P["Preuve"]
    V -- "Succès (itération)" --> N["Nouvelle tentative"]
    V -- "Échec (feedback erreur Lean)" --> R["Apprentissage par renforcement (mise à jour de la politique)"]
    N --> F
    R --> F

1.4 Details techniques (du papier Nature)

  • Modèle de base : Gemini fine-tune sur ~1M preuves formelles existantes
  • Self-play : Generation de 100M problemes synthetiques avec preuves
  • Recherche : Monte Carlo Tree Search (MCTS) guide par un reseau de valeur
  • Hardware : TPU v4 clusters pour l’entrainement, evaluation en parallele
# Exemple conceptuel du flux AlphaProof
# (Ce code illustre le principe, pas l'implémentation réelle)

class AlphaProofConcept:
    """Illustration conceptuelle de l'architecture AlphaProof."""
    
    def __init__(self, llm, lean_verifier):
        self.llm = llm
        self.lean = lean_verifier
        self.max_attempts = 1000
    
    def prove(self, theorem_statement: str) -> str:
        """Tente de prouver un théorème."""
        # Etape 1: Formaliser l'enonce
        formal_statement = self.formalize(theorem_statement)
        
        for attempt in range(self.max_attempts):
            # Etape 2: Generer des tactiques
            tactics = self.llm.generate_tactics(formal_statement)
            
            # Etape 3: Vérifier avec Lean
            result = self.lean.verify(formal_statement, tactics)
            
            if result.success:
                return tactics
            
            # Etape 4: Utiliser le feedback pour ameliorer
            self.llm.learn_from_error(result.error_message)
        
        raise ProofNotFound("Limite de tentatives atteinte")

print("Architecture AlphaProof illustree")
Architecture AlphaProof illustree

2. LeanCopilot et l’Ecosysteme LeanDojo

2.1 Presentation

LeanDojo (https://leandojo.org) est un ecosysteme complet pour le machine learning sur les preuves Lean, developpe par une équipe de recherche incluant Caltech, Stanford et MIT. Il comprend plusieurs composants :

Outil Description Publication
LeanDojo Framework d’extraction de données et interaction avec Lean NeurIPS 2023
LeanCopilot Copilote LLM integre dans Lean/VS Code NeurIPS 2025
LeanProgress Prediction du nombre d’étapes restantes TMLR 2025
LeanAgent Apprentissage lifelong pour theorem proving ICLR 2025

2.2 LeanCopilot (NeurIPS 2025)

LeanCopilot (https://github.com/lean-dojo/LeanCopilot) integre des LLMs directement dans Lean 4 pour suggerer des tactiques en temps réel.

Résultats cles : - 74.2% des étapes de preuves sur le textbook “Mathematics in Lean” peuvent etre automatisees (arXiv:2404.12534, Song et al. 2024) - 85% meilleur que aesop (40.1%) sur ce jeu de données - Integration transparente avec VS Code - Modèles locaux (Llama) ou API (GPT-4, Claude)

Fonctionnalite Description Exemple
suggest_tactics Suggere des tactiques pour le but courant by suggest_tactics
search_proofs Recherche complète de preuves by search_proofs
select_premises Selectionne les lemmes pertinents Filtrage intelligent

2.3 LeanProgress (TMLR 2025)

LeanProgress predit combien d’étapes il reste pour completer une preuve, permettant de guider la recherche plus efficacement.

  • Entraine sur des traces de preuves Mathlib
  • Predit le “progress” (0-1) vers la completion
  • Utilise comme heuristique dans la recherche de preuves

2.4 LeanAgent (ICLR 2025)

LeanAgent introduit l’apprentissage continu (lifelong learning) pour le theorem proving :

  • Curriculum automatique : Commence par des théorèmes simples, progresse vers les difficiles
  • Mémoire des preuves passees : Reutilise les patterns appris
  • Adaptation dynamique : S’ameliore au fil des interactions

2.5 Architecture LeanDojo

flowchart LR
    subgraph eco["Écosystème LeanDojo"]
        L["Lean 4 (vérificateur)"]
        D["LeanDojo (extraction de données)"]
        M["Modèles ML (ReProver, etc.)"]
        C["LeanCopilot (suggestions de tactiques)"]
        P["LeanProgress (prédiction du progrès)"]
        A["LeanAgent (lifelong learning)"]
    end
    L <--> D
    D <--> M
    D --> C
    M --> P
    C --> L
# Exemple d'utilisation de LeanCopilot (necessite installation)

LEANCOPILOT_EXAMPLE = """
-- import LeanCopilot

-- theorem example_copilot (n : Nat) : n + 0 = n := by
--   suggest_tactics  -- LeanCopilot suggere: rfl, simp, exact Nat.add_zero n

-- theorem harder_example (a b c : Nat) : (a + b) + c = a + (b + c) := by
--   suggest_tactics  -- Suggere: exact Nat.add_assoc a b c

-- Sans LeanCopilot, on fait manuellement:
theorem manual_example (n : Nat) : n + 0 = n := by
  rfl  -- ou exact Nat.add_zero n
"""

print("Exemple LeanCopilot (code Lean):")
print(LEANCOPILOT_EXAMPLE)
Exemple LeanCopilot (code Lean):

-- import LeanCopilot

-- theorem example_copilot (n : Nat) : n + 0 = n := by
--   suggest_tactics  -- LeanCopilot suggere: rfl, simp, exact Nat.add_zero n

-- theorem harder_example (a b c : Nat) : (a + b) + c = a + (b + c) := by
--   suggest_tactics  -- Suggere: exact Nat.add_assoc a b c

-- Sans LeanCopilot, on fait manuellement:
theorem manual_example (n : Nat) : n + 0 = n := by
  rfl  -- ou exact Nat.add_zero n

2.6 Installation de LeanCopilot

LeanCopilot s’installe via Lake en ajoutant la dépendance au lakefile.lean. Il necessite un modèle LLM (local ou API) et s’integre dans VS Code pour les suggestions en temps réel.

# Dans lakefile.lean de votre projet:

# require LeanCopilot from git
#   "https://github.com/lean-dojo/LeanCopilot.git"

# Puis:
# lake update
# lake build

# Configuration de l'API (dans .env ou variable d'environnement)
# OPENAI_API_KEY=sk-...
print("Configuration lakefile et API - voir commentaires ci-dessus")
Configuration lakefile et API - voir commentaires ci-dessus

3. Patterns de Collaboration Humain-LLM-Lean

3.1 “Vibe Coding” avec ChatGPT/Claude

L’approche la plus simple : utiliser un LLM conversationnel pour esquisser des preuves.

# Exemple de prompt pour "vibe coding" avec un LLM

VIBE_CODING_PROMPT = """
Je travaille sur une preuve Lean 4. Voici mon théorème:

```lean
theorem my_theorem (a b : Nat) : a + b = b + a := by
  sorry
```

Comment puis-je completer cette preuve? 
Donne-moi le code Lean exact avec les tactiques appropriees.
"""

# Reponse typique du LLM:
LLM_RESPONSE = """
Pour prouver la commutativite de l'addition sur Nat, vous pouvez utiliser:

```lean
theorem my_theorem (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b
```

Ou avec une preuve plus detaillee par recurrence:

```lean
theorem my_theorem (a b : Nat) : a + b = b + a := by
  induction b with
  | zero => simp [Nat.add_zero, Nat.zero_add]
  | succ n ih => simp [Nat.add_succ, Nat.succ_add, ih]
```
"""

print("Exemple de vibe coding:")
print(VIBE_CODING_PROMPT[:100] + "...")
Exemple de vibe coding:

Je travaille sur une preuve Lean 4. Voici mon théorème:

```lean
theorem my_theorem (a b : Nat) : a...

3.2 Proof Sketching

Le proof sketching consiste a utiliser le LLM pour generer la structure d’une preuve, puis a completer les details manuellement. Le LLM excelle pour identifier les étapes cles.

# Exemple de proof sketch genere par LLM

PROOF_SKETCH_EXAMPLE = """
-- LLM genere la structure:
theorem distributivity (a b c : Nat) : a * (b + c) = a * b + a * c := by
  -- Etape 1: Recurrence sur c (suggere par LLM)
  induction c with
  | zero => 
    -- Cas de base: a * (b + 0) = a * b + a * 0
    simp   -- Humain complète
  | succ n ih =>
    -- Cas inductif: utiliser l'hypothese de recurrence
    -- (Details a completer par l'humain)
    simp [Nat.add_succ, Nat.mul_succ]
    omega  -- ou linarith avec Mathlib
"""

print("Exemple de proof sketch (code Lean):")
print(PROOF_SKETCH_EXAMPLE)
Exemple de proof sketch (code Lean):

-- LLM genere la structure:
theorem distributivity (a b c : Nat) : a * (b + c) = a * b + a * c := by
  -- Etape 1: Recurrence sur c (suggere par LLM)
  induction c with
  | zero => 
    -- Cas de base: a * (b + 0) = a * b + a * 0
    simp   -- Humain complète
  | succ n ih =>
    -- Cas inductif: utiliser l'hypothese de recurrence
    -- (Details a completer par l'humain)
    simp [Nat.add_succ, Nat.mul_succ]
    omega  -- ou linarith avec Mathlib

3.3 DeepAlgebra Loop

La boucle DeepAlgebra est un pattern iteratif ou le LLM genere une preuve, Lean la vérifie, et le feedback d’erreur est utilise pour corriger. Chaque itération affine la preuve.

# Simulation de la boucle DeepAlgebra

def deep_algebra_loop(theorem: str, max_iterations: int = 10):
    """
    Boucle iterative d'amelioration de preuve.
    
    1. LLM genere une preuve
    2. Lean vérifie
    3. Si erreur -> feedback au LLM
    4. LLM corrige et recommence
    """
    
    history = []
    current_proof = None
    
    for i in range(max_iterations):
        # Generer ou corriger la preuve
        if current_proof is None:
            prompt = f"Genere une preuve Lean 4 pour: {theorem}"
        else:
            prompt = f"""
            Preuve precedente: {current_proof}
            Erreur Lean: {last_error}
            Corrige la preuve.
            """
        
        # Simuler la reponse LLM
        current_proof = f"-- Iteration {i+1}\nby simp"
        
        # Simuler la vérification Lean
        lean_result = {"success": i >= 3, "error": "unknown tactic"}
        
        history.append({
            "iteration": i + 1,
            "proof": current_proof,
            "result": lean_result
        })
        
        if lean_result["success"]:
            print(f"Preuve trouvee en {i+1} iterations!")
            return current_proof
        
        last_error = lean_result["error"]
    
    return None

# Demonstration
result = deep_algebra_loop("theorem test : 1 + 1 = 2")
Preuve trouvee en 4 iterations!

3.4 APOLLO : Collaboration Automatique LLM-Lean

APOLLO (https://arxiv.org/abs/2505.05758) pousse l’automatisation au maximum avec une boucle entierement autonome :

Caractéristiques : - Generation massive de candidats de preuve (milliers en parallele) - Filtrage par vérification formelle avec Lean - Optimisation par apprentissage sur les succes/echecs - Aucune intervention humaine requise après lancement

Résultats : - Amelioration de 20-30% sur les benchmarks miniF2F - Capable de resoudre des théorèmes Mathlib non trivaux - Temps median de resolution : quelques minutes par théorème

Principe : Au lieu de generer une seule preuve et iterer, APOLLO genere des milliers de candidats varies simultanement, les filtre par vérification Lean, et utilise les patterns des succes pour ameliorer la generation future.

3.5 Comparaison des approches

Approche Automatisation Forces Faiblesses
Vibe coding Faible Accessibilite, flexibilite Lent, expertise requise
LeanCopilot Moyenne Temps réel, IDE integre Modèle local limite
DeepAlgebra Loop Haute Apprentissage iteratif Feedback delays
APOLLO Très haute Parallelisme massif Cout computationnel
AlphaProof Complète Performance SOTA Ressources enormes 
# Architecture conceptuelle APOLLO

class APOLLOConcept:
    """
    APOLLO : Automated Proving with LLM-Lean Optimization
    
    Caractéristiques:
    - Generation parallele massive de preuves candidates
    - Vérification formelle systématique
    - Self-play pour l'amelioration
    """
    
    def __init__(self, num_workers: int = 100):
        self.num_workers = num_workers
        self.successful_proofs = []
    
    def prove_massively(self, theorem: str, num_candidates: int = 10000):
        """
        Genere des milliers de candidats en parallele.
        """
        candidates = []
        
        # Phase 1: Generation massive
        for i in range(num_candidates):
            # Variation de temperature et de prompts
            candidate = self.generate_candidate(
                theorem, 
                temperature=0.5 + (i % 10) * 0.1
            )
            candidates.append(candidate)
        
        # Phase 2: Vérification parallele
        verified = self.verify_parallel(candidates)
        
        # Phase 3: Retourner les succes
        successes = [c for c in verified if c["valid"]]
        
        return successes
    
    def generate_candidate(self, theorem: str, temperature: float):
        """Genere un candidat de preuve."""
        return f"-- candidate with temp {temperature}"
    
    def verify_parallel(self, candidates):
        """Vérifie les candidats en parallele."""
        return [{"proof": c, "valid": True} for c in candidates[:3]]

print("Architecture APOLLO illustree")
Architecture APOLLO illustree

4. Prompting Efficace pour Lean

Le prompting pour Lean necessite precision : specifier la version (Lean 4), les imports disponibles, le contexte (hypotheses), et le style de preuve souhaite (termes ou tactiques).

# Templates de prompts efficaces pour Lean

PROMPTS = {
    "basic": """
Ecris une preuve Lean 4 pour le théorème suivant:

```lean
{theorem}
```

Utilise des tactiques standard (apply, exact, intro, rw, simp).
    """,
    
    "with_context": """
Je travaille dans Lean 4 avec les imports suivants:
{imports}

Voici les hypotheses disponibles:
{hypotheses}

Je dois prouver:
{goal}

Quelle sequence de tactiques dois-je utiliser?
    """,
    
    "iterative": """
Ma preuve actuelle:
```lean
{current_proof}
```

Erreur Lean:
```
{error}
```

Comment corriger cette erreur? Donne la preuve complète corrigee.
    """,
    
    "expert": """
Tu es un expert en Lean 4 et Mathlib4. 

Théorème a prouver:
{theorem}

Contraintes:
- Utilise les tactiques Mathlib si appropriees (ring, linarith, omega, simp)
- Préfère les preuves courtes et elegantes
- Commente les etapes non triviales

Fournis le code Lean complet.
    """
}

print("Templates de prompts disponibles:")
for name in PROMPTS:
    print(f"  - {name}")
Templates de prompts disponibles:
  - basic
  - with_context
  - iterative
  - expert

4.2 Bonnes pratiques

  • Inclure le contexte complet (imports, variables, hypotheses)
  • Demander des tactiques spécifiques plutot que des preuves completes
  • Fournir des exemples similaires (few-shot)
  • Iterer avec les messages d’erreur Lean
# Bonnes pratiques pour le prompting Lean

BEST_PRACTICES = """
### Prompting efficace pour preuves Lean

1. **Contexte precis**
   - Specifier la version de Lean (4.x)
   - Mentionner les imports disponibles
   - Donner les hypotheses du contexte

2. **But clair**
   - Formuler le théorème exactement
   - Preciser le type des variables
   - Indiquer si c'est sur Nat, Int, Real, etc.

3. **Contraintes**
   - Tactiques preferees ou interdites
   - Style de preuve (term-mode vs tactic-mode)
   - Longueur souhaitee

4. **Feedback iteratif**
   - Inclure les erreurs Lean exactes
   - Montrer la preuve partielle
   - Demander des corrections specifiques

5. **Exemples similaires**
   - Donner des preuves similaires reussies
   - Montrer le style attendu
   - Few-shot learning ameliore les résultats
"""

print(BEST_PRACTICES)

### Prompting efficace pour preuves Lean

1. **Contexte precis**
   - Specifier la version de Lean (4.x)
   - Mentionner les imports disponibles
   - Donner les hypotheses du contexte

2. **But clair**
   - Formuler le théorème exactement
   - Preciser le type des variables
   - Indiquer si c'est sur Nat, Int, Real, etc.

3. **Contraintes**
   - Tactiques preferees ou interdites
   - Style de preuve (term-mode vs tactic-mode)
   - Longueur souhaitee

4. **Feedback iteratif**
   - Inclure les erreurs Lean exactes
   - Montrer la preuve partielle
   - Demander des corrections specifiques

5. **Exemples similaires**
   - Donner des preuves similaires reussies
   - Montrer le style attendu
   - Few-shot learning ameliore les résultats

Exercice 1 : Conception de prompts pour preuves Lean

Difficulte : Debutant | Duree estimée : 10 minutes

Vous avez vu les différents templates de prompts et les bonnes pratiques. Construisez maintenant votre propre prompt structure pour faire prouver un théorème sur les listes par un LLM.

Competences visees : - Structurer un prompt efficace pour le theorem proving - Appliquer le few-shot learning avec des exemples pertinents - Comparer différentes stratégies de prompting

# === EXERCICE 1 : Conception de prompts pour preuves Lean ===
#
# Objectif : Creer un prompt structure pour faire prouver un théorème par un LLM.
#
# Contexte : Vous devez prouver le théorème suivant en Lean 4 :
#   theorem list_reverse_reverse (l : List Nat) : l.reverse.reverse = l
#
# Instructions :
# 1. Construire un prompt en utilisant le template "expert" du dictionnaire PROMPTS
#    (defini plus haut). Remplir les champs {theorem} avec le théorème ci-dessus.
#
# 2. Ameliorer le prompt en ajoutant 2 exemples few-shot de preuves sur les listes :
#    - theorem list_nil_append (l : List Nat) : [] ++ l = l := by simp
#    - theorem list_length_nil : ([] : List Nat).length = 0 := by rfl
#
# 3. Stocker votre prompt final dans la variable `my_prompt` (type str)
#
# 4. (Bonus) Utiliser LeanProofPrompt.build_initial_prompt() et comparer
#    avec votre version manuelle. Lequel est plus complet ?
#
# Indices :
# - Les templates sont dans le dictionnaire PROMPTS (cles: basic, with_context, iterative, expert)
# - str.format() ou f-strings pour remplir les placeholders
# - Un bon prompt inclut : version Lean, imports, exemples, contraintes

# TODO: Votre code ici
pass  # TODO: completez cet exercice
print("Exercice 1: Conception de prompts - a completer")
Exercice 1: Conception de prompts - a completer

Exercice 2 : Analyseur d’erreurs Lean

Les erreurs retournees par Lean sont variées : erreurs de type, erreurs de syntaxe, identificateur inconnu, tactique echouee, etc. Un bon système LLM+Lean doit pouvoir classer automatiquement ces erreurs pour adapter la stratégie de correction.

Objectif : Implementer classify_lean_error(error_message: str) -> str qui retourne la catégorie de l’erreur parmi : "syntax", "type_error", "unknown_identifier", "tactic_failed", ou "unknown".

Étapes : 1. Chercher les mots-cles caractéristiques dans le message d’erreur 2. Retourner la catégorie correspondante 3. Si aucun pattern reconnu, retourner "unknown"

Indice : Les erreurs Lean courantes contiennent : "syntax error", "type mismatch", "unknown identifier", "tactic failed", "unsolved goals".

# ============================================================
# Exercice 2 : Analyseur d'erreurs Lean
# ============================================================
# Classer automatiquement les erreurs Lean par categorie.
# ============================================================

def classify_lean_error(error_message: str) -> str:
    """
    Classifie un message d'erreur Lean dans une categorie.

    Categories possibles :
    - "syntax" : erreur de syntaxe
    - "type_error" : erreur de typage
    - "unknown_identifier" : identificateur non defini
    - "tactic_failed" : tactique qui a echoue
    - "unknown" : categorie non reconnue

    Args:
        error_message: Message d'erreur brut de Lean

    Returns:
        La categorie de l'erreur
    """
    error_lower = error_message.lower()

    # TODO: Etape 1 - Detecter les erreurs de syntaxe
    if False:  # TODO étudiant : chercher "syntax" dans error_lower
        return "syntax"

    # TODO: Etape 2 - Detecter les erreurs de type
    if False:  # TODO étudiant : chercher "type" ou "mismatch" dans error_lower
        return "type_error"

    # TODO: Etape 3 - Detecter les identificateurs inconnus
    if False:  # TODO étudiant : chercher "unknown identifier" dans error_lower
        return "unknown_identifier"

    # TODO: Etape 4 - Detecter les tactiques echouees
    if False:  # TODO étudiant : chercher "tactic" ou "unsolved" dans error_lower
        return "tactic_failed"

    return "unknown"


# Test rapide
test_errors = [
    "syntax error: unexpected token",
    "type mismatch: Nat vs Int",
    "unknown identifier 'foo'",
    "tactic 'simp' failed",
    "unsolved goals",
    "something completely different",
]
for err in test_errors:
    cat = classify_lean_error(err)
    print(f"  {cat:20s} <- {err}")
  unknown              <- syntax error: unexpected token
  unknown              <- type mismatch: Nat vs Int
  unknown              <- unknown identifier 'foo'
  unknown              <- tactic 'simp' failed
  unknown              <- unsolved goals
  unknown              <- something completely different

5. Integration Réelle avec OpenAI et Anthropic

Cette section presente l’implémentation réelle (pas de simulation) d’un système complet d’assistance a la preuve par LLM. Nous allons construire:

  1. LLMClient : Abstraction unifiee pour OpenAI et Anthropic avec retry logic
  2. LeanProofPrompt : Templates de prompts et extraction de code
  3. ProofVerifier : Integration avec lean_runner.py pour vérification formelle
  4. ProofGenerator : Boucle de feedback LLM ↔︎ Lean avec itérations
  5. Exemples progressifs : Théorèmes simples → Mathlib → complexes
  6. Visualisations : Metriques de convergence et comparaisons

Prerequis

  • Cle API OpenAI ou Anthropic configuree dans .env
  • lean_runner.py disponible (déjà present dans ce repertoire)
  • Packages : openai, anthropic, matplotlib, pandas
# Installation des dependances
pip install openai anthropic matplotlib pandas python-dotenv tenacity
# Section 6.1 - Configuration et Imports
# Les classes LLM sont maintenant dans lean_runner.py

import os
import sys
from pathlib import Path

# Trouver le repertoire du notebook (plusieurs méthodes)
def find_notebook_dir():
    """Trouve le repertoire contenant lean_runner.py"""
    # Méthode 1: Chercher lean_runner.py depuis le cwd et ses parents
    candidates = [
        Path.cwd(),  # Repertoire courant
        Path.cwd() / "MyIA.AI.Notebooks" / "SymbolicAI" / "Lean",
    ]
    
    for candidate in candidates:
        if candidate.exists() and (candidate / "lean_runner.py").exists():
            return candidate
    
    # Méthode 2: Rechercher dans les parents du cwd
    current = Path.cwd()
    for _ in range(5):  # Remonter jusqu'a 5 niveaux
        lean_path = current / "MyIA.AI.Notebooks" / "SymbolicAI" / "Lean"
        if lean_path.exists() and (lean_path / "lean_runner.py").exists():
            return lean_path
        if (current / "lean_runner.py").exists():
            return current
        current = current.parent
    
    raise FileNotFoundError("Impossible de trouver lean_runner.py - verifiez le repertoire de travail")

# Trouver et ajouter le repertoire au path
notebook_dir = find_notebook_dir()
if str(notebook_dir) not in sys.path:
    sys.path.insert(0, str(notebook_dir))
print(f"Repertoire notebook: OK (trouve)")

# Charger les variables d'environnement avec debug
from lean_runner import load_env_file
env_path = notebook_dir / ".env"
print(f"Fichier .env: {'trouve' if env_path.exists() else 'MANQUANT'}")

# Vérifier si python-dotenv est disponible
try:
    import dotenv
    print(f"python-dotenv disponible: version {dotenv.__version__ if hasattr(dotenv, '__version__') else 'unknown'}")
except ImportError:
    print("ERREUR: python-dotenv non installe - executez: pip install python-dotenv")

# Charger le fichier
env_loaded = load_env_file(env_path)
print(f"Chargement .env: {'OK' if env_loaded else 'ECHEC'}")

# Vérifier si les variables sont chargees (sans reveler les valeurs)
openai_key = os.environ.get("OPENAI_API_KEY")
anthropic_key = os.environ.get("ANTHROPIC_API_KEY")
print(f"OPENAI_API_KEY: {'presente' if openai_key else 'MANQUANTE'}")
print(f"ANTHROPIC_API_KEY: {'presente' if anthropic_key else 'MANQUANTE'}")

print(f"\nConfiguration chargee")

# Importer les classes LLM depuis lean_runner
from lean_runner import (
    LeanRunner, LeanResult,
    PROVIDERS_CONFIG,
    LLMResponse, LLMClient,
    LeanProofPrompt,
    ErrorInfo, ProofVerifier,
    ProofAttempt, ProofResult, ProofGenerator
)

print("Classes importees depuis lean_runner.py")
Repertoire notebook: OK (trouve)
Fichier .env: trouve
python-dotenv disponible: version unknown
Chargement .env: OK
OPENAI_API_KEY: presente
ANTHROPIC_API_KEY: presente

Configuration chargee
Classes importees depuis lean_runner.py

5.2 Explications : LLMClient

Le LLMClient unifie les API OpenAI et Anthropic avec plusieurs fonctionnalites cles :

Gestion des paramètres max_tokens

Les modèles OpenAI ont evolue et utilisent des paramètres différents :

Modèles Paramètre Valeur typique
gpt-5.2, gpt-5, gpt-4o max_completion_tokens 800-1000
o1, o3 max_completion_tokens 8000
gpt-4, gpt-3.5 max_tokens 500-800

Le client detecte automatiquement le bon paramètre selon le modèle.

Retry logic avec exponential backoff

En cas d’erreur API (rate limit, timeout), le client retente automatiquement avec des delais croissants : - Tentative 1 echoue → attendre 2^0 = 1s - Tentative 2 echoue → attendre 2^1 = 2s - Tentative 3 echoue → attendre 2^2 = 4s

Cette stratégie evite de surcharger l’API et maximise les chances de succes.

Metriques collectees

Chaque LLMResponse contient : - content : La reponse textuelle - model : Le modèle utilise - provider : openai ou anthropic - tokens_used : Tokens prompt/completion/total - latency_ms : Temps de reponse en millisecondes

Ces metriques permettent d’analyser les performances et couts.

# Section 6.2 - Demonstration LLMClient

# Afficher la configuration des providers
print("Providers disponibles:")
for provider, config in PROVIDERS_CONFIG.items():
    api_key = os.environ.get(config["api_key_env"])
    status = "OK" if api_key else "NON CONFIGURE"
    print(f"  - {provider}: {status} (modele defaut: {config['default_model']})")

# Initialiser le client OpenAI (si configure)
try:
    client = LLMClient(provider="openai")
    print(f"Client OpenAI initialise avec modele: {client.model}")
except ValueError as e:
    print(f"OpenAI non configure: {e}")
    client = None
Providers disponibles:
  - openai: OK (modele defaut: gpt-5.2)
  - anthropic: OK (modele defaut: claude-sonnet-4-5)
Client OpenAI initialise avec modele: gpt-5.2

6.4 Explications : Prompt Engineering pour Lean

Le prompting efficace pour Lean necessite precision et structure. Voici les patterns cles :

1. Prompt initial : Contexte riche

Un bon prompt initial inclut : - Imports disponibles : Mathlib, tactiques standard - Variables et types : (a b : Nat), (x : Real), etc. - Hypotheses : Lemmes et faits déjà etablis - Théorème cible : Formulation exacte

Exemple :

Imports disponibles: Mathlib.Algebra.Ring.Basic
Variables: (a b c : Nat)

Théorème:
theorem distrib_example (a b c : Nat) : a * (b + c) = a * b + a * c := by sorry

Utilise les tactiques Mathlib appropriees.

2. Prompt de correction : Feedback cible

Quand une preuve echoue, le prompt de correction doit : - Montrer le code qui a echoue - Inclure l’erreur Lean complète (ligne, message) - Demander une correction SPÉCIFIQUE

Itération typique : 1. LLM suggere by rfl 2. Lean repond type mismatch 3. Correction : by omega ou by ring

3. Few-shot learning : Exemples similaires

Fournir 2-3 exemples de preuves similaires ameliore drastiquement les résultats :

Exemple 1:
theorem add_comm (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b

Exemple 2:
theorem mul_comm (a b : Nat) : a * b = b * a := by
  exact Nat.mul_comm a b

Maintenant prouve:
theorem add_mul_comm (a b c : Nat) : (a + b) * c = a * c + b * c

4. Temperature et determinisme

Temperature Comportement Usage
0.0-0.3 Déterministe, predictible Preuves simples, tactiques standard
0.4-0.7 Creatif, exploratoire Preuves complexes, stratégies nouvelles
0.8-1.0 Très creatif, variable Brainstorming, exploration

Pour Lean, temperature 0.2-0.4 est optimale : assez déterministe pour eviter les erreurs syntaxiques, assez flexible pour trouver des solutions elegantes.

# Section 6.3 - Demonstration LeanProofPrompt

# Exemple de prompt initial
theorem = "theorem add_comm_example (a b : Nat) : a + b = b + a := by sorry"
prompt = LeanProofPrompt.build_initial_prompt(theorem)

print("=== Exemple de prompt initial ===")
print(prompt[:300] + "...")

# Exemple d'extraction de code Lean
llm_response = """Voici la preuve:
```lean
theorem add_comm_example (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b
```
"""

extracted = LeanProofPrompt.extract_lean_code(llm_response)
print("=== Exemple d'extraction ===")
print(f"Code extrait: {extracted}")
=== Exemple de prompt initial ===
Ecris une preuve Lean 4 pour le theoreme suivant:

Theoreme:
```lean
theorem add_comm_example (a b : Nat) : a + b = b + a := by sorry
```


Donne le code Lean complet avec la preuve (remplace 'by sorry' par les tactiques).
IMPORTANT: Mathlib n'est PAS disponible. Utilise uniquement les tactiques sta...
=== Exemple d'extraction ===
Code extrait: theorem add_comm_example (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b

6.6 Explications : Vérification avec LeanRunner

Le ProofVerifier integre lean_runner.py, notre backend production-ready pour exécuter Lean depuis Python.

Backends disponibles

LeanRunner supporte 3 backends :

Backend Plateforme Avantages Utilisation
subprocess Tous Simple, rapide Default, théorèmes simples
wsl Windows REPL complet, kernel Jupyter Théorèmes interactifs
leandojo Python <3.13 ML/LLM, extraction théorèmes Recherche, training

Le mode backend="auto" selectionne automatiquement le meilleur backend disponible.

Parsing d’erreurs Lean

Les erreurs Lean suivent un format structure :

Main.lean:10:5: error: unknown identifier 'Nat.add_com'
                       ^
Main.lean:12:0: warning: unused variable `h`

Le parser extrait : - Fichier : Main.lean - Ligne : 10 - Colonne : 5 - Severite : error ou warning - Message : Description de l’erreur

Cette information permet au LLM de corriger précisément l’erreur.

Types d’erreurs courants

Type Message typique Correction LLM
Syntaxe unexpected token Fixer la syntaxe
Type type mismatch: expected Nat, got Int Convertir ou changer type
Tactique tactic 'rfl' failed Essayer autre tactique
Inconnu unknown identifier 'Nat.add_com' Corriger typo (add_comm)
Timeout timeout Simplifier ou changer stratégie 
# Section 6.4 - Demonstration ProofVerifier

# Initialiser le verificateur
verifier = ProofVerifier(backend="auto", timeout=30)

# Test avec un théorème simple
print("=== Test de verification ===")
test_code = """theorem test_verification (n : Nat) : n + 0 = n := by
  rfl
"""
print(f"Code a verifier: {test_code}")

result = verifier.verify(test_code)
print(f"Resultat: {'SUCCES' if result.success else 'ECHEC'}")
print(f"Backend: {result.backend}")
LeanRunner initialise (backend: subprocess)
=== Test de verification ===
Code a verifier: theorem test_verification (n : Nat) : n + 0 = n := by
  rfl

Resultat: SUCCES
Backend: subprocess

6.8 Explications : Feedback Loop LLM ↔︎ Lean

Le ProofGenerator orchestre la boucle complète de generation iterative. C’est le coeur du système.

Architecture du feedback loop

+---------------------------------------------------------------+
|                    Feedback Loop LLM ↔ Lean                   |
+---------------------------------------------------------------+
|                                                               |
|  Théorème → LLM (prompt initial) → Code Lean → LeanRunner    |
|                 ↑                                    ↓        |
|                 |                              Vérification   |
|                 |                                    ↓        |
|                 |                              Succes/Echec   |
|                 |                                    ↓        |
|                 └─── Correction (prompt + erreur) ←─┘        |
|                      (itérations 2-N)                         |
|                                                               |
+---------------------------------------------------------------+

Flux detaille

Étape Action Sortie
1 LLM genere preuve initiale Code Lean (tentative 1)
2 LeanRunner vérifie Succes → FIN / Echec → continuer
3 Parser erreur Lean ErrorInfo (ligne, message)
4 Construire prompt correction Prompt avec erreur detaillee
5 LLM corrige Code Lean (tentative 2)
6 Retour étape 2 Jusqu’a succes ou max_iterations

Metriques collectees

A chaque itération, on enregistre : - Code genere : Tentative de preuve - Résultat Lean : Succes/erreur - Reponse LLM : Tokens, latence - Timestamp : Pour analyse temporelle

Le ProofResult final contient : - Succes : Vrai/faux - Preuve finale : Code Lean valide (si succes) - Historique : Toutes les tentatives - Metriques : Tokens totaux, temps total, itérations

Stratégies d’optimisation

  1. Temperature adaptative : Basse (0.2-0.3) pour théorèmes simples, plus haute (0.4-0.6) pour complexes
  2. Few-shot si echec : Après 2-3 echecs, ajouter des exemples similaires
  3. Timeout progressif : Augmenter le timeout Lean pour théorèmes difficiles
  4. Multi-provider : Essayer Anthropic si OpenAI echoue (et vice-versa)
# Section 6.5 - ProofGenerator pret a l'emploi

# Le ProofGenerator est importe depuis lean_runner
print("ProofGenerator pret.")
print("Usage: generator = ProofGenerator(llm_client=client, verifier=verifier)")
ProofGenerator pret.
Usage: generator = ProofGenerator(llm_client=client, verifier=verifier)

6.9 Test du Pipeline Complet

Maintenant que tous les composants sont en place, testons le pipeline avec un théorème simple. Ce test valide l’integration complète : appel LLM, extraction de preuve, vérification Lean.

# Section 6.9 - Test : Théorème Simple

# Test complet du système avec un théorème simple
print("=== TEST SYSTEME COMPLET ===\n")

# Théorème de test (commutativite de l'addition)
test_theorem = "theorem test_add_comm (a b : Nat) : a + b = b + a := by sorry"

# Vérifier si une API est configuree
try:
    # Essayer d'initialiser le client
    llm = LLMClient(provider="openai")
    api_available = True
    print(f"API {llm.provider} disponible (modele: {llm.model})")
except ValueError:
    # Pas d'API configuree
    api_available = False
    print("[INFO] Aucune API LLM configuree")
    print("Pour tester avec une vraie API :")
    print("  1. Copier .env.example vers .env")
    print("  2. Ajouter votre OPENAI_API_KEY ou ANTHROPIC_API_KEY")
    print("  3. Relancer cette cellule\n")

if api_available:
    # Test réel avec API
    print(f"\nTest avec API reelle...")
    print(f"Theoreme: {test_theorem}\n")
    
    # Creer le generateur
    generator = ProofGenerator(
        llm_client=llm,
        verifier=verifier,
        max_iterations=3,
        temperature=0.3
    )
    
    # Tenter la preuve
    result = generator.prove(test_theorem, verbose=True)
    
    # Afficher le résultat
    print(f"\n{'='*60}")
    print(f"RESULTAT FINAL")
    print(f"{'='*60}")
    print(f"Succes: {result.success}")
    print(f"Iterations: {result.total_iterations}")
    print(f"Temps total: {result.total_time_ms:.0f}ms")
    
    if result.success:
        print(f"\nPreuve finale:")
        print(result.final_proof)
    
    # Metriques
    metrics = result.get_metrics()
    print(f"\nMetriques:")
    print(f"  - Tokens totaux: {metrics['total_tokens']}")
    print(f"  - Latence moyenne LLM: {metrics['avg_llm_latency_ms']:.0f}ms")
    print(f"  - Provider: {metrics['provider']} / {metrics['model']}")
else:
    # Test en mode simulation
    print("\n[MODE SIMULATION]")
    print("Le systeme est fonctionnel mais utilise des simulations.")
    print("Configurez une API pour tester reellement.")
=== TEST SYSTEME COMPLET ===

API openai disponible (modele: gpt-5.2)

Test avec API reelle...
Theoreme: theorem test_add_comm (a b : Nat) : a + b = b + a := by sorry


============================================================
TENTATIVE DE PREUVE
============================================================
Theoreme: theorem test_add_comm (a b : Nat) : a + b = b + a := by sorry...
Provider: openai / gpt-5.2
Max iterations: 3
============================================================

--- Iteration 1/3 ---
Generation initiale...
LLM genere (4142ms, 380 tokens)
Code:
theorem test_add_comm (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b...

[SUCCES] Preuve verifiee en 1 iteration(s)!
Temps total: 5213ms

============================================================
RESULTAT FINAL
============================================================
Succes: True
Iterations: 1
Temps total: 5213ms

Preuve finale:
theorem test_add_comm (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b

Metriques:
  - Tokens totaux: 380
  - Latence moyenne LLM: 4142ms
  - Provider: openai / gpt-5.2

6.10 Conclusion : Section 6 Complète

La Section 6 est maintenant complète avec une implémentation réelle du feedback loop LLM ↔︎ Lean.

Ce qui a ete implemente

Composant Description Status
LLMClient API OpenAI/Anthropic unifiee avec retry logic COMPLET
LeanProofPrompt Templates prompts (initial, correction, few-shot) COMPLET
ProofVerifier Integration lean_runner.py, parsing erreurs COMPLET
ProofGenerator Boucle feedback complète avec metriques COMPLET
Test simple Vérification système end-to-end COMPLET

Prochaines étapes (Phase 2)

La Phase 2 (section suivante ou notebook separe) ajoutera :

  1. SIMPLE_THEOREMS : Exemples add_zero, add_comm, mul_assoc (1-2 itérations attendues)
  2. MATHLIB_THEOREMS : Exemples ring, linarith, omega (2-4 itérations attendues)
  3. Visualisations : Graphes convergence, temps, tokens, taux succes
  4. Comparaisons providers : OpenAI vs Anthropic sur mêmes théorèmes
  5. Few-shot learning : Impact d’exemples sur taux succes
  6. Théorèmes complexes : Induction, recursion (5+ itérations)

Utilisation immediate

Vous pouvez maintenant :

# 1. Configurer votre .env avec OPENAI_API_KEY ou ANTHROPIC_API_KEY

# 2. Créer client et générateur
llm = LLMClient(provider="openai")  # ou "anthropic"
generator = ProofGenerator(llm, verifier, max_iterations=5)

# 3. Prouver un théorème
result = generator.prove("theorem test (n : Nat) : n + 0 = n := by sorry")

# 4. Analyser les metriques
metrics = result.get_metrics()
print(f"Succes: {result.success}, Itérations: {metrics['itérations']}")

Ressources

  • lean_runner.py : Backend robuste avec 3 backends (subprocess, wsl, leandojo)
  • .env.example : Template de configuration
  • examples/llm_assisted_proof.lean : Exemples de preuves pour few-shot

Section 6 terminee - Implémentation réelle fonctionnelle avec API OpenAI/Anthropic !

Exercice 3 : Pipeline de preuve automatique

Difficulte : Intermediaire | Duree estimée : 15 minutes

Vous avez vu le pipeline complet LLM -> Lean -> feedback. Utilisez maintenant le ProofGenerator pour prouver un théorème plus complexe et analysez les metriques de convergence (itérations, tokens, temps).

Competences visees : - Utiliser le ProofGenerator avec des paramètres adaptes - Analyser les metriques de convergence - Comprendre l’impact de la temperature sur la qualite des preuves

# === EXERCICE 3 : Pipeline de preuve automatique ===
# 
# Objectif : Utiliser le ProofGenerator pour prouver un théorème plus complexe
# et analyser les metriques de convergence.
#
# Instructions :
# 1. Choisir UN théorème parmi les suivants (difficulte croissante) :
#    a) "theorem ex_mul_zero (n : Nat) : n * 0 = 0 := by sorry"
#    b) "theorem ex_add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by sorry"
#    c) "theorem ex_mul_distrib (a b c : Nat) : a * (b + c) = a * b + a * c := by sorry"
#
# 2. Creer un ProofGenerator avec max_iterations=5 et temperature=0.3
#
# 3. Lancer la preuve avec verbose=True
#
# 4. Afficher les metriques : nombre d'iterations, tokens totaux, temps total
#
# 5. (Bonus) Comparer avec temperature=0.7 : plus ou moins d'iterations ?
#
# Indices :
# - Le ProofGenerator est deja importe depuis lean_runner
# - Utiliser le client LLM initialise plus haut (variable `client`)
# - Le verifier est aussi deja initialise (variable `verifier`)
# - result.get_metrics() retourne un dictionnaire avec toutes les metriques

# TODO: Votre code ici
pass  # TODO: completez cet exercice
print("Exercice 3: Pipeline de preuve - a completer")
Exercice 3: Pipeline de preuve - a completer

Navigation : ← Lean-06-Mathlib-Essentials-Lean | Index | Lean-08-Agentic-Proving-Python →

Retour au sommet