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
In[]:=
SetDirectory[NotebookDirectory[]];
In[]:=
mm=[File["DATA/set.mm"]];//AbsoluteTiming
Out[]=
{36.6201,Null}
In[]:=
tags=Import["DATA/setmm_tags.wxf"]
Out[]=
In[]:=
metamathAssoc=StringSplit[#,"/"][[1]]&/@tags
Out[]=
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
In[]:=
metamathColors=AssociationThread[Complement[metamathDomains,metamathInfrastructure]Take[ColorData[54,"ColorList"],Length[Complement[metamathDomains,metamathInfrastructure]]]];
In[]:=
Graph[TransitiveReductionGraph[Subgraph[mmgraph,VertexOutComponent[mmgraph,"pythag"]]],GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2,EdgeStyleGrayLevel[0.5,0.5],VertexStyle(#{Lighter@Lookup[metamathColors,metamathAssoc[#],LightGray]}&/@VertexList[mmgraph]),VertexSize0.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[]=
abscld232,lencl153,absidd98,absge0d87,wrdf85,prmuz273,hash069,absmuld61,absid57,hashsng54
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=ResourceDataResourceObject;
In[]:=
dates=Association@Normal[Rule@@@Values@mmReport[All,{"Label","Date"}]];
In[]:=
AssociationMap[dates,Keys@candidates]
Out[]=
abscld,lencl,absidd,absge0d,wrdf,prmuz2,hash0,absmuld,absid,hashsng
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[]=
In[]:=
BarChart[<|AssociationThread[keys,0],#|>&/@data,ChartLayout"Stacked",ChartStyle"Pastel",ChartLegendsSwatchLegend["Pastel",keys],Frame->True,FrameTicks{{Automatic,None},{MapIndexed[{First[#2],DateValue[#1,"YearShort"]}&,Keys[data]],None}}]
Out[]=
Coloring