OpenProver

Ce qu'il fait

OpenProver est un prouveur de théorèmes automatisé qui utilise des modèles de langage étendus pour découvrir et vérifier des preuves mathématiques. Il emploie une architecture sophistiquée planificateur-travailleur où un planificateur central gère un tableau blanc et un répertoire de lemmes, déléguant des tâches d'exploration spécifiques à des travailleurs parallèles. Cela lui permet de s'attaquer à des énoncés mathématiques complexes en les décomposant en morceaux gérables.

Outils

• lean_verify : Compile le code Lean 4 pour vérifier l'exactitude.
• lean_store : Conserve les extraits mathématiques vérifiés pour une réutilisation future.
• lean_search : Recherche dans Mathlib et les déclarations Lean pour trouver des théorèmes pertinents.
• literature_search : Effectue des recherches sur le web pour trouver des articles et des résultats mathématiques existants.

Installation

Pour utiliser OpenProver via Claude Desktop, ajoutez ce qui suit à votre fichier claude_desktop_config.json :

{
  "mcpServers": {
    "openprover": {
      "command": "openprover",
      "args": []
    }
  }
}

Note : Nécessite Python 3.10+ et pip install openprover.

Hôtes supportés

• Claude
• vLLM
• OpenRouter