Extracting Definitions

(*setmm=ResourceFunction["MetamathImport"][URL["https://raw.githubusercontent.com/metamath/set.mm/master/set.mm"]];*)
(*"DATA/setmm-basic.wxf"*)
defassoc=KeySelect[setmm["Statements"],StringStartsQ["df-"]];
In[]:=
RulesFromDefs[("Axiom"|"EssentialHypothesis")[_,x_List,___]]:=With[{xx=DeleteCases[DeleteCases[x,Alternatives@@mmvars],"("|")"|""|"{"|"}"]},Thread[xx[[2]]->Drop[xx,2]]]
In[]:=
mmvars=Keys[Select[setmm["Symbols"],Head[#]==="Variable"&]];
In[]:=
mmconsts=Keys[Select[setmm["Symbols"],Head[#]==="Constant"&]];
In[]:=
RulesFromDefs[setmm["Statements"]["df-gcd"]]
Out[]=
{gcd=,gcde.,gcdZZ,gcd,,gcde.,gcdZZ,gcd|->,gcdif,gcd=,gcd0,gcd/\,gcd=,gcd0,gcd,,gcd0,gcd,,gcdsup,gcde.,gcdZZ,gcd|,gcd||,gcd/\,gcd||,gcd,,gcdRR,gcd,,gcd<}
In[]:=
Graph[Flatten[Values[RulesFromDefs/@Take[defassoc,5]]]]
Out[]=
In[]:=
defgraph2=Graph[Flatten[Values[RulesFromDefs/@defassoc]]]
Out[]=
Graph
Vertex count: 1261
Edge count: 26305

In[]:=
MatrixPlot[AdjacencyMatrix[%]]
Out[]=
In[]:=
TakeLargestBy[Transpose[{VertexList[defgraph2],VertexInDegree[defgraph2]}],Last,100]
Out[]=
{{`,3482},{e.,3380},{=,1770},{,,1588},{|->,1137},{/\,742},{|,695},{_V,614},{A.,608},{>.,598},{<.,594},{Base,429},{E.,348},{/,314},{1,253},{0,251},{dom,244},{X.,214},{U.,198},{~P,194},{ran,182},{1st,164},{ndx,156},{i^i,149},{2nd,147},{C_,145},{].,145},{[.,144},{\,139},{CC,133},{->,129},{",128},{o.,122},{^m,120},{]_,118},{(/),117},{[_,117},{`',116},{if,115},{+,105},{NN,103},{RR,100},{ZZ,94},{<->,88},{-,86},{~H,85},{|`,85},{+g,83},{<,83},{u.,82},{NN0,82},{x.,82},{#,78},{2,77},{:,72},{0g,67},{EE,64},{Scalar,61},{^,60},{le,60},{=/=,59},{\/,58},{1o,58},{...,53},{Top,53},{-.,51},{<_,49},{.r,47},{RR*,47},{Fin,45},{-->,44},{_om,43},{+oo,41},{Hom,40},{iota_,39},{-u,38},{Cat,37},{.s,37},{">,36},{dist,36},{Vtx,35},{2o,33},{_I,32},{..^,31},{Atoms,30},{_E,30},{|`s,29},{|^|,29},{Poly1,29},{N.,28},{comp,28},{<",28},{sum_,28},{sSet,27},{LTrn,27},{Slot,26},{U_,25},{_i,25},{Prime,25},{TopOpen,24}}
In[]:=
VertexDelete[defgraph2,First/@TakeLargestBy[Transpose[{VertexList[defgraph2],VertexInDegree[defgraph2]}],Last,100]]
Out[]=
​
In[]:=
VertexDelete[defgraph2,First/@TakeLargestBy[Transpose[{VertexList[defgraph2],VertexInDegree[defgraph2]}],Last,100],GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2,EdgeStyle->Opacity[.4],VertexLabelsAutomatic]
Out[]=

Theorem Network

First thing is the statement; later thing is proofs....

Statement of statement should only contain defined terms

Multiple pieces of proof:
1. Which other theorems it’s pulling in
2. The “glue” i.e. LoI i.e. connectives etc.

I.e. there are a few unused definitions

Definitions are used as a macro pass

A previous historical version would show more isolated pieces...

As math progresses, the entailments join things up

Energy density vs. position in MM space?

How uniform is dimension vs. position?

FeatureSpacePlot based on proofs?

Homogeneity of human colonization of metamathematical space

If one assumes intrinsic homogeneity .... Where should one mine?

[ comparison between geo layout of cities and internet connectivity ]

Axioms

Famous Theorems

How many definitions do they ultimately depend on?

< Make a fabric based on theorems >

[[[ Lay out axioms across the page then show dependency of each theorem for each axiom ]]]

[[ split axioms by field ; order and color that way ... then for each theorem there are dots depending on dependency ]]