LeanCopilot : faire tourner un LLM dans le tacticiel Lean

Le problème : l'assistant de preuve ignore le contexte local du fichier

Lean sait vérifier une preuve, pas la proposer. Quand une étape vous résiste, vous quittez le fichier pour chercher un lemme dans mathlib4, vous revenez, vous essayez, vous échouez. LeanCopilot vise ce va-et-vient : le README annonce que les modèles de langage servent nativement dans Lean pour l'automatisation des preuves, avec des tactiques qui suggèrent des tactiques, cherchent des preuves et sélectionnent des prémisses. Le public visé est précis : quelqu'un qui écrit déjà des preuves Lean 4 et qui veut un appel de modèle au clavier, pas une interface séparée. Les trois tactiques exposées couvrent trois moments distincts du travail. suggest_tactics intervient quand vous savez à peu près quoi faire mais pas comment l'écrire. search_proof intervient quand vous acceptez de laisser chercher plusieurs étapes. select_premises intervient quand le problème est de trouver le bon lemme, pas la bonne syntaxe.

Ce qui tourne réellement sous la syntaxe Lean

Le paquet est écrit en C++ et s'appuie sur CTranslate2, ce que trahit l'option d'édition de liens demandée dans le lakefile : -lctranslate2. Les modèles livrés sont des conversions au format CTranslate2 d'un encodeur-décodeur de taille modeste, à en juger par les noms des dépôts Hugging Face listés dans le README : ct2-leandojo-lean4-tacgen-byt5-small pour la génération de tactiques, ct2-leandojo-lean4-retriever-byt5-small pour le retriever, premise-embeddings-leandojo-lean4-retriever-byt5-small pour les plongements de prémisses, plus ct2-byt5-small. L'inférence peut tourner localement, avec ou sans GPU, ou à distance. search_proof n'est pas un modèle qui produit une preuve complète d'un coup : le README précise qu'il combine des tactiques générées par le LLM avec aesop pour chercher des preuves multi-étapes. C'est un assemblage, et cela explique pourquoi la qualité dépend autant du modèle que de la tactique aesop sous-jacente. select_premises, lui, interroge le retriever de LeanDojo sur un snapshot figé de Lean et de mathlib4. Le README ne décrit pas de réindexation de votre projet, donc la sélection porte sur cet instantané et non sur les déclarations que vous venez d'écrire.

Installation : quatre commandes et une version à épingler

Tout passe par Lake. Il faut d'abord éditer le lakefile pour que l'éditeur de liens trouve la bibliothèque du paquet : moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"] dans lakefile.lean, ou la clé équivalente moreLinkArgs en tableau TOML si votre projet utilise lakefile.toml. Ensuite vient la dépendance, avec une révision explicite : require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION". Le README donne la règle de choix : pour une version stable de Lean, par exemple v4.33.0, on épingle cette version ; pour les versions instables récentes, par exemple v4.34.0-rc1, on met main. Il ajoute une mise en garde qui compte plus que le reste : dans les deux cas, assurez-vous que la version est compatible avec les autres dépendances comme mathlib. Sur Windows natif, une étape supplémentaire consiste à ajouter le chemin .lake/packages/LeanCopilot/.lake/build/lib à la variable Path. Puis lake update LeanCopilot, lake exe LeanCopilot/download pour récupérer les modèles dans ~/.cache/lean_copilot/, et lake build. Le téléchargement peut aussi se faire à la main depuis les quatre dépôts Hugging Face cités plus haut. Le projet exige Git LFS, et votre projet doit utiliser Lean au moins en version lean4:v4.3.0-rc2.

La compilation depuis les sources, un chemin de secours qui coûte cher

Un paquet en aval ne compile normalement pas LeanCopilot : il télécharge une release précompilée. Le README décrit une exception, et elle est instructive. Sur une plateforme pour laquelle aucune release n'est publiée, il cite Intel macOS, la compilation depuis les sources se déclenche automatiquement. Il faut alors CMake en version 3.7 ou supérieure et un compilateur compatible C++17. Autrement dit, la facilité d'installation dépend d'une matrice de publication que le README ne détaille pas. Si vous êtes sur une plateforme couverte, vous ne verrez jamais ces dépendances. Sinon, vous héritez d'une chaîne C++ complète pour un paquet dont vous vouliez seulement les tactiques. C'est un point à vérifier avant de promettre à une équipe que l'ajout se limite à quelques lignes de lakefile. Les scripts scripts/build.sh, scripts/build_example.sh et le Dockerfile sont mentionnés comme recours en cas d'échec de compilation, ce qui suggère que le chemin depuis les sources est suffisamment fréquenté pour mériter des outils dédiés.

