In[]:=

SetDirectory[NotebookDirectory[]]

Out[]=

/Users/sw/Dropbox/Physics/WorkingMaterial/2022

In[]:=

metamathGraph=CloudGet["https://wolfr.am/PLbmdhRv"];

In[]:=

metamathAssoc=CloudGet["https://wolfr.am/PLborw8R"];

In[]:=

metamathDomains=Union[Values[metamathAssoc]];

In[]:=

metamathInfrastructure={"SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)","GUIDES AND MISCELLANEA"};

(*setmm=ResourceFunction["MetamathImport"][URL["https://raw.githubusercontent.com/metamath/set.mm/master/set.mm"]];*)

(*"DATA/setmm-basic.wxf"*)

In[]:=

setmm=Import["DATA/setmm-basic.wxf"];

In[]:=

defassoc=KeySelect[setmm["Statements"],StringStartsQ["df-"]];

In[]:=

axiomassoc=KeySelect[setmm["Statements"],StringStartsQ["ax-"]];

In[]:=

RulesFromDefs[("Axiom"|"EssentialHypothesis")[_,x_List,___]]:=With[{xx=DeleteCases[DeleteCases[x,Alternatives@@mmvars],"("|")"|""|"{"|"}"]},Thread[xx[[2]]->Drop[xx,2]]]

In[]:=

