You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
[ Use MetamathImport ]
In[]:=
mm=MetamathImportUncompress@
Out[]=
MetamathObject
In[]:=
DumpSave["mmset-object.mx",mm]
Out[]=
MetamathObject
In[]:=
metamathGraph=mm["DependencyGraph"];
In[]:=
SetDirectory[NotebookDirectory[]]
Out[]=
/Users/sw/Dropbox/Physics/WorkingMaterial/2022
In[]:=
Export["DATA/setmm-graph.wxf",metamathGraph]
Out[]=
DATA/setmm-graph.wxf
In[]:=
VertexCount[metamathGraph]
Out[]=
42124
In[]:=
gdm=GraphDistanceMatrix[metamathGraph];
In[]:=
frows=Count[#,Except[Infinity]]&/@gdm;
In[]:=
outsizes=AssociationThread[VertexList[metamathGraph],frows];
In[]:=
Export["DATA/setmm-out-sizes.wxf",outsizes]
Out[]=
DATA/setmm-out-sizes.wxf
In[]:=
TakeLargest[outsizes,5]
Out[]=
dirith10360,dirith210359,rplogsum10356,dchrmusum10281,dchrvmasum10281
In[]:=
Histogram[Values[outsizes],Frame->True,AspectRatio1/2]
Out[]=
In[]:=
barData=Table[Counts@DeleteCases["SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)"|"GUIDES AND MISCELLANEA"]@DeleteMissing@Lookup[metamathAssoc,Extract[VertexList[metamathGraph],Position[frows,_?(Between[{n,n+500}]),{1}]]],{n,1,Max[frows],500}];
In[]:=
Length[barData]
Out[]=
21
Histogram[]
In[]:=
Take[outsizes,10]
Out[]=
mp23,wi1,ax-mp1,mp2b2,a1i4,ax-11,2a1i5,mp1i5,a2i4,ax-21
In[]:=
KeyDrop[DeleteMissing[outsizes/@#]&/@GroupBy[metamathAssoc/.{"CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY""logic","ZF (ZERMELO-FRAENKEL) SET THEORY""set theory","SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)"None,"ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY""set theory","TG (TARSKI-GROTHENDIECK) SET THEORY""set theory","REAL AND COMPLEX NUMBERS""numbers","ELEMENTARY NUMBER THEORY""number theory","BASIC STRUCTURES""basic structures","BASIC CATEGORY THEORY""category theory","BASIC ORDER THEORY""order theory","BASIC ALGEBRAIC STRUCTURES""algebra","BASIC LINEAR ALGEBRA""linear algebra","BASIC TOPOLOGY""topology","BASIC REAL AND COMPLEX ANALYSIS""analysis","BASIC REAL AND COMPLEX FUNCTIONS""functional analysis","ELEMENTARY GEOMETRY""geometry","GRAPH THEORY""graph theory","GUIDES AND MISCELLANEA"None},Identity,Keys],None]
Out[]=
In[]:=
KeyDrop[DeleteMissing[outsizes/@#]&/@GroupBy[metamathAssoc/.{"CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY""logic","ZF (ZERMELO-FRAENKEL) SET THEORY""set theory","SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)"None,"ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY""set theory","TG (TARSKI-GROTHENDIECK) SET THEORY""set theory","REAL AND COMPLEX NUMBERS""numbers","ELEMENTARY NUMBER THEORY""numbers","BASIC STRUCTURES""algebra","BASIC CATEGORY THEORY""algebra","BASIC ORDER THEORY""algebra","BASIC ALGEBRAIC STRUCTURES""algebra","BASIC LINEAR ALGEBRA""algebra","BASIC TOPOLOGY""geometry & topology","BASIC REAL AND COMPLEX ANALYSIS""analysis","BASIC REAL AND COMPLEX FUNCTIONS""analysis","ELEMENTARY GEOMETRY""geometry & topology","GRAPH THEORY""basic structures","GUIDES AND MISCELLANEA"None},Identity,Keys],None][[{"set theory","logic","numbers","algebra","analysis","geometry & topology"}]]
Out[]=
Histogram[%,ChartLayout"Stacked",ChartLegendsAutomatic,Frame->True,AspectRatio1/2]
Out[]=
In[]:=
Counts[Values[metamathAssoc]]
Out[]=
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY2380,ZF (ZERMELO-FRAENKEL) SET THEORY6329,SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)10955,ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY242,TG (TARSKI-GROTHENDIECK) SET THEORY155,REAL AND COMPLEX NUMBERS4887,ELEMENTARY NUMBER THEORY760,BASIC STRUCTURES404,BASIC CATEGORY THEORY557,BASIC ORDER THEORY294,BASIC ALGEBRAIC STRUCTURES2662,BASIC LINEAR ALGEBRA601,BASIC TOPOLOGY2338,BASIC REAL AND COMPLEX ANALYSIS587,BASIC REAL AND COMPLEX FUNCTIONS1424,ELEMENTARY GEOMETRY495,GRAPH THEORY799,GUIDES AND MISCELLANEA61
In[]:=
Column[#->&/@DeleteDuplicates[Values[metamathAssoc]]]
In[]:=
"CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY""logic" |
"ZF (ZERMELO-FRAENKEL) SET THEORY""set theory" |
"SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)"None |
"ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY""set theory" |
"TG (TARSKI-GROTHENDIECK) SET THEORY""set theory" |
"REAL AND COMPLEX NUMBERS""numbers" |
"ELEMENTARY NUMBER THEORY""number theory" |
"BASIC STRUCTURES""basic structures" |
"BASIC CATEGORY THEORY""category theory" |
"BASIC ORDER THEORY""order theory" |
"BASIC ALGEBRAIC STRUCTURES""algebra" |
"BASIC LINEAR ALGEBRA""linear algebra" |
"BASIC TOPOLOGY""topology" |
"BASIC REAL AND COMPLEX ANALYSIS""analysis" |
"BASIC REAL AND COMPLEX FUNCTIONS""functional analysis" |
"ELEMENTARY GEOMETRY""geometry" |
"GRAPH THEORY""graph theory" |
"GUIDES AND MISCELLANEA"None |
Out[]=
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITYlogic |
ZF (ZERMELO-FRAENKEL) SET THEORYset theory |
SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)None |
ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORYset theory |
TG (TARSKI-GROTHENDIECK) SET THEORYset theory |
REAL AND COMPLEX NUMBERSnumbers |
ELEMENTARY NUMBER THEORYnumber theory |
BASIC STRUCTURESbasic structures |
BASIC CATEGORY THEORYcategory theory |
BASIC ORDER THEORYorder theory |
BASIC ALGEBRAIC STRUCTURESalgebra |
BASIC LINEAR ALGEBRAlinear algebra |
BASIC TOPOLOGYtopology |
BASIC REAL AND COMPLEX ANALYSISanalysis |
BASIC REAL AND COMPLEX FUNCTIONSfunctional analysis |
ELEMENTARY GEOMETRYgeometry |
GRAPH THEORYgraph theory |
GUIDES AND MISCELLANEANone |