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[3].
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[4].
Le langage Metamath
Le langage Metamath est un métalangage, 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[5]).
Syntaxe
Le langage admet trois types de lexèmes, séparés par des espaces : les mots-clefs, les labels et les symboles mathématiques.
Les mots clefs sont : ${, $}, $c, $v, $f, $e, $d, $a, $p, $., $=, $(, $), $[, et $].
Les labels sont les successions de caractères alphanumériques, de tirets, de tirets bas ou de virgules.
Les symboles mathématiques sont les successions de caractères imprimables à l'exception du symbole dollar ($).
La grammaire, au format EBNF, est la suivante (ici traduite en français):
`LABEL`, `SYMBOLE-MATHÉMATIQUE` et `BLOC-PREUVE-COMPRESSÉE` sont produits lors de l'analyse lexicale.
Les bases du langage
L'ensemble des symboles qui peuvent être utilisés pour construire des formules est déclaré en utilisant $c (déclaration de constante) et $v (déclaration de variable) déclarations. Par exemple :
$( Declare the constant symbols we will use $)
$c 0 + = -> ( ) term wff |- $.
$( Declare the metavariables we will use $)
$v t r s P Q $.
La grammaire pour les formules est spécifiée en utilisant une combinaison de déclarations $f (hypothèse flottante) et $a (assertion axiomatique). Par exemple :
$( Specify properties of the metavariables $)
tt $f term t $.
tr $f term r $.
ts $f term s $.
wp $f wff P $.
wq $f wff Q $.
$( Define "wff" (part 1) $)
weq $a wff t = r $.
$( Define "wff" (part 2) $)
wim $a wff ( P -> Q ) $.
Axiomes et règles d'inférence sont spécifiés avec les expressions $a avec $ { et $} pour la structure de blocs et optionnellement des expressions $e (hypothèses essentielles). Par exemple :
$( State axiom a1 $)
a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
$( State axiom a2 $)
a2 $a |- ( t + 0 ) = t $.
${
min $e |- P $.
maj $e |- ( P -> Q ) $.
$( Define the modus ponens inference rule $)
mp $a |- Q $.
$}
Utiliser un seul type d'expression, $a, pour définir les règles syntaxiques, les schémas axiomatiques et mes règles d'inférence doit fournir un niveau de flexibilité similaire aux cadres logiques d'ordre supérieur sans dépendre d'un système complexe de types.
Preuves
Les théorèmes (et les règles d'inférence dérivées) sont définis avec les expressions $p. Par exemple :
$( Prove a theorem $)
th1 $p |- t = t $=
$( Here is its proof: $)
tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
tt weq tt tze tpl tt weq tt tt weq wim tt a2
tt tze tpl tt tt a1 mp mp
$.
Notez l'inclusion de la preuve dans l'expression $p. Cela permet une représentation compacte de la preuve sous forme détaillée suivante :
Toutes les étapes des preuves de Metamath utilisent une seule règle de substitution, qui est simplement le remplacement d'une variable avec une expression et non la substitution définie formellement dans le domaine du calcul de prédicats. La substitution formelle, dans les bases de données de Metamath qui la gèrent, est une construction dérivée et non une fonctionnalité intégrée au langage.
La règle de substitution ne dépend pas du système logique utilisé et ne requiert que les remplacements de variables soient faits correctement.
Une preuve étape par étape
Voici un exemple détaillé de la façon dont cet algorithme fonctionne. Les étapes 1 et 2 du théorème 2p2e4 dans le Metamath Proof Explorer (set.mm) sont représentées à gauche. Nous allons expliquer comment Metamath utilise son algorithme de remplacement pour vérifier que l'étape 2 est la conséquence logique de l'étape 1 lorsque vous utilisez le théorème opreq2i. L'étape 2 indique que (2 + 2) = (2 + (1 + 1). C'est la conclusion du théorème opreq2i. Le théorème opreq2i affirme que si A = B = A = B, puis ((C F A) = (C F B)) = ((C F A) = (C F B)). Ce théorème n'apparaîtrait jamais sous cette forme cryptique dans un manuel, mais sa formulation littéraire est banale: lorsque deux quantités sont égales, il peut être remplacé l'un par l'autre dans une opération. Pour vérifier la preuve Metamath essaie d'unifier ((C F A) = (C F B)) = ((C F A) = (C F B)) avec (2 + 2) = (2 + (1 + 1). Il n'y a qu'une seule FAçon de le faire: unifier C avec 2, F avec +, A avec 2 et B avec (1 + 1). Alors maintenant Metamath utilise la prémisse de opreq2i. Cette prémisse indique que A = B. En rA = Bison de son calcul précédent, Metamath sait que A doit être remplacé par 2 et A = B par 1 + 1). Le A = B prémisse A = A = B devient 2=(1 + 1) et donc l'étape 1 est générée. Dans son étape 1 il est unifié avec df-2. df-2 est la définition du nombre 2 et indique que 2 = (1 + 1). Ici l'unification est simplement une question de constantes et est directe (sans problème des variables à remplacer). La vérification est terminée et ces deux étapes de la preuve2p2e4 sont correctes.
Lorsque Metamath unifie (2 + 2) avec B, il faut vérifier que les règles de syntaxe sont respectées. En fait B est de type classdonc Metamath doit vérifier que (2 + 2) est également de type class.
Le programme Metamath est le programme original créé pour manipuler les bases de données écrites avec le langage Metamath. Il dispose d'une interface en ligne de commande et est écrit en C. Vous pouvez charger une base de données Metamath en mémoire, vérifier les preuves de la base, éditer la base (notamment en ajoutant des preuves), et sauvegardée la base modifiée.
Il a une commande prove qui permet aux utilisateurs d'ajouter une preuve, ainsi que des mécanismes pour rechercher une preuve dans la base.
Le programme Metamath peut convertir des déclarations en notation HTML ou TeX par exemple, vous pouvez afficher l'axiome modus ponens de set.mm ainsi :
De nombreux autres programmes peuvent gérer les bases de preuves Metamath, en particulier, il y a au moins 17 vérificateurs de preuve pour le format[3].
Bases de preuves Metamath
Le site Web de Metamath héberge plusieurs bases de données qui stockent des théorèmes dérivés de divers systèmes axiomatiques. La plupart des bases de données (fichiers .mm) ont une interface associée, appelée "Explorer", qui permet de naviguer dans les théorèmes et les preuves de façon ergonomique. La plupart des bases de données utilisent un système de déduction à la Hilbert, mais ce n'est pas obligatoire.
Le Metamath Proof Explorer (et son fichier set.mm) est la principale et de loin la plus grande base de données, avec plus de 23.000 preuves dans sa partie principale en . Il est basé sur la logique classique de premier ordre et la théorie des ensembles ZFC (avec l'ajout de Tarski-Grothendieck théorie des ensembles si nécessaire, par exemple dans la théorie de la catégorie). La base de données a été maintenue pendant plus de vingt ans (les premières preuves en set.mm datent d'). La base de données contient des développements, entre autres, de théorie des ensembles (ordinaux et cardinaux, récursion, équivalents de l'axiome de choix, l'hypothèse continue…), la construction des systèmes de nombres réels et complexes, la théorie de l'ordre, la théorie des graphiques, l'algèbre abstraite, 'algèbre linéaire, topologie générale, analyse réelle et complexe, les espaces Hilbertiens, la théorie des nombres et la géométrie élémentaire. Cette base de données a été créée pour la première fois par Norman Megill, mais au 04/10/2019 on compte 48 collaborateurs (en incluant Norman Megill[6]).
Le Metamath Proof Explorer fait référence à de nombreux manuels pouvant être utilisés conjointement avec Metamath[7]. Ainsi, les personnes intéressées à étudier les mathématiques peuvent utiliser Metamath en relation avec ces livres et vérifier que les affirmations prouvées correspondent à la littérature.
Explorer de logique intuitionniste
Cette base de données développe les mathématiques d'un point de vue constructif, en commençant par les axiomes de la logique intuitionniste et en continuant avec les systèmes axiomes de théorie constructive de l'ensemble.
Explorer New Foundations
Cette base de données développe les mathématiques issus de la théorie New Foundation de Quine.
Explorer de Logique d'ordre supérieur
Cette base de données commence par la logique d'ordre supérieur et dérive des équivalents aux axiomes de la logique de premier ordre et de la théorie des ensembles ZFC .
Bases de données sans Explorer
Le site Web de Metamath héberge quelques autres bases de données qui ne peuvent être consultées en ligne, mais restent néanmoins remarquables. La base de données peano.mm écrite par Robert Solovay formalise l'arithmétique de Peano. La base de données nat.mm formalise la déduction naturelle[8]. La base de données miu.mm formalise le puzzle MU basé sur le système formel MIU présenté dans Gödel, Escher, Bach.
Explorer historiques
Le site Web de Metamath abrite également des bases de données plus anciennes qui ne sont plus maintenues, comme le "Hilbert Space Explorer", qui présente des théorèmes appartenant à la théorie des espaces hilbertiens qui a maintenant rejoint la base principale, et le "Quantum Logic Explorer", qui développe la logique quantique à partir de la théorie des lattices orthomodulaires.
Déduction Naturelle
Parce que Metamath a un concept très générique de ce qui est une preuve (c'est-à-dire un arbre de formules connectées par des règles d'inférence) et aucune logique spécifique n'est incorporée dans le logiciel, Metamath peut être utilisé avec des espèces de logique aussi différentes que des logiques de style Hilbert ou logiques basées sur des séquences ou même avec calcul lambda.
Cependant, Metamath ne fournit pas de support direct pour les systèmes de déduction naturel. Comme indiqué précédemment, la base de données nat.mm formalise la déduction naturelle. Le Metamath Proof Explorer (avec sa base de données set.mm) utilise un ensemble de conventions qui permettent l'utilisation d'approches de déduction naturelle dans une logique de style hilbertien.
Autres travaux autour de Metamath
Preuve de vérification
En utilisant les idées de conception mises en œuvre dans Metamath, Raph Levien a réalisé un très petit vérificateur, mmverify.py, en seulement 500 lignes de code Python.
Ghilbert est un langage plus élaboré basé sur mmverify.py[9]. Levien cherche à obtenir un système qui permettrait la collaboration entre plusieurs utilisateurs et son travail promeut la modularité et l'interconnection des modules théoriques.
Sur la base de ces travaux originaux, de multiples réimplémentations de l'architecture Metamath ont vu le jour dans de nombreux langages de programmation : Juha Arpiainen a réalisé son vérificateur Bourbaki[10] en Common Lisp et Marnix Klooster a codé le sien en Haskell called Hmm[11].
Bien que tous utilisent l'approche commune de Metamath pour le mécanisme de vérification formelle, ils apportent également leurs propres concepts originaux.
Éditeurs
Mel O'Cat a conçu un système nommé Mmj2, qui propose une interface utilisateur graphique pour la saisie des preuves[12]. L'objectif initial de Mel O'Cat était de permettre à l'utilisateur de saisir les preuves en écrivant simplement les formules et en laissant Mmj2 trouver les règles d'inférence appropriées pour les relier. Dans Metamath au contraire ne peut entrer dans les noms des théorèmes. Vous ne pouvez pas entrer les formules directement. Mmj2 permet également de saisir une preuve dans les deux sens alors que Metamath permet seulement de saisir une preuve en partant du résultat. De plus, Mmj2 possède un vrai analyseur grammatical, ce qui n'est pas le cas pour Metamath. Cette différence technique apporte plus de confort à l'utilisateur. En particulier, Metamath hésite parfois entre plusieurs formules et demande à l'utilisateur de choisir. Avec Mmj2, cette limitation n'existe plus.
Le projet Mmide[13] de William Hale ajoute lui aussi une interface utilisateur graphique à Metamath. Paul Chapman travaille sur un nouvel explorer, qui peut mettre en évidence un théorème appliqué avant et après l'action de substitution..
Milpgame est un assistant de preuve et un vérificateur (un message s'affiche en cas d'erreur) avec une interface utilisateur graphique pour le langage de Metamath (set.mm), écrit par Filip Cernatescu, et distribué sous forme d'application Java open source (licence MIT) (application multi-plateforme: Windows, Linux, Mac OS). L'utilisateur peut introduire la démonstration dans le deux sens. Milpgame vérifie si une déclaration est bien formée (présence d'un vérificateur syntaxique). Vous pouvez enregistrer des preuves inachevées sans l'utilisation du théorème dummylink. La preuve s'affiche sous forme d'arbre, les déclarations sont affichées à l'aide des définitions html. Milpgame est distribué sous forme d'archive .jar Java (JRE version 6u24 requis, développé avec l'IDE NetBeans ID.
(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Metamath » (voir la liste des auteurs).
Références
↑Norman Megill et David A. Wheeler, Metamath: A Computer Language for Mathematical Proofs, Morrisville, North Carolina, US, Second, , 248 p. (ISBN978-0-359-70223-7, lire en ligne)
