Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Metamath
Résumé
Metamath est un langage formel et un logiciel associé (un assistant de preuve) pour rassembler, vérifier et étudier les preuves de théorèmes mathématiques. Plusieurs bases de théorèmes avec leurs preuves ont été développés avec Metamath. Elles rassemblent des résultats standards en logique, théorie des ensembles, théorie des nombres, algèbre, topologie, analyse, entre autres domaines.
Début 2022, les théorèmes prouvées à l'aide de Metamath forment l'un des plus grands corps de mathématiques formalisées, et incluent notamment 74 des 100 théorèmes du défi "Formalizing 100 Theorems", ce qui en fait le quatrième après HOL Light et Isabelle et Coq, mais devant , Mizar, Proof Power, Lean, Nqthm, ACL2, et Nuprl. Il y a au moins 17 vérificateurs de preuves pour les bases de théorèmes au format Metamath.
Ce projet est le premier de son genre qui permet la navigation interactive d'une base de théorèmes formalisés sous la forme d'un site web.
Le langage Metamath est un metalanguage, adapté au développement d'une grande variété de systèmes formels. Le langage Metamath n'a pas de logique prédéfinie intégrée. Au lieu de cela, il peut être considéré simplement comme un moyen de prouver que les règles d'inférence (définies comme axiomes ou démontrées) peuvent être appliquées. La plus grande base de preuves concernent la logique classique et les théorèmes de la théorie des ensembles ZFC, mais il existe d'autres bases de données et d'autres peuvent être créés.
La conception du langage Metamath se concentre sur la simplicité. Le langage, utilisé pour déclarer les définitions, axiomes, règles d'inférence et théorèmes ne se compose que d'une poignée de mots-clés, et toutes les preuves sont vérifiées à l'aide d'un algorithme simple basé sur les substitutions de variables (avec des contraintes possibles sur la liste des variables qui doivent rester distinctes après substitution).
L'ensemble des symboles qui peuvent être utilisés pour construire des formules est déclaré en utilisant v (déclaration de variable) déclarations.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.