Projet dédié à l'automatisation et à l'assistance de la vérification de preuves mathématiques formelles à l'aide d'agents IA. Il propose des outils pour écrire, vérifier et corriger des preuves dans le langage Lambdapi, ainsi qu'un environnement de benchmarking pour évaluer les performances des agents. Le projet explore également différentes approches d'interaction entre agents et outils de preuve.

Projet de recherche en informatique théorique axé sur la vérification formelle de preuves mathématiques et le développement de tactiques dépendantes dans le langage Meta Dedukti. Il permet d'assurer la correction et la fiabilité des démonstrations logiques et mathématiques à l'aide de méthodes formelles avancées.