Ce projet est une implémentation de la théorie des ensembles dans Dedukti, utilisant une version intuitionniste de la théorie des ensembles où les ensembles sont représentés par des graphes pointés. Il contient plusieurs fichiers de code organisés en fonctionnalités, notamment la logique, les nombres naturels, la théorie des graphes pointés, la théorie des formules, l'extension de la langue, la preuve de la théorie des ensembles et des lemmes associés.

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.

Pari-gp-binder est une configuration Binder dédiée à l'utilisation du logiciel PARI/GP dans un environnement Jupyter. Il facilite le calcul numérique et la théorie des nombres en offrant un environnement dédié et personnalisé, directement accessible via un navigateur web.

GMP-ECM est un outil spécialisé dans la factorisation de grands nombres entiers en utilisant des algorithmes avancés comme ECM (Elliptic Curve Method), P-1 et P+1. Il est largement utilisé en cryptographie, en théorie des nombres et pour la vérification de la primalité de grands nombres. Le projet permet d'optimiser les calculs en ajustant des paramètres comme les bornes B1 et B2 pour maximiser l'efficacité.

Ce projet développe une bibliothèque Rocq qui traduit automatiquement une partie de la bibliothèque HOL-Light, notamment la définition des nombres réels et des fonctions associées, vers des types et fonctions compatibles avec MathComp. L'objectif est de permettre l'utilisation de théorèmes HOL-Light dans des développements Rocq, facilitant ainsi l'interopérabilité entre ces environnements de preuve formelle. Les preuves traduites sont fournies comme axiomes pour une intégration rapide, tout en restant vérifiables via un script dédié.

Ce projet fournit une traduction en Coq de la définition des nombres réels dans HOL-Light, en utilisant le type nat de Coq. Il permet de formaliser des concepts mathématiques avancés et de vérifier des preuves automatiquement. La bibliothèque est générée à partir de HOL-Light et peut être utilisée pour des développements formels en mathématiques ou en informatique théorique.

Ce projet développe des outils pour concevoir et évaluer des circuits quantiques optimisés, réduisant le nombre de qubits nécessaires pour des algorithmes spécifiques. Il permet de tester et comparer des implémentations quantiques, notamment pour des opérations comme l'inversion de matrices ou la multiplication de polynômes binaires. Les résultats sont utilisés pour valider des formules théoriques et améliorer l'efficacité des algorithmes quantiques dans le domaine du décodage d'information.