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 ]

Pythagorean theorem

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

[[ to do ]]

[[ Also look at this in Euclid ]]

Distance from all nodes to a particular axiom

Full Metamath set.mm Graph

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

Definitions