Wolfram Function Repository
Instant-use add-on functions for the Wolfram Language
Function Repository Resource:
Import a Metamath file
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. |
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 |
"Verify" | False | whether to verify proofs or not |
Import Metamath source code with a bunch of constants and a simple axiom:
In[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]:= |
![]() |
Out[2]= |
![]() |
Construct a proof graph:
In[3]:= |
![]() |
Out[3]= |
![]() |
The option "Verify" adds annotation edges:
In[4]:= |
![]() |
Out[4]= |
![]() |
Label vertices by symbol name:
In[5]:= |
![]() |
Out[5]= |
![]() |
Unlabeled proof graph for a proof of 2+2=4 based on Peano axioms:
In[6]:= |
![]() |
Out[6]= |
![]() |
Pre-parse into a raw expression before importing:
In[7]:= |
![]() |
In[8]:= |
![]() |
Out[8]= |
![]() |
Verifying theorems expands proofs with more information:
In[9]:= |
![]() |
Out[9]= |
![]() |
Verify logic, set theory Metamath source code and examine a part of its proof graph:
In[10]:= |
![]() |
Out[10]= |
![]() |
In[11]:= |
![]() |
Out[11]= |
![]() |
This work is licensed under a Creative Commons Attribution 4.0 International License