In[]:=
mm=ResourceFunction["MetamathImport"];
In[]:=
theorems=Cases[mm["Statements"],"Theorem"[l_,__]:>l]
Out[]=
{eqcom,eqtr,eq3tr,eq4tr,eq5tr,eq6tr,eq7tr,eq8tr,eq9tr,eq10tr,eq11tr,eq12tr,eq13tr,eq14tr,eq15tr,eq16tr,eq17tr,eq18tr,eq19tr,shefeq1,shefeq2,shefeq11,shefeq12,shefeq21,shefeq22,shefeq111,shefeq112,shefeq121,shefeq211,shefeq212,shefeq221,shefeq222,shefeq1112,shefeq1211,shefeq1221,shefeq2121,shefeq2211,shefeq2212,shefeq2221,shefeq2222,shefeq21121,shefeq21221,shefeq22111,shefeq22112,shefeq22121,shefeq221121,shefeq221221,shefeq222121,shefeqeq,L1,L2,L3,L4,L5,L6,L7,L8,L9,L10,L11,L12,T1,L13,L14,L15,L16,L17,L18,L19,L20,L21,L22,L23,L24,L25,L26,L27,L28,L29,L30,L31,L32,L33,L34,L35,L36,L37,L38,L39,L40,L41,L42,L43,L44,L45,L46,T2,L47,L48,L49,L50,L51,L52,L53,L54,L55,L56,L57,L58,L59,L60,L61,L62,L63,L64,T3,nksL1,nksL2,nksL3,nksL4,nksL5,nksL6,nksL7,nksL8,nksL9,nksL10,nksL11,nksL12,nksL13,nksL14,nksL15,nksL16,nksL17,nksL18,nksL19,nksL20,nksL21,nksL22,nksT1,nksL23,nksL24,nksL25,nksL26,nksL27,nksL28,nksL29,nksL30,nksL31,nksL32,nksL33,nksL34,nksL35,nksL36,nksL37,nksL38,nksL39,nksL40,nksL41,nksL42,nksL43,nksL44,nksL45,nksL46,nksL47,nksL48,nksL49,nksL50,nksL51,nksL52,nksL53,nksL54,nksL55,nksL56,nksT2,nksL57,nksL58,nksL59,nksL60,nksL61,nksL62,nksL63,nksL66,nksL67,nksL68,nksL69,nksL70,nksL71,nksL72,nksL73,nksL74,nksL75,nksL76,nksL77,nksL78,nksL79,nksL80,nksL81,nksT3}
In[]:=
axioms=Cases[mm["Statements"],"Axiom"[l_,__]:>l]
Out[]=
{tshef,weq,ax-eqcom,ax-eqtr,ax-shefeq1,ax-shefeq2,ax-A}
In[]:=
MetaMathProof[mm]["L1","ExpandedTree"]
Out[]=
In[]:=
MetaMathProof[mm]["L1","ExpandedGraph"]
Out[]=
This is like a function taking arguments:
In[]:=
ReverseGraph[MetaMathProof[mm]["L1","ExpandedGraph"]]
Out[]=
In[]:=
mm["Statements"]["ax-A"]
Out[]=
Axiom[ax-A,{|-,(,(,(,b,|,c,),|,a,),|,(,b,|,(,(,b,|,a,),|,b,),),),=,a},{{},{Hypothesis[wva,{term,a}],Hypothesis[wvb,{term,b}],Hypothesis[wvc,{term,c}]},{}}]
In[]:=
StringJoin[%[[2]]]
Out[]=
|-(((b|c)|a)|(b|((b|a)|b)))=a
In[]:=
StringJoin[mm["Statements"]["L1"][[2]]]
Out[]=
|-((a|b)|(((c|d)|a)|((((c|d)|a)|b)|((c|d)|a))))=b
In[]:=
MetaMathProof[mm]["T1","Tree"]
Out[]=
In[]:=
MetaMathProof[mm]["T1","Graph"]
Out[]=
In[]:=
MetaMathProof[mm]["T1","ExpandedGraph"]
[[ This is the equivalent of a pure-substitution-based analog of the FEP results ]]
[[ This is the equivalent of a pure-substitution-based analog of the FEP results ]]
[[ Metamath is taking clusters of nodes and naming them as named theorems ]]
[[ Metamath is taking clusters of nodes and naming them as named theorems ]]
Not only is it picking a particular “path” through metamathematical space; it is also describing the path using coarse-graining [[ i.e. it’s annotating raw metamathematical space with named chunks ]]
In[]:=
ReverseGraph[MetaMathProof[mm]["ax-A","ExpandedGraph"]]
Out[]=
ReverseGraphFailure
In FindEquationalProof, one “burns down” to True; in Metamath one builds up to the theorem one wants...
In FindEquationalProof, one “burns down” to True; in Metamath one builds up to the theorem one wants...