Metamath
Langage formel et assistant de preuve associé / De Wikipedia, l'encyclopédie encyclopedia
Cher Wikiwand IA, Faisons court en répondant simplement à ces questions clés :
Pouvez-vous énumérer les principaux faits et statistiques sur Metamath?
Résumez cet article pour un enfant de 10 ans
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[2]. 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[3].
Créateur | Norm Megill |
---|---|
Dernière version | 0.198 ()[1] |
Dépôt | Metamath sur GitHub |
État du projet | En développement actif |
Écrit en | ANSI C |
Environnement | Linux, Windows, macOSes |
Langues | Anglais |
Type | Assistant de preuve |
Politique de distribution | Gratuit et open source |
Licence | GNU General Public License (Creative Commons Domaine public pour les bases) |
Documentation | us.metamath.org/downloads/metamath.pdf |
Site web | metamath.org |
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[4].
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[5].