In[]:=
ResourceFunction["MetamathImport"][URL["https://raw.githubusercontent.com/geohot/twitchcoq/master/metamath/twoplustwo.mm"],"ProofGraphStructure"]
Out[]=
In[]:=
ResourceFunction["MetamathImport"][URL["https://raw.githubusercontent.com/geohot/twitchcoq/master/metamath/twoplustwo.mm"]]
Out[]=

Addition Facts

eq[succ[succ[0]],plus[succ[0],succ[0]]]
In[]:=
Table[eq[Nest[s,0,i+j],plus[Nest[s,0,i],Nest[s,0,j]]],{i,3},{j,3}]
Out[]=
{{eq[s[s[0]],plus[s[0],s[0]]],eq[s[s[s[0]]],plus[s[0],s[s[0]]]],eq[s[s[s[s[0]]]],plus[s[0],s[s[s[0]]]]]},{eq[s[s[s[0]]],plus[s[s[0]],s[0]]],eq[s[s[s[s[0]]]],plus[s[s[0]],s[s[0]]]],eq[s[s[s[s[s[0]]]]],plus[s[s[0]],s[s[s[0]]]]]},{eq[s[s[s[s[0]]]],plus[s[s[s[0]]],s[0]]],eq[s[s[s[s[s[0]]]]],plus[s[s[s[0]]],s[s[0]]]],eq[s[s[s[s[s[s[0]]]]]],plus[s[s[s[0]]],s[s[s[0]]]]]}}
In[]:=
ExpressionGraph/@Flatten[%]
Out[]=

,
,
,
,
,
,
,
,

In[]:=
ExpressionGraph[#,VertexLabelsAutomatic]&/@Flatten[%327]
Out[]=

,
,
,
,
,
,
,
,

In[]:=
VertexList

Out[]=
{1,2,3,4,5,6,7,8,9}
In[]:=
AnnotationValue
,VertexLabels
Out[]=
{6s,3s,5plus,8s,70,40,90,2s,1eq}
In[]:=
EdgeList
/.AnnotationValue
,VertexLabels
Out[]=
{eqs,ss,s0,eqplus,pluss,s0,pluss,s0}
In[]:=
atomify[g_]:=Graph[(DirectedEdge@@@EdgeList[g])/.(AnnotationValue[g,VertexLabels])]
In[]:=
ExpressionGraph[#,VertexLabelsAutomatic]&/@Flatten[Table[eq[Nest[s,0,i+j],plus[Nest[s,0,i],Nest[s,0,j]]],{i,3},{j,3}]]
Out[]=

,
,
,
,
,
,
,
,

In[]:=
atomify/@%
Out[]=

,
,
,
,
,
,
,
,


Really should use more of a WM approach with ordered relations

“Ultrapure mathematics”