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.

Bibliothèque dédiée à l'intégration de l'outil ZenonModulo avec Lambdapi pour générer des preuves formelles en logique. Elle facilite l'automatisation des démonstrations mathématiques et la vérification de théorèmes dans un cadre formel, en s'appuyant sur des outils de preuve automatisée existants.

Projet dédié à l'optimisation des transferts de fichiers et des tactiques de preuve pour Meta Dedukti, un outil de vérification formelle. Il facilite la manipulation et l'échange de preuves mathématiques formalisées en utilisant des méthodes efficaces et automatisées.

GeoCoqInE-Euclid est un projet de démonstration de théorèmes géométriques automatisée, utilisant le langage de programmation fonctionnelle Coq et la bibliothèque Euclid. Il permet le développement et la vérification de preuves formelles, ainsi que le travail collaboratif sur des théories mathématiques.

Bibliothèque de tactiques pour l'assistant de preuve Coq, dédiée à la simplification des preuves d'inégalités sur des expressions de nombres réels. Elle permet d'automatiser le calcul d'encadrements précis pour des fonctions mathématiques complexes, facilitant ainsi la vérification formelle de propriétés analytiques dans les preuves assistées par ordinateur.

Ce projet propose une bibliothèque Rocq (anciennement Coq) qui traduit automatiquement la bibliothèque HOL-Light dédiée à la logique. Il permet d'utiliser des théorèmes et outils de HOL-Light dans l'écosystème Rocq, facilitant ainsi la vérification formelle et l'automatisation de preuves mathématiques. La traduction couvre des concepts comme la logique propositionnelle, la résolution, les modèles canoniques et les algorithmes de réécriture.

Ltac2 est un langage de programmation utilisé pour l'automatisation de preuves formelles dans le domaine des mathématiques et de l'informatique. Il permet de simplifier et d'automatiser des raisonnements complexes, contribuant ainsi à améliorer la fiabilité et la vérifiabilité des démonstrations.

Ce projet propose une bibliothèque Rocq qui automatise la traduction des bibliothèques HOL-Light vers Rocq, permettant d'utiliser des théorèmes et fonctions mathématiques dans Rocq. Il facilite l'interopérabilité entre ces deux systèmes de preuve formelle en alignant types et fonctions, et offre un accès à plus de 20 000 théorèmes couvrant des domaines variés comme l'arithmétique, l'algèbre, l'analyse ou la topologie. Les preuves traduites sont fournies sous forme d'axiomes pour une utilisation rapide, avec la possibilité de régénérer et vérifier les preuves originales si nécessaire.