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"};
In[]:=
(*setmm=ResourceFunction["MetamathImport"][URL["https://raw.githubusercontent.com/metamath/set.mm/master/set.mm"]];*)
In[]:=
(*"DATA/setmm-basic.wxf"*)
In[]:=
setmm=Import["DATA/setmm-basic.wxf"];
In[]:=
metamathGraph=Graph[Flatten@KeyValueMap[{label,thm}Map[label#&,TakeWhile[Rest@thm〚-1〛,#=!=")"&]],Select[setmm["Statements"],MatchQ["Theorem"[__]]]]];
In[]:=
metamathGraph
Out[]=
Graph
Vertex count: 42127
Edge count: 1303436

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[VertexQ[metamathGraph,#[[2]]]&]@Flatten[StringCases[Import["http://us.metamath.org/mm_100.html","Data"][[2]],DigitCharacter..~~" . "~~descr__~~" ( "~~label:WordCharacter..~~__:>{descr,label}],1];
In[]:=
Length[famous]
Out[]=
74
[ 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
3948
293
44
108
The Fundamental Theorem of Algebra
7800
566
48
238
The Denumerability of the Rational Numbers
4078
296
45
108
Pythagorean Theorem
4901
352
48
135
The Prime Number Theorem
8735
586
48
247
Law of Quadratic Reciprocity
6678
518
48
213
The Area of a Circle
8716
586
48
248
Euler's Generalization of Fermat's Little Theorem
4616
323
45
122
The Infinitude of Primes
3518
274
45
98
Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + ....
7775
564
48
237
The Fundamental Theorem of Integral Calculus
7582
537
49
223
De Moivre's Theorem
5374
349
48
133
Liouville's Theorem and the Construction of Transcendental Numbers
7431
563
48
237
Four Squares Theorem
4847
329
45
124
All Primes (1 mod 4) Equal the Sum of Two Squares
7508
580
48
242
The Non-Denumerability of the Continuum
3635
280
45
101
Formula for Pythagorean Triples
4471
319
44
120
Schroeder-Bernstein Theorem
1536
131
21
48
Leibniz' Series for Pi
8121
564
48
237
Sum of the Angles of a Triangle
7546
552
48
231
The Ballot Problem (aka Bertrand's ballot problem)
4436
304
44
113
Ramsey's Theorem
5061
339
46
129
Divergence of the Harmonic Series
5018
334
46
127
Taylor's Theorem
7515
585
48
248
The Solution of a Cubic
7743
556
48
233
Arithmetic Mean/Geometric Mean
8019
595
48
253
Solutions to Pell's Equation
8152
579
48
244
Sum of the Reciprocals of the Triangular Numbers
4813
332
46
126
The Binomial Theorem
4668
326
46
123
The Partition Theorem (by Euler)
5725
358
47
136
The Solution of the General Quartic Equation
7714
556
48
233
Dirichlet's Theorem
10324
713
48
311
The Cayley-Hamilton Theorem
6806
552
47
229
Wilson's Theorem
5737
438
48
174
The Number of Subsets of a Set
1813
156
21
59
The Konigsberg Bridge Problem
4770
346
45
132
Product of Segments of Chords
7612
552
48
231
Heron's Formula
7536
552
48
231
Formula for the Number of Combinations
4092
297
44
110
Bezout's Theorem
3996
300
44
111
Theorem of Ceva
2758
227
42
78
Cantor's Theorem
1787
144
21
55
L'Hôpital's Rule
6737
524
48
217
Isosceles Triangle Theorem
7560
552
48
231
Sum of a Geometric Series
4605
322
46
121
e is Transcendental
9244
606
49
256
Sum of an arithmetic series
4691
326
46
123
Greatest Common Divisor Algorithm
4107
304
44
113
The Perfect Number Theorem
7833
565
48
237
Order of a Subgroup
4903
365
46
141
Sylow's Theorem
5609
388
46
152
Ascending or Descending Sequences
4041
292
45
107
The Principle of Mathematical Induction
1591
126
20
47
The Mean Value Theorem
6676
522
48
216
Fourier Series
9160
582
49
245
Sum of kth powers
4846
329
46
124
The Cauchy-Schwarz Inequality
6776
532
48
221
The Intermediate Value Theorem
3919
299
44
111
Fundamental Theorem of Arithmetic
4682
327
45
123
Erdős's proof of the divergence of the inverse prime series
5516
352
46
134
The Friendship Theorem
6672
417
46
166
Divisibility by 3 Rule
4715
338
46
129
Lebesgue Measure and Integration
4697
336
46
127
Desargues's Theorem
2818
209
22
80
Derangements Formula
5708
359
48
137
The Factor and Remainder Theorems
5173
349
47
133
Stirling's Formula
9007
589
49
249
The Triangle Inequality
3759
289
44
106
The Birthday Problem
8251
562
48
236
The Law of Cosines
7520
552
48
231
Ptolemy's Theorem
7352
548
48
229
Principle of Inclusion/Exclusion
4795
328
46
124
Cramer's Rule
6432
526
47
217
Bertrand's Postulate
8195
570
48
239
NOTE: could also figure out the deepest one has to go to reach an axiom
In[]:=
axiomdeps=(Function[thm,thm[[1]]->Select[#,StringStartsQ["ax-"]]&[With[{g=VertexOutComponentGraph[metamathGraph,thm[[2]]]},Select[VertexList[g],VertexOutDegree[g,#]==0&]]]]/@famous);
In[]:=
usedaxioms=Union@@axiomdeps[[All,2]];
In[]:=
Length@usedaxioms
Out[]=
50
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"},​​"ax-ac2"->{"Axiom of Choice"}}];
inf2: http://us.metamath.org/mpeuni/ax-inf2.html [axiom of infinity]
http://us.metamath.org/mpeuni/ax-cc.html [countable choice]
http://us.metamath.org/mpeuni/ax-ac2.html [AC]

[ 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