In[]:=
SetDirectory[NotebookDirectory[]];
In[]:=
mm=
[◼]
MetamathImport
[File["DATA/set.mm"]];//AbsoluteTiming
Out[]=
{36.6201,Null}
In[]:=
tags=Import["DATA/setmm_tags.wxf"]
Out[]=
a1iiCLASSICAL FIRST-ORDER LOGIC WITH EQUALITY/Pre-logic/Inferences for assisting proof development,idiCLASSICAL FIRST-ORDER LOGIC WITH EQUALITY/Pre-logic/Inferences for assisting proof development,ax-mpCLASSICAL FIRST-ORDER LOGIC WITH EQUALITY/Propositional calculus/The axioms of propositional calculus,
⋯41196⋯
,amgmw2dSUPPLEMENTARY MATERIAL (USER'S MATHBOXES)/Mathbox for Kunhao Zheng/Weighted AM-GM Inequality,young2dSUPPLEMENTARY MATERIAL (USER'S MATHBOXES)/Mathbox for Kunhao Zheng/Weighted AM-GM Inequality
large output
show less
show more
show all
set size limit...
In[]:=
metamathAssoc=StringSplit[#,"/"][[1]]&/@tags
Out[]=
a1iiCLASSICAL FIRST-ORDER LOGIC WITH EQUALITY,idiCLASSICAL FIRST-ORDER LOGIC WITH EQUALITY,ax-mpCLASSICAL FIRST-ORDER LOGIC WITH EQUALITY,ax-1CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY,ax-2CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY,ax-3CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY,
⋯41190⋯
,aacllemSUPPLEMENTARY MATERIAL (USER'S MATHBOXES),amgmwlemSUPPLEMENTARY MATERIAL (USER'S MATHBOXES),amgmlemALTSUPPLEMENTARY MATERIAL (USER'S MATHBOXES),amgmw2dSUPPLEMENTARY MATERIAL (USER'S MATHBOXES),young2dSUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
large output
show less
show more
show all
set size limit...
In[]:=
metamathDomains=Union[Values[metamathAssoc]];
In[]:=
metamathInfrastructure={"SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)","GUIDES AND MISCELLANEA",​​"COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)","SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)","COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)"};
In[]:=
dropTheorems=Select[metamathAssoc,MatchQ[Alternatives@@metamathInfrastructure]];
In[]:=
metamathGraph=mm["DependencyGraph"];
In[]:=
mmvars=Cases[mm["Statements"],_[label_,{"wff"|"class"|"setvar",__},___]:>label];
In[]:=
mmgraph=Subgraph[metamathGraph,DeleteCases[VertexList[metamathGraph],Alternatives@@Join[mmvars,Keys@dropTheorems]]]
Out[]=
Graph
Vertex count: 26492
Edge count: 466655

In[]:=
metamathColors=AssociationThread[Complement[metamathDomains,metamathInfrastructure]Take[ColorData[54,"ColorList"],Length[Complement[metamathDomains,metamathInfrastructure]]]];
In[]:=
Graph[TransitiveReductionGraph[Subgraph[mmgraph,VertexOutComponent[mmgraph,"pythag"]]],GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2,EdgeStyleGrayLevel[0.5,0.5],VertexStyle(#{Lighter@Lookup[metamathColors,metamathAssoc[#],LightGray]}&/@VertexList[mmgraph]),VertexSize0.75]
In[]:=
outsizes=Import["DATA/setmm-out-sizes.wxf"];
In[]:=
numberTheorems=Keys@Select[metamathAssoc,MatchQ["REAL AND COMPLEX NUMBERS"|"ELEMENTARY NUMBER THEORY"]];
In[]:=
setmmDescription[name_] := First @ StringCases[​​ Import[StringTemplate["http://us.metamath.org/mpeuni/``.html"] @ name, "Data"][[2]],​​ "Description: " ~~ desc__ ~~ EndOfLine :> desc​​]
In[]:=
degrees=AssociationThread[VertexList[mmgraph],VertexInDegree[mmgraph]];
In[]:=
candidates=TakeLargest[KeySelect[3500<outsizes[#]<4000&]@AssociationMap[degrees,numberTheorems],10]
Out[]=
abscld232,lencl153,absidd98,absge0d87,wrdf85,prmuz273,hash069,absmuld61,absid57,hashsng54
In[]:=
KeyMap[setmmDescription,candidates]
Out[]=
Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)232,The length of a word is a nonnegative integer. This corresponds to the definition in section 9.1 of [ AhoHopUll ] p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015.)153,A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)98,Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)87,A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)85,A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)73,The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)69,Absolute value distributes over multiplication. Proposition 10-3.7(f) of [ Gleason ] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)61,A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)57,The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.)54
In[]:=
mmReport=ResourceDataResourceObject
Name: Metamath Report
»
Type: DataResource
Description: Contributions to the Set.mm database
;
In[]:=
dates=Association@Normal[Rule@@@Values@mmReport[All,{"Label","Date"}]];
In[]:=
AssociationMap[dates,Keys@candidates]
Out[]=
abscld
Sun 29 May 2016
,lencl
Thu 27 Aug 2015
,absidd
Sun 29 May 2016
,absge0d
Sun 29 May 2016
,wrdf
Sat 15 Aug 2015
,prmuz2
Sat 17 Nov 2012
,hash0
Tue 8 Jul 2014
,absmuld
Sun 29 May 2016
,absid
Sun 29 May 2016
,hashsng
Wed 13 Feb 2013

In[]:=
metamathSections=DeleteCases[None]@ReplaceAll[{​​"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""abstract structures","GUIDES AND MISCELLANEA"None}]@DeleteCases[Alternatives@@metamathInfrastructure]@metamathAssoc;
In[]:=
(*keys=Union@Values[metamathSections];*)​​keys={"logic","set theory","numbers","algebra","geometry & topology","analysis","abstract structures"}
Out[]=
{logic,set theory,numbers,algebra,geometry & topology,analysis,abstract structures}
In[]:=
data=Counts/@KeySort@GroupBy[Values@Merge[KeyIntersection[{DateObject[#,"Year"]&/@dates,metamathSections}],Identity],First,Map@Last];
In[]:=
Min@dates
Out[]=
Wed 30 Sep 1992
In[]:=
BarChart[​​<|AssociationThread[keys,0],#|>&/@data,​​ChartLayout"Stacked",​​ChartStyle"Pastel",​​ChartLegendsSwatchLegend["Pastel",keys],​​Frame->True,​​FrameTicks{{Automatic,None},{MapIndexed[{First[#2],DateValue[#1,"YearShort"]}&,Keys[data]],None}}​​]
Out[]=
set theory
numbers
logic
geometry & topology
basic structures
analysis
algebra
Coloring