Dépôt de code source contenant des définitions de logiques formelles, y compris la logique polymorphe du premier ordre (TFF), la théorie U introduite dans Axioms for Mathematics, et des fichiers de logique utilisés par l'assistant de preuve automatisé ZenonModulo. Il contient également une implémentation de l'embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.

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.

Ce projet propose des ressources pédagogiques pour les cours de preuves assistées par ordinateur et de preuve formelle. Il s'adresse principalement aux étudiants en informatique de niveau master, notamment ceux suivant les cours du M1 Informatique ou du M2 LMFI à Paris Diderot. Les documents couvrent des concepts théoriques et pratiques liés à la vérification et à la formalisation des preuves en informatique.

Le projet B-in-Dedukti vise à implémenter la théorie mathématique du langage de spécification formelle B dans l'assistant de preuve Dedukti. Cela permet de traduire des preuves de correctitude formelles réalisées dans l'assistant de preuve Atelier B vers Dedukti, facilitant ainsi l'interopérabilité entre différents outils de preuve formelle.

Le projet math-comp est une bibliothèque de théories mathématiques formalisées, basée sur l'assistant de preuve Coq et le langage Coq/SSReflect. Il couvre un large éventail de sujets, des structures de données de base telles que les listes, les nombres premiers et les graphes fins, à des sujets avancés en algèbre. La bibliothèque a été utilisée dans des preuves formelles de théorèmes importants tels que le théorème des quatre couleurs et le théorème de l'ordre impair.

Ce projet est la bibliothèque standard du Rocq Prover, un assistant de preuve interactif. Il propose un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, accompagnés d'un environnement pour développer des preuves vérifiées par machine. La bibliothèque standardise et organise les modules essentiels pour les utilisateurs et développeurs, favorisant ainsi la rigueur et la réutilisabilité dans les travaux de preuve formelle.

Coq est un assistant de preuve interactif qui permet la vérification formelle de preuves mathématiques et la spécification et vérification de systèmes informatiques. Il utilise un langage de programmation dédié, le Gallina, pour écrire des preuves et des spécifications.

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.

Rocq-prover.org est une plateforme en ligne dédiée au langage Rocq, un assistant de preuve formelle. Elle centralise la documentation technique, les paquets logiciels et les ressources pédagogiques pour faciliter l'apprentissage et le développement avec Rocq. Le site propose une interface moderne et accessible, adaptée aux besoins des chercheurs, développeurs et étudiants en informatique théorique.

HOL Light est un assistant de preuve interactif écrit en Objective CAML, permettant la vérification formelle de preuves mathématiques et le développement de théories mathématiques formelles.