Voir la source de Metamath

{{Infobox Logiciel
 | créateur                 = Norm Megill
 | dépôt                    = {{Github|metamath}}
 | état                     = {{oui|En développement actif}}
 | type                     = [[Assistant de preuve]]
 | langues                  = [[Anglais]]
 | langage de programmation = [[ANSI C]]
 | environnement = [[Linux]], [[Microsoft Windows|Windows]], [[macOS]]es
 | licence                  = [[GNU General Public License]] ([[Creative Commons]] [[Domaine public (propriété intellectuelle)|Domaine public]] pour les bases)
 | documentation            = {{URL|http://us.metamath.org/downloads/metamath.pdf}}
 | site web                 = {{URL|http://metamath.org}}
 | politique de prix        = Gratuit et [[open source]]
}}

'''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<ref name="metamath-book">{{Ouvrage|prénom1=Norman|nom1=Megill|prénom2=David A.|nom2=Wheeler|titre=Metamath: A Computer Language for Mathematical Proofs|lieu=Morrisville, North Carolina, US|éditeur=Second|date=2019-06-02|pages totales=248|isbn=978-0-359-70223-7|lire en ligne=http://us.metamath.org/#book}}</ref>.  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<ref>{{Lien web |auteur=Megill, Norman |titre=What is Metamath? |url=http://us.metamath.org/#faq |série=Metamath Home Page}}</ref>.

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 [https://www.cs.ru.nl/~freek/100/ "Formalizing 100 Theorems"], ce qui en fait le quatrième après HOL Light et [[Isabelle (logiciel)|Isabelle]] et [[Rocq (logiciel)|Rocq]], mais devant, [[Mizar (système)|Mizar]], [http://www.lemma-one.com/ProofPower/index/ Proof Power], [[Lean (assistant de preuve)|Lean]], [[:en:Nqthm|Nqthm]], [[:en:ACL2|ACL2]] et [[:en:Nuprl|Nuprl]]. Il y a au moins 17 vérificateurs de preuves pour les bases de théorèmes au  format Metamath<ref name="us.metamath.org">{{Lien web |auteur=Megill |prénom=Norman |titre=Known Metamath proof verifiers |url=http://us.metamath.org/other.html#verifiers |consulté le=14 juillet 2019}}</ref>.

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<ref>[http://us2.metamath.org:88/mpeuni/mmtheorems.html TOC of Theorem List - Metamath Proof Explorer]</ref>.

== Le langage Metamath ==
Le langage Metamath est un [[métalangage]], adapté au développement d'une grande variété de [[Système formel|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  [[Théorie des ensembles de Zermelo-Fraenkel|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<ref name="howpswork">{{Lien web |auteur=Megill,Norman |titre=How Proofs Work |url=http://us.metamath.org/mpegif/mmset.html#proofs |série=Metamath Proof Explorer Home Page}}</ref>).

=== 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 [[tiret]]s, de [[tiret bas|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 [[Extended Backus-Naur Form|EBNF]], est la suivante (ici traduite en français):

<syntaxhighlight lang=ebnf>base-de-données ::= déclaration-globale*

déclaration-globale ::=
  inclusion-de-fichier | déclaration-de-constantes | déclaration

inclusion-de-fichier ::= '$[' nom-de-fichier '$]'

déclaration-de-constantes ::= '$c' constante+ '$.'

déclaration ::= bloc | déclaration-de-variables | déclaration-disjointe |
  hypothèse | affirmation

bloc ::= '${' déclaration* '$}'

déclaration-de-variables ::= '$v' variable+ '$.'

déclaration-disjointe ::= '$d' variable variable variable* '$.'

hypothèse ::= déclaration-flottante | déclaration-essentielle

déclaration-flottante ::= LABEL '$f' code-type variable '$.'

déclaration-essentielle ::= LABEL '$e' code-type SYMBOLE-MATHÉMATIQUE* '$.'

affirmation ::= axiome | théorème

axiome ::= LABEL '$a' code-type SYMBOLE-MATHÉMATIQUE* '$.'

théorème ::= LABEL '$p' code-type SYMBOLE-MATHÉMATIQUE*
  '$=' preuve '$.'

preuve ::= preuve-non-compressée | preuve-compressée
preuve-non-compressée ::= (LABEL | '?')+
preuve-compressée ::= '(' LABEL* ')' BLOC-PREUVE-COMPRESSÉE

code-type ::= constante

nom-de-fichier ::= SYMBOLE-MATHÉMATIQUE
constante ::= SYMBOLE-MATHÉMATIQUE
variable ::= SYMBOLE-MATHÉMATIQUE
</syntaxhighlight>

`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 :
<pre>
$( Declare the constant symbols we will use $)
    $c 0 + = -> ( ) term wff |- $.
$( Declare the metavariables we will use $)
    $v t r s P Q $.
</pre>
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 :

<pre>
$( 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 ) $.
</pre>

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 :

<pre>
$( 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 $.
    $}
</pre>

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 <code>$p</code>. Par exemple :

<pre>
$( 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
     $.
</pre>

Notez l'inclusion de la preuve dans l'expression <code>$p</code>.  Cela permet une représentation compacte de la preuve sous forme détaillée suivante :

<syntaxhighlight line lang="nasm">
tt            $f term t
tze           $a term 0
1,2 tpl       $a term ( t + 0 )
3,1 weq       $a wff ( t + 0 ) = t
1,1 weq       $a wff t = t
1 a2          $a |- ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
7,1 weq       $a wff ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
9,1 weq       $a wff ( t + 0 ) = t
1,1 weq       $a wff t = t
10,11 wim     $a wff ( ( t + 0 ) = t -> t = t )
1 a2          $a |- ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
14,1,1 a1     $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )
8,12,13,15 mp $a |- ( ( t + 0 ) = t -> t = t )
4,5,6,16 mp   $a |- t = t
</syntaxhighlight>

La forme « essentielle » de la preuve masque les détails syntaxiques et conduit à une présentation plus conventionnelle :

<syntaxhighlight line lang="nasm">
a2             $a |- ( t + 0 ) = t
a2             $a |- ( t + 0 ) = t
a1             $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )
2,3 mp         $a |- ( ( t + 0 ) = t -> t = t )
1,4 mp         $a |- t = t
</syntaxhighlight>

=== Substitutions ===
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. 
[[Fichier:Proofstep.gif|droite|vignette|592x592px|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 <code>2p2e4</code> 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 <code>opreq2i</code>. L'étape 2 indique que (2 + 2) = (2 + (1 + 1). C'est la conclusion du théorème <code>opreq2i</code>. Le théorème <code>opreq2i</code> affirme que si {{Formule|1={{magenta|''A''}} = {{magenta|''B''}}}} = {{Formule|1={{magenta|''A''}} = {{magenta|''B''}}}}, puis ({{Formule|1=({{magenta|''C F A''}}) = ({{magenta|''C F B''}})}}) = ({{Formule|1=({{magenta|''C F A''}}) = ({{magenta|''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 ({{Formule|1=({{magenta|''C F A''}}) = ({{magenta|''C F B''}})}}) = ({{Formule|1=({{magenta|''C F A''}}) = ({{magenta|''C F B''}})}}) avec (2 + 2) = (2 + (1 + 1). Il n'y a qu'une seule {{Magenta|{{mvar|F}}}}{{Magenta|{{mvar|A}}}}çon de le faire: unifier {{Magenta|{{mvar|C}}}} avec 2, F avec {{Formule|+}}, A avec {{Magenta|{{mvar|2}}}} et {{Magenta|{{mvar|B}}}} avec (1 + 1). Alors maintenant Metamath utilise la [[prémisse]] de <code>opreq2i</code>. Cette prémisse indique que A = B. En r{{Formule|1={{magenta|''A''}} = {{magenta|''B''}}}}ison de son calcul précédent, Metamath sait que A doit être remplacé par {{Val|2}} et {{Formule|1={{magenta|''A''}} = {{magenta|''B''}}}} par 1 + 1). Le {{Formule|1={{magenta|''A''}} = {{magenta|''B''}}}} prémisse A = {{Formule|1={{magenta|''A''}} = {{magenta|''B''}}}} devient 2=(1 + 1) et donc l'étape 1 est générée. Dans son étape 1 il est unifié avec df-<code>2</code>. <code>df-2</code> 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 preuve<code>2p2e4</code> sont correctes.

Lorsque Metamath unifie (2 + 2) avec {{Magenta|{{mvar|B}}}}, il faut vérifier que les règles de syntaxe sont respectées. En fait {{Magenta|{{mvar|B}}}} est de type <code>class</code>donc Metamath doit vérifier que (2 + 2) est également de type <code>class</code>.

== Le vérificateur de preuves Metamath ==
{{Section guide pratique|date=octobre 2023}}
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 [[Hypertext Markup Language|HTML]] ou [[TeX]] par exemple, vous pouvez afficher l'axiome [[modus ponens]] de set.mm ainsi :

: <math>\vdash \varphi\quad\&\quad \vdash ( \varphi \rightarrow \psi )\quad\Rightarrow\quad \vdash \psi</math>

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<ref name="us.metamath.org"/>.

== Bases de preuves Metamath ==
Le [[Site web|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 [[Ergonomie|ergonomique]]. La plupart des bases de données utilisent un [[Système à la Hilbert|système de déduction à la Hilbert]], mais ce n'est pas obligatoire.

=== Metamath Proof Explorer ===
{{Infobox Site web
 | url                         = {{URL|http://us.metamath.org/mpeuni/mmset.html}}
 | commercial                  = No
 | type                        = [[Online encyclopedia]]
}}
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 {{date-|juillet 2019}}. Il est basé sur la [[Calcul des prédicats|logique]] classique de premier ordre et la théorie des ensembles [[Théorie des ensembles de Zermelo-Fraenkel|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'{{date-|août 1993}}). 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 [[Nombre réel|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<ref name="gource">{{Lien web |auteur=Wheeler, David A. |titre=Metamath set.mm contributions viewed with Gource through 2019-10-04 |url=https://www.youtube.com/watch?v=XC1g8FmFcUU}}</ref>).

Le Metamath Proof Explorer fait référence à de nombreux manuels pouvant être utilisés conjointement avec Metamath<ref name="reading">{{Lien web |auteur=Megill, Norman |titre=Reading suggestions |url=http://us2.metamath.org:8888/mpegif/mmset.html#read |série=Metamath}}</ref>. 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 Foundations|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]]<ref name="natmm">{{Lien web |auteur=Liné, Frédéric |titre=Natural deduction based Metamath system |url=http://wiki.planetmath.org/cgi-bin/wiki.pl/Natural_deduction_based_metamath_system |archive-url=https://archive.today/20121228041230/http://wiki.planetmath.org/cgi-bin/wiki.pl/Natural_deduction_based_metamath_system |archive-date=2012-12-28}}</ref>. 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 naturelle|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<ref name="ghilbert">{{lien web| auteur=Levien,Raph | titre=Ghilbert | url=https://ghilbert-app.appspot.com}}</ref>. 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<ref name="bourbaki">{{lien web| auteur=Arpiainen, Juha | titre=Presentation of Bourbaki | url=http://wiki.planetmath.org/cgi-bin/wiki.pl/Bourbaki_proof_checker | archiveurl=https://archive.today/20121228115800/http://wiki.planetmath.org/cgi-bin/wiki.pl/Bourbaki_proof_checker | archivedate=2012-12-28 }}</ref> en [[Common Lisp]] et Marnix Klooster a codé le sien en [[Haskell]] called ''Hmm''<ref name="Hmm">{{lien web| auteur=Klooster,Marnix | titre=Presentation of Hmm | url=http://wiki.planetmath.org/cgi-bin/wiki.pl/Hmm | archiveurl=https://web.archive.org/web/20120402081636/http://wiki.planetmath.org/cgi-bin/wiki.pl/Hmm | archivedate=2012-04-02 }}</ref>.

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 graphique|interface utilisateur graphique]] pour la saisie des preuves<ref name="mmj2">{{Lien web |auteur=O'Cat,Mel |titre=Presentation of mmj2 |url=http://wiki.planetmath.org/cgi-bin/wiki.pl/mmj2 |archive-url=https://web.archive.org/web/20131219001737/http://wiki.planetmath.org/cgi-bin/wiki.pl/mmj2 |archive-date=December 19, 2013}}</ref>. 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<ref name="mmide">{{Lien web |auteur=Hale, William |titre=Presentation of mmide |url=http://wiki.planetmath.org/cgi-bin/wiki.pl/mmide |archive-url=https://archive.today/20121228044320/http://wiki.planetmath.org/cgi-bin/wiki.pl/mmide |archive-date=2012-12-28}}</ref> 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 graphique|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.

== Voir aussi ==

* [[Assistant de preuve]]
* [[Assistant de preuve|Contrôle automatique de la vérification]]
* [[Démonstration automatique de théorèmes]]
* [[Rocq (logiciel)|Rocq]]
* [[Isabelle (logiciel)|Isabelle]]
* [[Mizar (système)|Système Mizar]]
* [[PhoX (logiciel)|PhoX]]
* [[Prototype Verification System|PVS]]

{{Traduction/Référence|lang1=en|art1=Metamath|id1=1029559253}}

== Références ==
 {{Références}}

== Liens externes ==

* [http://us.metamath.org Metamath]: site officiel.

{{Portail|logiciels libres|mathématiques}}

[[Catégorie:Assistant de preuve]]
[[Catégorie:Théorie de la démonstration]]
[[Catégorie:Logique formelle]]
[[Catégorie:Logiciel libre sous licence GPL]]