[ Use MetamathImport ]
In[]:=
mm=MetamathImportUncompress@

Out[]=
MetamathObject

Symbols: 1605
Statements: 97142
Data not saved. Save now

In[]:=
DumpSave["mmset-object.mx",mm]
Out[]=

MetamathObject

Symbols: 1605
Statements: 97142
Data not saved. Save now


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[]=
dirith10360,dirith210359,rplogsum10356,dchrmusum10281,dchrvmasum10281
In[]:=
Histogram[Values[outsizes],Frame->True,AspectRatio1/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[]=
mp23,wi1,ax-mp1,mp2b2,a1i4,ax-11,2a1i5,mp1i5,a2i4,ax-21
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[]=
logic{1,1,1,1,1,3,2,4,5,5,4,5,7,8,9,10,8,10,7,6,9,9,10,12,9,9,11,13,14,10,16,15,14,14,15,14,10,12,11,12,12,13,11,12,8,
⋯2192⋯
,532,556,442,527,400,409,91,92,175,176,174,175,155,156,175,177,164,165,166,175,167,176,163,163,156,169,166,165,163,164,48,49,68,40,17,96,154,230,209,80,226,202,331,398,393},
⋯13⋯

large output
show less
show more
show all
set size limit...
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[]=
set theory{1,159,201,203,566,1,192,370,371,466,467,1,204,532,1,206,206,209,209,210,209,214,210,211,216,217,218,218,218,219,220,226,223,
⋯6520⋯
,882,1830,1524,1714,1536,1838,2746,2038,3118,3202,3572,4023,4175,1,539,1704,615,596,1481,2726,2762,3786,3789,517,3908,782,4012,1,1294,1300,1884,1305,1890},
⋯4⋯
,
⋯1⋯

large output
show less
show more
show all
set size limit...
Histogram[%,ChartLayout"Stacked",ChartLegendsAutomatic,Frame->True,AspectRatio1/2]
Out[]=
set theory
logic
numbers
algebra
analysis
geometry & topology
In[]:=
Counts[Values[metamathAssoc]]
Out[]=
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY2380,ZF (ZERMELO-FRAENKEL) SET THEORY6329,SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)10955,ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY242,TG (TARSKI-GROTHENDIECK) SET THEORY155,REAL AND COMPLEX NUMBERS4887,ELEMENTARY NUMBER THEORY760,BASIC STRUCTURES404,BASIC CATEGORY THEORY557,BASIC ORDER THEORY294,BASIC ALGEBRAIC STRUCTURES2662,BASIC LINEAR ALGEBRA601,BASIC TOPOLOGY2338,BASIC REAL AND COMPLEX ANALYSIS587,BASIC REAL AND COMPLEX FUNCTIONS1424,ELEMENTARY GEOMETRY495,GRAPH THEORY799,GUIDES AND MISCELLANEA61
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 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