Extracting Definitions
Extracting Definitions
(*setmm=ResourceFunction["MetamathImport"][URL["https://raw.githubusercontent.com/metamath/set.mm/master/set.mm"]];*)
(*"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=,gcde.,gcdZZ,gcd,,gcde.,gcdZZ,gcd|->,gcdif,gcd=,gcd0,gcd/\,gcd=,gcd0,gcd,,gcd0,gcd,,gcdsup,gcde.,gcdZZ,gcd|,gcd||,gcd/\,gcd||,gcd,,gcdRR,gcd,,gcd<}
In[]:=
Graph[Flatten[Values[RulesFromDefs/@Take[defassoc,5]]]]
Out[]=
In[]:=
defgraph2=Graph[Flatten[Values[RulesFromDefs/@defassoc]]]
Out[]=
Graph
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",AspectRatio1/2,EdgeStyle->Opacity[.4],VertexLabelsAutomatic]
Out[]=
Theorem Network
Theorem Network
First thing is the statement; later thing is proofs....
Statement of statement should only contain defined terms
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.
Multiple pieces of proof:
1. Which other theorems it’s pulling in
2. The “glue” i.e. LoI i.e. connectives etc.
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
Definitions are used as a macro pass
A previous historical version would show more isolated pieces...
A previous historical version would show more isolated pieces...
As math progresses, the entailments join things up
Energy density vs. position in MM space?
Energy density vs. position in MM space?
How uniform is dimension vs. position?
How uniform is dimension vs. position?
FeatureSpacePlot based on proofs?
FeatureSpacePlot based on proofs?
Homogeneity of human colonization of metamathematical space
Homogeneity of human colonization of metamathematical space
If one assumes intrinsic homogeneity .... Where should one mine?
If one assumes intrinsic homogeneity .... Where should one mine?
[ comparison between geo layout of cities and internet connectivity ]
[ comparison between geo layout of cities and internet connectivity ]
Axioms
Axioms
Famous Theorems
Famous Theorems
How many definitions do they ultimately depend on?
How many definitions do they ultimately depend on?
< Make a fabric based on theorems >
< Make a fabric based on theorems >
[[[ Lay out axioms across the page then show dependency of each theorem for each axiom ]]]
[[[ 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 ]]
[[ split axioms by field ; order and color that way ... then for each theorem there are dots depending on dependency ]]