Wolfram Research

Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

Function Repository Resource:

 MetamathImport (1.0.0) current version: 2.0.0 »

Source Notebook

Import a Metamath file

Contributed by: Mario Carneiro and Nikolay Murzin

ResourceFunction["MetamathImport"][src]

imports Metamath source code from src and returns an Association with defined symbols and statements.

ResourceFunction["MetamathImport"][src,param]

returns a specific parameter param computed from provided Metamath source code.

Details and Options

The src can be a File, URL, String or a List of "Raw" parsed statements.
The parameter param for ResourceFunction["MetamathImport"] may be one of the following:
All association of all elements
"Axioms" list of defined axioms
"Constants" list of defined symbols
"ProofGraph" a graph with edges indicating a usage of theorems by other theorems
"ProofGraphStructure" a proof graph without labels
"Raw" raw parsed statements
"Theorems" list of defined theorems
"Variables" list of defined variables
Options for ResourceFunction["MetamathImport"] may be one of the following:
"Verify" False whether to verify proofs or not

Examples

Basic Examples

Import Metamath source code with a bunch of constants and a simple axiom:

In[1]:=
ResourceFunction["MetamathImport"][" $c = 0 S 1 $. wp $a = 0 S 1 $. "]
Out[1]=

Import a basic Metamath source code sample with 4 constants, 5 variables, 5 floating hypotheses, 1 axiom and 2 proved theorems:

In[2]:=
ResourceFunction["MetamathImport"][" $c ( ) \[Rule] wff $. $v p q r s t $. wp $f wff p $. wq $f wff q $. wr $f wff r $. ws $f wff s $. wt $f wff t $. w\[Rule] $a wff ( p \[Rule] q ) $. w\[Rule](\[Rule]) $p wff ( r \[Rule] ( s \[Rule] t ) ) $= wr ws wt w\[Rule] w\[Rule] $. w(\[Rule])\[Rule] $p wff ( ( r \[Rule] s ) \[Rule] t ) $= wr ws w\[Rule] wt w\[Rule] $. "]
Out[2]=

Construct a proof graph:

In[3]:=
ResourceFunction["MetamathImport", ResourceVersion->"1.0.0"]["\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n", "ProofGraph"]
Out[3]=

Scope

The option "Verify" adds annotation edges:

In[4]:=
ResourceFunction["MetamathImport", ResourceVersion->"1.0.0"]["\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n", "ProofGraph", "Verify" -> True]
Out[4]=

Label vertices by symbol name:

In[5]:=
Graph[AnnotationDelete[ ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n", "ProofGraph", "Verify" -> True], VertexLabels], VertexLabels -> "Name"]
Out[5]=

Unlabeled proof graph for a proof of 2+2=4 based on Peano axioms:

In[6]:=
ResourceFunction["MetamathImport"][ URL["https://raw.githubusercontent.com/geohot/twitchcoq/master/metamath/realtwoplustwo.mm"], "ProofGraphStructure"]
Out[6]=

Pre-parse into a raw expression before importing:

In[7]:=
parsedRaw = ResourceFunction["MetamathImport"][ URL["https://raw.githubusercontent.com/geohot/twitchcoq/master/metamath/twoplustwo.mm"], "Raw"];
In[8]:=
ResourceFunction["MetamathImport"][parsedRaw, "ProofGraphStructure"]
Out[8]=

Options

Verify

Verifying theorems expands proofs with more information:

In[9]:=
Cases[ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n", "Theorems", "Verify" -> True], "Theorem"[label_, _, _, proof_] :> label -> proof]
Out[9]=

Neat Examples

Verify logic, set theory Metamath source code and examine a part of its proof graph:

In[10]:=
proofGraph = ResourceFunction["MetamathImport"][ URL["https://raw.githubusercontent.com/metamath/set.mm/master/iset.mm"], "ProofGraph", "Verify" -> True]; // AbsoluteTiming
Out[10]=
In[11]:=
Subgraph[proofGraph, VertexOutComponent[proofGraph, "2p2e4", 1]] // SimpleGraph
Out[11]=

Version History

  • 2.0.0 – 07 March 2022
  • 1.0.0 – 21 September 2020

Source Metadata

  • Citation:
    Original implementation by Mario Carneiro: http://us.metamath.org/downloads/mmamm.m

Related Resources

License Information