## 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 ]]