In[]:=
Take[VertexList[metamathGraph],20]
Out[]=
{mp2,wi,ax-mp,mp2b,a1i,ax-1,2a1i,mp1i,a2i,ax-2,mpd,imim2i,syl,3syl,4syl,mpi,mpisyl,id,idALT,idd}
In[]:=
Subgraph[metamathGraph,%]
Out[]=
In[]:=
MatrixPlot[AdjacencyMatrix[%]]
Out[]=
In[]:=
MatrixPlot[AdjacencyMatrix[Subgraph[metamathGraph,Take[VertexList[metamathGraph],50]]]]
Out[]=
In[]:=
MatrixPlot[AdjacencyMatrix[Subgraph[metamathGraph,Take[VertexList[metamathGraph],2000]]]]
Out[]=
In[]:=
Subgraph[metamathGraph,Take[VertexList[metamathGraph],100],GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2]
Out[]=
In[]:=
ReverseGraph[Subgraph[metamathGraph,Take[VertexList[metamathGraph],100],VertexLabels->Placed[Automatic,Tooltip],GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2]]
Out[]=
In[]:=
Select[mm["Axioms"],StringStartsQ["ax-"]]
Out[]=
{ax-mp,ax-1,ax-2,ax-3,ax-gen,ax-4,ax-5,ax-6,ax-7,ax-8,ax-9,ax-10,ax-11,ax-12,ax-13,ax-ext,ax-rep,ax-sep,ax-nul,ax-pow,ax-pr,ax-un,ax-reg,ax-inf,ax-inf2,ax-cc,ax-dc,ax-ac,ax-ac2,ax-groth,ax-cnex,ax-resscn,ax-1cn,ax-icn,ax-addcl,ax-addrcl,ax-mulcl,ax-mulrcl,ax-mulcom,ax-addass,ax-mulass,ax-distr,ax-i2m1,ax-1ne0,ax-1rid,ax-rnegex,ax-rrecex,ax-cnre,ax-pre-lttri,ax-pre-lttrn,ax-pre-ltadd,ax-pre-mulgt0,ax-pre-sup,ax-addf,ax-mulf,ax-hilex,ax-hfvadd,ax-hvcom,ax-hvass,ax-hv0cl,ax-hvaddid,ax-hfvmul,ax-hvmulid,ax-hvmulass,ax-hvdistr1,ax-hvdistr2,ax-hvmul0,ax-hfi,ax-his1,ax-his2,ax-his3,ax-his4,ax-hcompl,ax-xrssca,ax-xrsvsca,ax-hgt749,ax-ros335,ax-ros336,ax-7d,ax-8d,ax-9d1,ax-9d2,ax-10d,ax-11d,ax-prv1,ax-prv2,ax-prv3,ax-luk1,ax-luk2,ax-luk3,ax-wl-13v,ax-wl-11v,ax-wl-8cl,ax-c5,ax-c4,ax-c7,ax-c10,ax-c11,ax-c11n,ax-c15,ax-c9,ax-c14,ax-c16,ax-riotaBAD,ax-frege1,ax-frege2,ax-frege8,ax-frege28,ax-frege31,ax-frege41,ax-frege52a,ax-frege54a,ax-frege58a,ax-frege52c,ax-frege54c,ax-frege58b,ax-bgbltosilva,ax-tgoldbachgt,ax-hgprmladder,ax-bgbltosilvaOLD,ax-hgprmladderOLD,ax-tgoldbachgtOLD}
Axiom Naming
Axiom Naming
Famous Theorems
Famous Theorems