Out[]=
Out[]=
In[]:=
VertexCount[metamathGraph]
Out[]=
42279
In[]:=
pythgraph=VertexOutComponentGraph[metamathGraph,"pythag"];
In[]:=
Select[VertexList[pythgraph],StringStartsQ["ax-"|"df-"]]
Out[]=
{df-fv,ax-mp,df-ne,ax-icn,df-3an,df-br,ax-1cn,ax-1,ax-resscn,df-or,df-ov,df-sub,ax-mulcl,ax-addcl,df-an,ax-mulcom,df-neg,df-cos,df-re,df-pr,df-clel,ax-5,df-iota,df-2,ax-1ne0,ax-rnegex,ax-rrecex,df-4,ax-2,df-riota,df-rab,df-reu,df-abs,ax-i2m1,df-bi,ax-mulrcl,ax-addass,ax-distr,df-div,df-seq,df-ef,df-log,df-un,df-sn,df-op,df-pi,ax-addrcl,ax-cnre,df-3,df-xr,df-ioc,df-mnf,df-pnf,ax-pre-mulgt0,df-sin,df-cleq,df-eu,df-sbc,df-ral,df-rex,df-sqrt,df-nel,df-cj,ax-mulass,ax-1rid,df-dif,df-im,df-uz,df-rdg,df-fac,df-nn,df-ima,df-mpt,df-v,df-rp,ax-gen,df-if,df-clab,df-ioo,ax-pre-lttri,df-pw,df-le,ax-cnex,df-3or,df-ltxr,ax-ext,ax-4,ax-nul,df-rmo,df-in,df-n0,df-f1o,df-f1,df-f,df-z,df-sum,ax-inf2,df-ss,df-fn,df-exp,df-clim,df-mo,df-res,df-fo,df-rn,df-nfc,df-nf,df-uni,df-9,df-icc,df-tru,df-inf,df-ex,ax-pre-lttrn,ax-sep,ax-pow,df-cnv,df-6,df-5,ax-3,df-nul,df-sb,ax-pre-ltadd,df-suc,df-lim,df-rel,df-fun,df-opab,df-xp,df-id,df-co,df-mod,df-bc,df-cncf,df-csb,df-8,df-so,ax-un,ax-6,ax-7,df-dm,df-fl,df-ord,df-tr,df-om,ax-11,df-fz,df-recs,df-2nd,df-dv,df-cnfld,df-topsp,df-rest,df-topon,df-7,ax-mulf,df-mpt2,df-po,df-sup,ax-12,ax-13,ax-pr,df-shft,df-fzo,df-fin,df-en,df-isom,df-wrecs,df-we,ax-rep,ax-10,df-pss,df-iun,ax-addf,df-of,df-base,df-tp,df-map,ax-pre-sup,df-sdom,ax-9,df-oprab,df-er,df-rlim,df-hash,df-on,df-fr,df-eprel,df-mopn,df-tset,df-tx,df-limc,df-cn,df-cnp,df-ple,df-ds,df-unif,df-top,df-dom,df-card,df-se,df-pred,df-1o,df-met,df-xmet,df-topn,df-pm,df-ntr,df-ms,df-xms,df-dec,df-starv,df-ndx,df-slot,df-struct,df-bases,df-fi,ax-8,df-fal,df-oi,df-1st,df-xadd,df-xps,df-2o,df-perf,df-iin,df-int,df-cls,df-plusg,df-mulr,df-topgen,df-limsup,df-bl,df-tms,df-imas,df-q,df-ico,df-psmet,df-pt,df-qtop,df-ixp,df-lp,df-haus,df-flf,df-cld,df-xneg,df-oadd,df-prds,df-hom,df-cda,df-sets,df-sca,df-vsca,df-ip,df-hmeo,df-xrs,df-xmul,df-flim,df-fil,df-fm,df-cmn,df-fsupp,df-fbas,df-nei,df-fg,df-cco,df-gsum,df-ress,df-0g,df-mnd,df-supp,df-mgm,df-sgrp,df-cntz,df-mulg,df-submnd,df-acs,df-mrc,df-mre}
In[]:=
Select[VertexList[pythgraph],StringStartsQ["ax-"]]
Out[]=
{ax-mp,ax-icn,ax-1cn,ax-1,ax-resscn,ax-mulcl,ax-addcl,ax-mulcom,ax-5,ax-1ne0,ax-rnegex,ax-rrecex,ax-2,ax-i2m1,ax-mulrcl,ax-addass,ax-distr,ax-addrcl,ax-cnre,ax-pre-mulgt0,ax-mulass,ax-1rid,ax-gen,ax-pre-lttri,ax-cnex,ax-ext,ax-4,ax-nul,ax-inf2,ax-pre-lttrn,ax-sep,ax-pow,ax-3,ax-pre-ltadd,ax-un,ax-6,ax-7,ax-11,ax-mulf,ax-12,ax-13,ax-pr,ax-rep,ax-10,ax-addf,ax-pre-sup,ax-9,ax-8}
In[]:=
Length[%]
Out[]=
48
In[]:=
Length[Select[VertexList[pythgraph],StringStartsQ["df-"]]]
Out[]=
231
In[]:=
VertexDelete[pythgraph,Select[VertexList[pythgraph],StringStartsQ["df-"]]]
Out[]=
Graph
Vertex count: 7316
Edge count: 121216

In[]:=
mmtf=ResourceFunction["https://www.wolframcloud.com/obj/nikm/DeployedResources/Function/MetamathImport"]["TheoremFields"];
Out[]=
$Aborted
In[]:=
metamathGraph=CloudGet["https://wolfr.am/PLbmdhRv"];
In[]:=
VertexCount[metamathGraph]
Out[]=
35241
In[]:=
metamathAssoc=CloudGet["https://wolfr.am/PLborw8R"];
In[]:=
Length[metamathAssoc]
Out[]=
35930
In[]:=
mmg=Import["/Users/sw/Dropbox/Physics/WorkingMaterial/2022/DATA/setmm-graph.wxf"];
Out[]=
$Aborted
In[]:=
metamathDomains=Union[Values[metamathAssoc]];
In[]:=
metamathInfrastructure={"SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)","GUIDES AND MISCELLANEA"};
In[]:=
metamathColors=Merge[{AssociationThread[Complement[metamathDomains,metamathInfrastructure]Take[ColorData[54,"ColorList"],Length[Complement[metamathDomains,metamathInfrastructure]]]],AssociationThread[metamathInfrastructureLightGray]},Identity];
In[]:=
Legended[Subgraph[metamathGraph,VertexOutComponent[metamathGraph,"pythag",1],GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2,VertexLabelsNone,EdgeStyleGrayLevel[0.5,0.5],VertexStyle(#{Lighter/@metamathColors[metamathAssoc[#]]}&/@VertexList[metamathGraph]),VertexSize0.75],SwatchLegend[Lighter/@Flatten[metamathColors[#]&/@{"BASIC REAL AND COMPLEX FUNCTIONS","CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY","REAL AND COMPLEX NUMBERS","ZF (ZERMELO-FRAENKEL) SET THEORY"}][[{2,4,3,1}]],{"real & complex functions","logic","real & complex numbers","set theory"}[[{2,4,3,1}]]]]
Out[]=
logic
set theory
real & complex numbers
real & complex functions

Previous Version

Pythag

Whole-theorem direct dependency theorem dependency

[[ probably rather boring ]]

Full whole-theorem dependency

Inside-statements dependency graph

Whole graph

Color code this graph....

Famous theorems

[ total theorems on which it depends | total “sources” | total distinct axioms | total distinct definitions ]