mmvars=Keys[Select[setmm["Symbols"],Head[#]==="Variable"&]];

In[]:=

mmconsts=Keys[Select[setmm["Symbols"],Head[#]==="Constant"&]];

In[]:=

famous=Select[{{"The Irrationality of the Square Root of 2","sqrt2irr"},{"The Fundamental Theorem of Algebra","fta"},{"The Denumerability of the Rational Numbers","qnnen"},{"Pythagorean Theorem","pythag"},{"The Prime Number Theorem","pnt"},{"Law of Quadratic Reciprocity","lgsquad"},{"The Area of a Circle","areacirc"},{"Euler's Generalization of Fermat's Little Theorem","eulerth"},{"The Infinitude of Primes","infpn2"},{"Euler's Summation of 1 +","1/2)^2 + (1/3)^2 + .... (basel"},{"The Fundamental Theorem of Integral Calculus","ftc1 and ftc2"},{"De Moivre's Theorem","demoivreALT"},{"Liouville's Theorem and the Construction of Transcendental Numbers","aaliou"},{"Four Squares Theorem","4sq"},{"All Primes","1 mod 4) Equal the Sum of Two Squares (2sq"},{"The Non-Denumerability of the Continuum","ruc"},{"Formula for Pythagorean Triples","pythagtrip"},{"Schroeder-Bernstein Theorem","sbth"},{"Leibniz' Series for Pi","leibpi"},{"Sum of the Angles of a Triangle","ang180"},{"The Ballot Problem","aka Bertrand's ballot problem) (ballotth"},{"Ramsey's Theorem","ramsey"},{"Divergence of the Harmonic Series","harmonic"},{"Taylor's Theorem","taylth"},{"The Solution of a Cubic","cubic"},{"Arithmetic Mean/Geometric Mean","amgm"},{"Solutions to Pell's Equation","rmxycomplete"},{"Sum of the Reciprocals of the Triangular Numbers","trirecip"},{"The Binomial Theorem","binom"},{"The Partition Theorem","by Euler) (eulerpart"},{"The Solution of the General Quartic Equation","quart"},{"Dirichlet's Theorem","dirith"},{"The Cayley-Hamilton Theorem","cayleyhamilton"},{"Wilson's Theorem","wilth"},{"The Number of Subsets of a Set","pw2en"},{"The Konigsberg Bridge Problem","konigsberg"},{"Product of Segments of Chords","chordthm by David Moews"},{"Heron's Formula","heron by Mario Carneiro based on work by Jon Pennant and Thierry Arnoux"},{"Formula for the Number of Combinations","hashbc"},{"Bezout's Theorem","bezout"},{"Theorem of Ceva","cevath"},{"Cantor's Theorem","canth2"},{"L'Hôpital's Rule","lhop"},{"Isosceles Triangle Theorem","isosctr"},{"Sum of a Geometric Series","geoser"},{"e is Transcendental","etransc"},{"Sum of an arithmetic series","arisum"},{"Greatest Common Divisor Algorithm","eucalg"},{"The Perfect Number Theorem","perfect"},{"Order of a Subgroup","lagsubg"},{"Sylow's Theorem","sylow1 and sylow2 and sylow2b and sylow3"},{"Ascending or Descending Sequences","erdsze and erdsze2"},{"The Mean Value Theorem","mvth"},{"Fourier Series","fourier"},{"Sum of kth powers","fsumkthpow"},{"The Cauchy-Schwarz Inequality","sii"},{"The Intermediate Value Theorem","ivth"},{"Fundamental Theorem of Arithmetic","1arith2"},{"Erdős's proof of the divergence of the inverse prime series","prmrec"},{"The Friendship Theorem","friendship"},{"Divisibility by 3 Rule","3dvds"},{"Lebesgue Measure and Integration","itgcl"},{"Desargues's Theorem","dath"},{"Derangements Formula","derangfmla and subfaclim"},{"The Factor and Remainder Theorems","facth and plyrem"},{"Stirling's Formula","stirling by Glauco Siliprandi"},{"The Triangle Inequality","abstrii"},{"The Birthday Problem","birthday"},{"The Law of Cosines","lawcos"},{"Ptolemy's Theorem","ptolemy"},{"Principle of Inclusion/Exclusion","incexc"},{"Cramer's Rule","cramer"},{"Bertrand's Postulate","bpos"}},Length[VertexOutComponent[metamathGraph,Last[#]]]>2&];//Quiet

In[]:=

Length[%]

Out[]=

60

Derived below:

In[]:=

usedaxioms={"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-inf2","ax-cc","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"};

In[]:=

axiomnames=Association[#1->First[#2]&@@@{"ax-mp"{"modus ponens"},"ax-1"{"axiom of simplification"},"ax-2"{"Frege's axiom"},"ax-3"{"principle of transposition"},"ax-gen"{"rule of generalization"},"ax-4"{"axiom of quantified implication"},"ax-5"{"Axiom of Distinctness"},"ax-6"{"Axiom of Existence"},"ax-7"{"Axiom of Equality"},"ax-8"{"Axiom of Left Equality for Binary Predicate"},"ax-9"{"Axiom of Right Equality for Binary Predicate"},"ax-10"{"Axiom of Quantified Negation"},"ax-11"{"Axiom of Quantifier Commutation"},"ax-12"{"Axiom of Substitution"},"ax-13"{"Axiom of Quantified Equality"},"ax-ext"{"Axiom of Extensionality"},"ax-rep"{"Axiom of Replacement"},"ax-sep"{"Axiom of Separation"},"ax-nul"{"The Null Set Axiom"},"ax-pow"{"Axiom of Power Sets"},"ax-pr"{"Axiom of Pairing"},"ax-un"{"Axiom of Union"},"ax-inf2"{"Axiom of Infinity"},"ax-cc"{"Axiom of Countable choice"},"ax-cnex"{"Complex numbers form a set"},"ax-resscn"{"Real numbers are subset complex"},"ax-1cn"{"1 is a complex number"},"ax-icn"{"i is a complex number"},"ax-addcl"{"Closure for complex addition"},"ax-addrcl"{"Closure for real addition"},"ax-mulcl"{"Closure for complex multiplication"},"ax-mulrcl"{"Closure for real multiplication"},"ax-mulcom"{"Commutativity of complex multiplication"},"ax-addass"{"Associativity of complex addition"},"ax-mulass"{"Associativity of complex multiplication"},"ax-distr"{"Distributivity for complex numbers"},"ax-i2m1"{"i-squared equals -1"},"ax-1ne0"{"1 and 0 are distinct"},"ax-1rid"{"1 is identity for real multiplication"},"ax-rnegex"{"Existence of negative of real number"},"ax-rrecex"{"Existence of reciprocal of nonzero real number"},"ax-cnre"{"Complex numbers can be expressed in terms of two reals"},"ax-pre-lttri"{"Ordering on reals satisfies strict trichotomy"},"ax-pre-lttrn"{"Ordering on reals is transitive"},"ax-pre-ltadd"{"Ordering property of addition on reals"},"ax-pre-mulgt0"{"Product of two positive reals is positive"},"ax-pre-sup"{"Nonempty bounded-above set of reals has supremum"},"ax-addf"{"Addition is an operation on complex numbers"},"ax-mulf"{"Multiplication is an operation on complex numbers"}}];

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

In[]:=

Text[Grid[Flatten/@({#1,Length[VertexOutComponent[metamathGraph,#2]],{Length[#],Length[Select[#,StringStartsQ["ax-"]]],Length[Select[#,StringStartsQ["df-"]]]}&[With[{g=VertexOutComponentGraph[metamathGraph,#2]},Select[VertexList[g],VertexOutDegree[g,#]==0&]]]}&@@@famous),Frame->All]]

Out[]=

The Irrationality of the Square Root of 2 | 3723 | 152 | 44 | 108 |

The Fundamental Theorem of Algebra | 7368 | 286 | 48 | 238 |

The Denumerability of the Rational Numbers | 3842 | 153 | 45 | 108 |

Pythagorean Theorem | 7099 | 279 | 48 | 231 |

The Prime Number Theorem | 8292 | 295 | 48 | 247 |

Law of Quadratic Reciprocity | 6292 | 261 | 48 | 213 |

The Area of a Circle | 8279 | 296 | 48 | 248 |

Euler's Generalization of Fermat's Little Theorem | 4340 | 166 | 45 | 121 |

The Infinitude of Primes | 3300 | 143 | 45 | 98 |

De Moivre's Theorem | 5070 | 180 | 48 | 132 |

Liouville's Theorem and the Construction of Transcendental Numbers | 7003 | 285 | 48 | 237 |

Four Squares Theorem | 4576 | 168 | 45 | 123 |

The Non-Denumerability of the Continuum | 3412 | 146 | 45 | 101 |

Formula for Pythagorean Triples | 4202 | 163 | 44 | 119 |

Schroeder-Bernstein Theorem | 1411 | 70 | 21 | 49 |

Leibniz' Series for Pi | 7694 | 285 | 48 | 237 |

Sum of the Angles of a Triangle | 7123 | 279 | 48 | 231 |

Ramsey's Theorem | 4783 | 174 | 46 | 128 |

Divergence of the Harmonic Series | 4747 | 172 | 46 | 126 |

Taylor's Theorem | 7080 | 296 | 48 | 248 |

The Solution of a Cubic | 7320 | 281 | 48 | 233 |

Arithmetic Mean/Geometric Mean | 7576 | 301 | 48 | 253 |

Solutions to Pell's Equation | 7707 | 292 | 48 | 244 |

Sum of the Reciprocals of the Triangular Numbers | 4537 | 171 | 46 | 125 |

The Binomial Theorem | 4421 | 169 | 46 | 123 |

The Solution of the General Quartic Equation | 7292 | 281 | 48 | 233 |

Dirichlet's Theorem | 9814 | 359 | 48 | 311 |

The Cayley-Hamilton Theorem | 6510 | 278 | 47 | 231 |

Wilson's Theorem | 5393 | 222 | 48 | 174 |

The Number of Subsets of a Set | 1669 | 80 | 21 | 59 |

The Konigsberg Bridge Problem | 4504 | 176 | 45 | 131 |

Formula for the Number of Combinations | 3857 | 154 | 44 | 110 |

Bezout's Theorem | 3739 | 154 | 44 | 110 |

Theorem of Ceva | 2580 | 120 | 42 | 78 |

Cantor's Theorem | 1653 | 76 | 21 | 55 |

L'Hôpital's Rule | 6333 | 265 | 48 | 217 |

Isosceles Triangle Theorem | 7137 | 279 | 48 | 231 |

Sum of a Geometric Series | 4360 | 167 | 46 | 121 |

e is Transcendental | 8797 | 306 | 49 | 256 |

Sum of an arithmetic series | 4444 | 169 | 46 | 123 |

Greatest Common Divisor Algorithm | 3848 | 156 | 44 | 112 |

The Perfect Number Theorem | 7401 | 285 | 48 | 237 |

Order of a Subgroup | 4631 | 187 | 46 | 141 |

The Mean Value Theorem | 6273 | 264 | 48 | 216 |

Fourier Series | 8719 | 294 | 49 | 245 |

Sum of kth powers | 4594 | 170 | 46 | 124 |

The Intermediate Value Theorem | 3689 | 155 | 44 | 111 |

Fundamental Theorem of Arithmetic | 4414 | 167 | 45 | 122 |

Erdős's proof of the divergence of the inverse prime series | 5229 | 179 | 46 | 133 |

The Friendship Theorem | 6330 | 211 | 46 | 165 |

Divisibility by 3 Rule | 4457 | 175 | 46 | 129 |

Lebesgue Measure and Integration | 4417 | 172 | 46 | 126 |

Desargues's Theorem | 2636 | 102 | 22 | 80 |

The Triangle Inequality | 3535 | 150 | 44 | 106 |

The Birthday Problem | 7819 | 284 | 48 | 236 |

The Law of Cosines | 7097 | 279 | 48 | 231 |

Ptolemy's Theorem | 6927 | 277 | 48 | 229 |

Principle of Inclusion/Exclusion | 4546 | 170 | 46 | 124 |

Cramer's Rule | 6160 | 266 | 47 | 219 |

Bertrand's Postulate | 7760 | 287 | 48 | 239 |

NOTE: could also figure out the deepest one has to go to reach an axiom

inf2: http://us.metamath.org/mpeuni/ax-inf2.html [axiom of infinity]

http://us.metamath.org/mpeuni/ax-cc.html [countable choice]

#### [ want to do same from all theorems ]

[ want to do same from all theorems ]

### Pythagorean theorem

Pythagorean theorem

#### How many copies of each axiom are there in the Pythagorean theorem?

How many copies of each axiom are there in the Pythagorean theorem?

[[ to do ]]

#### [[ Also look at this in Euclid ]]

[[ Also look at this in Euclid ]]

### Distance from all nodes to a particular axiom

Distance from all nodes to a particular axiom

## Full Metamath set.mm Graph

Full Metamath set.mm Graph

## pythag vs. pythi [[ probably not interesting; different spaces being used ]]

pythag vs. pythi [[ probably not interesting; different spaces being used ]]

## Definitions

Definitions