Les limites que le README assume lui-même

La section Caveats existe, et c'est déjà un signal : l'auteur ne présente pas l'outil comme sans friction. La contrainte la plus lourde est la correspondance de versions. Lean évolue vite, LeanCopilot publie des releases qui suivent ces versions, et un décalage avec mathlib casse la compilation. La règle du README, à savoir main pour les versions instables, place votre projet sur une branche mouvante : vous acceptez de suivre les changements du paquet en même temps que ceux de Lean. Ensuite, select_premises travaille sur un snapshot figé de Lean et de mathlib4. Sur un projet qui définit ses propres lemmes, la sélection ne peut pas les proposer tant que ce snapshot n'est pas mis à jour par les mainteneurs. Enfin, search_proof dépend d'aesop : quand la recherche échoue, il n'est pas évident de savoir si la faute revient au modèle de génération de tactiques ou à la tactique de recherche. Le README ne fournit pas d'outil de diagnostic pour trancher, et les modèles livrés sont des modèles de taille réduite, ce qui limite la portée des preuves qu'on peut raisonnablement attendre.

Copilot face à un serveur d'inférence séparé

L'approche opposée consiste à faire tourner un serveur d'inférence à part et à l'appeler depuis Lean par HTTP. Vous gardez alors le choix du modèle, vous pouvez mettre à jour les poids sans toucher au lakefile, et vous ne dépendez d'aucune release liée à une version de Lean. En échange, vous écrivez et maintenez la couche d'appel, le format des requêtes et la gestion des erreurs, et vous perdez l'intégration directe dans le tacticiel. LeanCopilot fait le pari inverse : le pont est fourni, les modèles sont téléchargés par lake exe LeanCopilot/download, et l'appel se fait depuis une tactique. Le coût de ce confort est visible dans le lakefile : une option d'édition de liens vers CTranslate2 et une révision épinglée. Le README prévoit d'ailleurs l'usage de modèles externes, locaux ou distants, donc la frontière n'est pas étanche. La vraie différence est le point de couplage : ici, c'est le système de build de Lean qui porte la dépendance ; là, c'est votre code.

Coût de maintenance et licence

Le rythme des releases est élevé : v4.31.0 en juin 2026, puis v4.32.0 et v4.33.0 en août 2026. Un projet qui épingle une version stable devra donc remonter régulièrement pour rester aligné avec mathlib. Le dépôt n'est pas archivé, ce qui indique une maintenance active au moment de la rédaction. La licence est MIT, ce qui autorise l'usage, la modification et la redistribution avec conservation de l'avis de licence. Deux réserves, sans conseil juridique : les modèles sont hébergés sur Hugging Face sous les identifiants kaiyuy/..., et leur régime de licence n'est pas décrit dans le README ; il faut le vérifier séparément si vous les redistribuez. Par ailleurs, la licence MIT couvre le code du paquet, pas les données d'entraînement des modèles ni les conditions d'utilisation de mathlib4.

Conclusion éditoriale

LeanCopilot convient aux projets Lean 4 déjà alignés sur une version stable publiée (par exemple v4.33.0) et à ceux qui veulent des suggestions de tactiques sans quitter l'éditeur. Il ne convient pas si votre projet suit une version de Lean non couverte par une release, si vous travaillez sur Intel macOS, ou si vous attendez de select_premises qu'il voie vos déclarations locales : la documentation indique explicitement un snapshot figé de Lean et de mathlib4. Avant d'adopter, vérifiez la correspondance entre LEAN_COPILOT_VERSION et la version de Lean de votre lakefile, puis lancez lake exe LeanCopilot/download et confirmez que les modèles sont bien dans ~/.cache/lean_copilot/.

Sources officielles

1. lean-dojo/LeanCopilot on GitHub
2. License: MIT
3. Project website
4. README
5. Releases