Cet article présente une nouvelle méthode permettant de récupérer efficacement des prémisses, une étape importante du processus de formalisation des mathématiques. Les méthodes de récupération existantes basées sur le langage naturel requièrent une expertise mathématique de la part des utilisateurs, tandis que les méthodes basées sur le langage formel (par exemple, Lean) présentent des performances médiocres en raison de données d'apprentissage insuffisantes. Dans cette étude, nous avons entraîné un modèle de récupération de prémisses léger mais efficace à partir de données extraites de Mathlib. Plus précisément, nous avons utilisé un tokeniseur spécialisé pour les corpus de langage formel afin d'intégrer les requêtes (états de preuve fournis par Lean) et les prémisses dans l'espace latent, et appliqué une méthode de calcul de similarité fine et un module de reclassement pour améliorer les performances. Les résultats expérimentaux montrent que le modèle proposé atteint une précision supérieure et un coût de calcul inférieur à celui des méthodes existantes. Le moteur de recherche développé est disponible en open source.
