MathCode : un agent de codage mathématique avec formalisation Lean 4

MathCode est un assistant IA de codage en terminal qui formalise et prouve des problèmes mathématiques en utilisant Lean 4. Au lieu d'écrire du code Lean vous-même, vous lui donnez un problème en anglais simple, et il génère un théorème et tente une preuve, avec un REPL persistant et une bibliothèque de théorèmes réutilisables.

Fonctionnalités clés

• REPL Lean persistant : Après un échauffement unique, les vérifications de compilation passent à ~0,4 s (au lieu de ~30 s).
• Bibliothèque de théorèmes : Chaque théorème prouvé est automatiquement nommé, stocké et importable pour réutilisation.
• Bibliothèque d'axiomes : Stockez les hypothèses de conversation comme des déclarations Lean persistantes et vérifiées à la compilation.
• Intégration LSP Lean : Recherche sur leansearch.net et Loogle pour des lemmes Mathlib vérifiés, utilise des diagnostics LSP structurés pour les réparations.
• Graphe de théorèmes Obsidian : Génère un graphe de dépendances visuel des théorèmes et lemmes dans Obsidian.
• Preuve en mode agent : Sessions interactives où l'agent itère sur des candidats de preuve en fonction des erreurs.
• Arbre de sous-objectifs : Décompose les théorèmes complexes en sous-objectifs indépendants, les prouve en parallèle, puis les assemble.
• Multi-planificateur : Exécute plusieurs planificateurs en parallèle pour diverses stratégies de preuve ; le prouveur choisit la meilleure approche.

Démarrage rapide

Nécessite macOS (arm64) ou Linux (x86_64), ainsi que l'interface CLI codex pour le backend par défaut.

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login

Essayez avec :

mathcode -p "prouver que le carré d'un nombre pair est pair"

Les sorties sont écrites dans LeanFormalizations/. Une interface navigateur est disponible via ./run webui.

Cet outil est destiné aux mathématiciens, chercheurs et développeurs travaillant avec la vérification formelle ou la preuve de théorèmes assistée par IA.