Towards a Science of Metamathematics
One of the many surprising things about our Wolfram Physics Project is that it seems to have implications even beyond physics. In our effort to develop a fundamental theory of physics it seems as if the tower of ideas and formalism that we’ve ended up inventing are actually quite general, and potentially applicable to all sorts of areas.
One area about which I’ve been particularly excited of late is metamathematics—where it’s looking as if it may be possible to use our formalism to make what might be thought of as a “bulk theory of metamathematics”.
Mathematics itself is about what we establish about mathematical systems. Metamathematics is about the infrastructure of how we get there—the structure of proofs, the network of theorems, and so on. And what I’m hoping is that we’re going to be able to make an overall theory of how that has to work: a formal theory of the large-scale structure of metamathematics—that, among other things, can make statements about the general properties of “metamathematical space”.
Like with physical space, however, there’s not just pure underlying “geometry” to study. There’s also actual “geography”: in our human efforts to do mathematics over the last few millennia, where in metamathematical space have we gone, and “colonized”? There’ve been a few million mathematical theorems explicitly published in the history of human mathematics. What does the “empirical metamathematics” of them reveal? Some of it presumably reflects historical accidents, but some may instead reflect general features of metamathematics and metamathematical space.
I’ve wondered about empirical metamathematics for a long time, and tucked away on page 1176 at the end of the Notes for the section about “Implications for Mathematics and Its Foundations” in A New Kind of Science is something I wrote more than 20 years ago about it:
This note is mostly about what a descriptive theory of empirical metamathematics might be like—for example characterizing what one might mean by a powerful theorem, a deep theorem, a surprising theorem and so on. But at the end of the note is a graph: an actual piece of quantitative empirical metamathematics, based on the best-known structured piece of mathematics in history—Euclid’s Elements.
The graph shows relationships between theorems in the Elements: a kind of causal graph of how different theorems make use of each other. As presented in A New Kind of Science, it’s a small “footnote item” that doesn’t look like much. But for more than 20 years, I’ve kept wondering what more there might be to learn from it. And now that I’m trying to make a general theory of metamathematics, it seemed like it was a good time to try to find out…
The Most Famous Math Book in History
Euclid’s Elements is an impressive achievement. Written in Greek around 300 BC (though presumably including many earlier results), the Elements in effect defined the way formal mathematics is done for more than two thousand years. The basic idea is to start from certain axioms that are assumed to be true, then—without any further “input from outside”—use purely deductive methods to establish a collection of theorems.
Euclid effectively had 10 axioms (5 “postulates” and 5 “common notions”), like “one can draw a straight line from any point to any other point”, or “things which equal the same thing are also equal to one another”. (One of his axioms was his fifth postulate—that parallel lines never meet—which might seem obvious, but which actually turns out not to be true for physical curved space in our universe.)
On the basis of his axioms, Euclid then gave 465 theorems. Many were about 2D and 3D geometry; some were about arithmetic and numbers. Among them were many famous results, like the Pythagorean theorem, the triangle inequality, the fact that there are five Platonic solids, the irrationality of 
and the fact that there are an infinite number of primes. But certainly not all of them are famous—and some seem to us now pretty obscure. And in what has remained a (sometimes frustrating) tradition of pure mathematics for more than two thousand years, Euclid never gives any narrative about why he’s choosing the theorems he does, out of all the infinitely many possibilities.
We don’t have any original Euclids, but versions from a few centuries later exist. They’re written in Greek, with each theorem explained in words, usually by referring to a diagram. Mathematical notation didn’t really start getting invented until the 1400s or so (i.e. a millennium and a half later)—and even the notation for numbers in Euclid’s time was pretty unwieldy. But Euclid had basically modern-looking diagrams, and he even labeled points and angles with (Greek) letters—despite the fact that the idea of variables standing for numbers wouldn’t be invented until the end of the 1500s.
There’s a stylized—almost “legalistic”—way that Euclid states his theorems. And so far as we can tell, in the original version, all that was done was to state theorems; there was no explanation for why a theorem might be true—no proof offered. But it didn’t take long before people started filling in proofs, and there was soon a standard set of proofs, in which each particular theorem was built up from others—and ultimately from the axioms.
There’ve been more than a thousand editions of Euclid printed (probably more than any other book except the Bible), and reading Euclid was until quite recently part of any serious education. (At Eton—where I went to high school—it was only in the 1960s that learning “mathematics” began to mean much other than reading Euclid, in the original Greek of course.) Here’s an edition of Euclid from the 1800s that I happen to own, with the proof of every theorem giving little references to other theorems that are used:
But so what about the metamathematics of Euclid? Given all those theorems—and proofs—can we map out the structure of what Euclid did? That’s what the graph in A New Kind of Science was about. A few years ago, we put the data for that graph into our Wolfram Data Repository—and I looked at it again, but nothing immediately seemed to jump out about it; it still just seemed like a complicated mess:
What else happened? One thing is that we added automated theorem proving to Mathematica and the Wolfram Language. Enter a potential theorem, and axioms from which to derive it, and FindEquationalProof will try to generate a proof. This works well for “structurally simple” mathematical systems (like basic logic), and indeed one can generate proofs with complex networks of lemmas that go significantly beyond what humans can do (or readily understand):
✕
FindEquationalProof[p\[CenterDot]q == q\[CenterDot]p, \!\(
\*SubscriptBox[\(\[ForAll]\), \({a, b,
c}\)]\(\((\((a\[CenterDot]b)\)\[CenterDot]c)\)\[CenterDot]\((a\
\[CenterDot]\((\((a\[CenterDot]c)\)\[CenterDot]a)\))\) ==
c\)\)]["ProofGraph"]
|
It’s in principle possible to use these methods to prove theorems in Euclidean geometry too. But it’s a different problem to make the proofs readily understandable to humans (like the step-by-step solutions of Wolfram|Alpha). So at least for now—even after 2000 years—the most effective source of information about the empirical metamathematics of proofs of Euclid’s theorems is still basically going to be Euclid’s Elements.
But when it comes to representing Euclid’s theorems there’s something new. The whole third-of-a-century story of the Wolfram Language has been about finding ways to represent more and more things in the world computationally. I had long wondered what it would take to represent Euclid-style geometry computationally. And in April I was excited to announce that we’d managed to do it:
Basic Statistics of Euclid
Euclid’s Elements is divided into 13 “books”, containing a total of 465 theorems (and 131 definitions):
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; Module[{g, h},
g[expr_] := Style[Row[{"(", expr, ")"}], Italic, Gray, 10];
h[expr_] := Style[expr, Italic, FontFamily -> "Source Sans Pro"];
Text[Grid[
MapIndexed[
Prepend[#,
Style[{"subjects", "books", "theorems", "totals", "definitions",
"totals"}[[First[#2]]], Italic,
FontFamily -> "Source Sans Pro"]] &, {{h[
"2D geometry"], \[SpanFromLeft], \[SpanFromLeft], \
\[SpanFromLeft], \[SpanFromLeft], \[SpanFromLeft],
h["numbers"], \[SpanFromLeft], \[SpanFromLeft], \[SpanFromLeft],
h["3D geometry"], \[SpanFromLeft], \[SpanFromLeft]},
Style[#, Italic, Smaller] & /@ Range[13], {48, 14, 37, 16, 25,
33, 39, 27, 36, 115, 39, 18,
18}, {g[173], \[SpanFromLeft], \[SpanFromLeft], \
\[SpanFromLeft], \[SpanFromLeft], \[SpanFromLeft],
g[217], \[SpanFromLeft], \[SpanFromLeft], \[SpanFromLeft],
g[75], \[SpanFromLeft], \[SpanFromLeft]}, {23, 2, 11, 7, 18, 4,
22, 0, 0, 16, 28, 0,
0}, {g@
65, \[SpanFromLeft], \[SpanFromLeft], \[SpanFromLeft], \
\[SpanFromLeft], \[SpanFromLeft],
g@38, \[SpanFromLeft], \[SpanFromLeft], \[SpanFromLeft],
g@28, \[SpanFromLeft], \[SpanFromLeft]}}],
Background -> {Prepend[
Composition[Lighter[#, 0.4] &, bookColor] /@ Range[13],
GrayLevel[0.9]], None}, Frame -> All]]]
|
Stating the theorems takes 9589 words (about 60k characters) of Greek (about 13,000 words in a standard English translation). (The 10 axioms take another 115 words in Greek or about 140 in English, and the definitions another 2369 words in Greek or about 3300 in English.)
A typical theorem (or “proposition”)—in this case Book 1, Theorem 20—is stated as:
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; GreekEnglishShort[<| "Book" -> 1, "Theorem" -> 20|>] |
(This is what we now call the triangle inequality. And of course, to make this statement we have to have defined what a triangle is, and Euclid does that earlier in Book 1.)
If we look at the statements of Euclid’s theorems in Greek (or in English), there’s a distribution of lengths (colored here by subjects, and reasonably fit by a Pascal distribution):
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; GraphicsRow[
MapThread[
Function[{t, l}, Module[{dataE = WordCount[#[t]] & /@ eus, dataG},
dataG =
GroupBy[If[MissingQ[#[[1]]["Book"]],
0 -> #[[2]], #[[1]]["Book"] -> #[[2]]] & /@ Normal[dataE],
First -> Last];
Histogram[
Flatten[Join[Values[dataG[[Key /@ #]]]]] & /@ {{0}, {1, 2, 3, 4,
5, 6}, {7, 8, 9, 10}, {11, 12, 13}}, {1}, Frame -> True,
PlotRange -> All, FrameLabel -> {l, None},
FrameTicks -> {Automatic, None}, ChartLayout -> "Stacked",
ChartBaseStyle -> Opacity[1],
ChartStyle -> {bookColorIntense /@ {0, 6, 10, 13},
EdgeForm[Directive[Thin, GrayLevel[0.15]]]}]]], {{"GreekText",
"Text"}, {"Greek words", "English words"}}]]
|
The “outlier” longest-to-state theorem (in both Greek and English) is the rather unremarkable 103-Greek-word 3.8
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; GreekEnglish[<|"Book" -> 3, "Theorem" -> 8|>, 12] |
which can be illustrated as:
✕
GeometricScene[
{A, B, C, D, E, F, G, H, K, L, M},
{
GeometricAssertion[{D}, {"Outside", CircleThrough[{A, B, C}, M]}],
GeometricAssertion[{A, B, C, E, F, G, H, K, L}, "Distinct"],
Line[{D, G, M, A}],
Line[{{D, K, E}, {D, L, F}, {D, H, C}}],
CircleThrough[{A, B, C, E, F, G, H, K, L}, M],
GeometricAssertion[{A, E, F, C, H, L, K, G, B},
"CyclicallyOrdered"],
Style[{Line[{M, K}], Line[{M, L}], Line[{M, H}], Line[{M, C}],
Line[{M, F}], Line[{M, E}]}, Dashed],
PlanarAngle[{D, M, B}] == PlanarAngle[{D, M, K}],
Line[{D, B}]
}(*,
{
EuclideanDistance[D,A]>EuclideanDistance[D,E]>EuclideanDistance[D,
F]>EuclideanDistance[D,C],
EuclideanDistance[D,G]<EuclideanDistance[D,K]<EuclideanDistance[D,
L]<EuclideanDistance[D,H],
EuclideanDistance[D,B]==EuclideanDistance[D,K]
}*)
] // RandomInstance
|
(The runner-up, at about two-thirds the length, is the also rather unremarkable 11.35.)
The nominally shortest-to-state theorems are in Book 10, Theorems 85 through 90, and all have just 4 Greek words:
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; GreekEnglish[<|"Book" -> 10, "Theorem" -> 85|>] |
⋮
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; GreekEnglishShort[<|"Book" -> 10, "Theorem" -> 90|>] |
The shortness of these theorems is a bit of a cheat, since the successive “apotomes” (pronounced /əˈpɒtəmi/ like “hippopotamus”) actually have quite long definitions that are given elsewhere. And, yes, some emphasis in math has changed in the past 2000+ years; you don’t hear about apotomes these days. (An apotome is a number x – y where 
isn’t rational, but 
is—as for 
, y = 1. It’s difficult enough to describe even this without math notation. But then for a “first apotome” Euclid added the conditions that both 
and x must be rational—all described in words.)
At five words, we’ve got one more familiar theorem (3.30) and another somewhat obscure one (10.26):
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; GreekEnglishShort[<|"Book" -> 3, "Theorem" -> 30|>] |
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; GreekEnglishShort[<|"Book" -> 10, "Theorem" -> 26|>] |
In our modern Wolfram Language representation, we’ve got a precise, symbolic way to state Euclid’s theorems. But Euclid had to rely on natural language (in his case, Greek). Some words he just assumed people would know the meanings of. But others he defined. Famously, he started at the beginning of Book 1 with his Definition 1—and in a sense changing how we think about this is what launched our whole Physics Project:
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; GreekEnglishShort[<|"Book" -> 1, "Definition" -> 1|>] |
There is at least an implicit network of dependencies among Euclid’s definitions. Having started by defining points and lines, he moves on to defining things like triangles, and equilaterality, until eventually, for example, by Book 11 Definition 27 he’s saying things like “An icosahedron is a solid figure contained by twenty equal and equilateral triangles”.
Of course, Euclid didn’t ultimately have to set up definitions; he could just have repeated the content of each definition every time he wanted to refer to that concept. But like words in natural language—or functions in our computational language—definitions are an important form of compression for making statements. And, yes, you have to pick the right definitions to make the things you want to say easy to say. And, yes, your definitions will likely play at least some role in determining what kinds of things you choose to talk about. (Apotomes, anyone?)
The Interdependence of Theorems
All the theorems Euclid states represent less than 10,000 words of Greek. But the standard proofs of them are perhaps 150,000 words of Greek. (They’re undoubtedly not minimal proofs—but the fact that the same ones are being quoted after more than 2000 years presumably tells us at least something.)
Euclid is very systematic. Every theorem throughout the course of his Elements is proved in terms of earlier theorems (and ultimately in terms of his 10 axioms). Thus, for example, the proof of 1.14 (i.e. Book 1, Theorem 14) uses 1.13 as well as the axioms P2 (i.e. Postulate 2), P4, CN1 (i.e. Common Notion 1) and CN3. By the time one’s got to 12.18 the proof is written only in terms of other theorems (in this case 12.17, 12.2, 5.14 and 5.16) and not directly in terms of axioms.
The total number of theorems (or axioms) directly referenced in a given proof varies from 0 (for axioms) to 21 (for 12.17, which is about inscribing polyhedra in spheres); the average is 4.3:
✕
CloudGet["https://wolfr.am/PJKo9Lnq"];
Histogram[
Module[{vod = # -> VertexOutDegree[euc, #] & /@ VertexList[euc],
dataG}, dataG =
GroupBy[If[MissingQ[#[[1]]["Book"]],
0 -> #[[2]], #[[1]]["Book"] -> #[[2]]] & /@ vod, First -> Last];
Flatten[Join[Values[dataG[[Key /@ #]]]]] & /@ {{0}, {1, 2, 3, 4, 5,
6}, {7, 8, 9, 10}, {11, 12, 13}}
], {1}, Frame -> True,
FrameLabel -> {"number of theorems directly referenced"},
ChartLayout -> "Stacked", ChartBaseStyle -> Opacity[1],
ChartStyle -> {bookColorIntense /@ {0, 6, 10, 13},
EdgeForm[Directive[Thin, GrayLevel[0.15]]]}]
|
If we put Euclid’s axioms and theorems in order, we can represent which axioms or theorems occur in a given proof by an arrangement of dots across the page. For example, for 1.12 through 1.17 we have:
✕
CloudGet["https://wolfr.am/PJKo9Lnq"];
With[{axiomcol = bookColorDarker[0], geom2dcol = bookColor[1]},
Grid[With[{head =
Composition[Text, Style[#, 13] &, EuclidVertexName] /@
Take[SortBy[VertexList[euc], Length], 26]},
Prepend[Table[
Prepend[If[
MemberQ[Rest[
VertexOutComponent[euc, <|"Book" -> 1, "Theorem" -> n|>,
1]], #], Style["\[FilledCircle]", 10], ""] & /@
Take[SortBy[VertexList[euc], Length], 25],
Text[Style[EuclidVertexName[<|"Book" -> 1, "Theorem" -> n|>],
13]]], {n, 12, 17}], Prepend[head, ""]]],
Background -> {1 -> GrayLevel[.9],
1 -> GrayLevel[.9], {{{2, -1}, {2, 11}} ->
axiomcol, {{2, -1}, {12, -1}} -> geom2dcol}}, Frame -> All,
FrameStyle -> GrayLevel[.7], ItemSize -> All,
Spacings -> {0.2, 0.2}]]
|
Doing this for all the theorems we get:
✕
Cell[CellGroupData[{
Cell[BoxData[
RowBox[{
RowBox[{"CloudGet", "[", "\"\<https://wolfr.am/PJKo9Lnq\>\"", "]"}],
";"}]], "Input"],
Cell[BoxData[
RowBox[{
RowBox[{"key", "=",
RowBox[{"MapIndexed", "[",
RowBox[{
RowBox[{
RowBox[{"#", "\[Rule]",
RowBox[{"First", "[", "#2", "]"}]}], "&"}], ",",
RowBox[{
RowBox[{"GatherBy", "[",
RowBox[{
RowBox[{"VertexList", "[", "euc", "]"}], ",", "Length"}],
"]"}], "[",
RowBox[{"[", "1", "]"}], "]"}]}], "]"}]}], ";"}]], "Input"],
Cell[BoxData[
RowBox[{
RowBox[{"bookmarkers", "=",
RowBox[{"Append", "[",
RowBox[{
RowBox[{"First", "/@",
RowBox[{"Table", "[",
RowBox[{
RowBox[{"FirstPosition", "[",
RowBox[{
RowBox[{"First", "/@", "key"}], ",",
RowBox[{"<|",
RowBox[{
RowBox[{"\"\<Book\>\"", "\[Rule]", "b"}], ",",
RowBox[{"\"\<Theorem\>\"", "\[Rule]", "_"}]}], "|>"}]}],
"]"}], ",",
RowBox[{"{",
RowBox[{"b", ",", "13"}], "}"}]}], "]"}]}], ",",
RowBox[{"Length", "[", "key", "]"}]}], "]"}]}], ";"}]], "Input"],
Cell[BoxData[
RowBox[{"ListPlot", "[",
RowBox[{
RowBox[{
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{"1", ",",
RowBox[{"-", "1"}]}], "}"}], "*", "#"}], "&"}], "/@",
RowBox[{"DeleteCases", "[",
RowBox[{
RowBox[{"Reverse", "/@",
RowBox[{"(",
RowBox[{"List", "@@@",
RowBox[{"(",
RowBox[{
RowBox[{"EdgeList", "[", "euc", "]"}], "/.", "key"}],
")"}]}], ")"}]}], ",",
RowBox[{"{",
RowBox[{"x_", ",", "x_"}], "}"}]}], "]"}]}], ",",
RowBox[{"PlotStyle", "\[Rule]", "Black"}], ",",
RowBox[{"AspectRatio", "\[Rule]", "1"}], ",",
RowBox[{"GridLines", "\[Rule]",
RowBox[{"{",
RowBox[{"bookmarkers", ",",
RowBox[{"-", "bookmarkers"}]}], "}"}]}], ",",
RowBox[{"Ticks", "\[Rule]", "None"}], ",",
RowBox[{"PlotRange", "->",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"-", "10"}], ",", "460"}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"-", "468"}], ",",
RowBox[{"-", "10"}]}], "}"}]}], "}"}]}], ",", " ",
RowBox[{"Epilog", "\[Rule]",
RowBox[{"{",
RowBox[{
RowBox[{"MapIndexed", "[",
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"Style", "[",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"Text", "[",
RowBox[{
RowBox[{"#2", "[",
RowBox[{"[", "1", "]"}], "]"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"Mean", "[", "#1", "]"}], ",", "5"}],
"}"}]}], "]"}], ",",
RowBox[{"Text", "[",
RowBox[{
RowBox[{"#2", "[",
RowBox[{"[", "1", "]"}], "]"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"-", "5"}], ",",
RowBox[{"-",
RowBox[{"Mean", "[", "#1", "]"}]}]}], "}"}]}],
"]"}]}], "}"}], ",", "14"}], "]"}], ",",
RowBox[{"bookColorDarker", "[",
RowBox[{"#2", "[",
RowBox[{"[", "1", "]"}], "]"}], "]"}], ",",
RowBox[{"Opacity", "[", ".3", "]"}], ",",
RowBox[{"Rectangle", "[",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"#1", "[",
RowBox[{"[", "1", "]"}], "]"}], ",",
RowBox[{"-", "465"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"#1", "[",
RowBox[{"[", "2", "]"}], "]"}], ",", "0"}], "}"}]}],
"]"}], ",",
RowBox[{"Rectangle", "[",
RowBox[{
RowBox[{"{",
RowBox[{"0", ",",
RowBox[{"-",
RowBox[{"#1", "[",
RowBox[{"[", "2", "]"}], "]"}]}]}], "}"}], ",",
RowBox[{"{",
RowBox[{"465", ",",
RowBox[{"-",
RowBox[{"#1", "[",
RowBox[{"[", "1", "]"}], "]"}]}]}], "}"}]}], "]"}]}],
"}"}], "&"}], ",",
RowBox[{"Partition", "[",
RowBox[{"bookmarkers", ",", "2", ",", "1"}], "]"}]}], "]"}],
",",
RowBox[{"GrayLevel", "[", ".6", "]"}], ",",
RowBox[{"Opacity", "[", ".3", "]"}], ",",
RowBox[{"Rectangle", "[",
RowBox[{
RowBox[{"{",
RowBox[{"0", ",", "0"}], "}"}], ",",
RowBox[{"{",
RowBox[{"465", ",", "20"}], "}"}]}], "]"}], ",",
RowBox[{"Rectangle", "[",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"-", "10"}], ",",
RowBox[{"-", "465"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{"0", ",", "0"}], "}"}]}], "]"}]}], "}"}]}]}],
"]"}]], "Input"]
}, Open ]]
|
We can see there’s lots of structure here. For example, there are clearly “popular” theorems near the beginning of Book 6 and Book 10, to which lots of at least “nearby” theorems refer. There are also “gaps”: ranges of theorems that no theorems in a given book refer to.
At a coarse level, something we can do is to look at cross-referencing within and between books:
✕
Cell[CellGroupData[{
Cell[BoxData[
RowBox[{
RowBox[{"CloudGet", "[", "\"\<https://wolfr.am/PJKo9Lnq\>\"", "]"}],
";"}]], "Input"],
Cell[BoxData[
RowBox[{
RowBox[{"books", "=",
RowBox[{"{",
RowBox[{
RowBox[{"\"\<Book\>\"", "\[Rule]", "1"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "2"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "3"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "4"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "5"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "6"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "7"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "8"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "9"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "10"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "11"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "12"}], ",",
RowBox[{"\"\<Book\>\"", "\[Rule]", "13"}]}], "}"}]}],
";"}]], "Input"],
Cell[BoxData[
RowBox[{
RowBox[{"vertexweights", "=",
RowBox[{"Select", "[",
RowBox[{
RowBox[{"Tally", "[",
RowBox[{
RowBox[{
RowBox[{"First", "[",
RowBox[{"Normal", "[", "#", "]"}], "]"}], "&"}], "/@",
RowBox[{"VertexList", "[", "euc", "]"}]}], "]"}], ",",
RowBox[{
RowBox[{"MemberQ", "[",
RowBox[{"books", ",",
RowBox[{"First", "[", "#", "]"}]}], "]"}], "&"}]}], "]"}]}],
";"}]], "Input"],
Cell[BoxData[
RowBox[{
RowBox[{"edgeweights", "=",
RowBox[{"Select", "[",
RowBox[{
RowBox[{"Tally", "[",
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{
RowBox[{"Normal", "[", "#", "]"}], "[",
RowBox[{"[",
RowBox[{"1", ",", "1"}], "]"}], "]"}], ",",
RowBox[{
RowBox[{"Normal", "[", "#", "]"}], "[",
RowBox[{"[",
RowBox[{"2", ",", "1"}], "]"}], "]"}]}], "}"}], "&"}], "/@",
RowBox[{"EdgeList", "[", "euc", "]"}]}], "]"}], ",",
RowBox[{
RowBox[{"MemberQ", "[",
RowBox[{"books", ",",
RowBox[{"#", "[",
RowBox[{"[",
RowBox[{"1", ",", "2"}], "]"}], "]"}]}], "]"}], "&"}]}],
"]"}]}], ";"}]], "Input"],
Cell[BoxData[
RowBox[{
RowBox[{"bookweights", "=",
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"Last", "[",
RowBox[{"First", "[", "#", "]"}], "]"}], ",",
RowBox[{"Last", "[", "#", "]"}]}], "}"}], "&"}], "/@",
"vertexweights"}]}], ";"}]], "Input"],
Cell[BoxData[
RowBox[{
RowBox[{"edgesout", "=",
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"#", "[",
RowBox[{"[",
RowBox[{"1", ",", "1", ",", "1", ",", "2"}], "]"}], "]"}],
",",
RowBox[{"Total", "[",
RowBox[{"#", "[",
RowBox[{"[", "2", "]"}], "]"}], "]"}]}], "}"}], "&"}], "/@",
RowBox[{"(",
RowBox[{"Transpose", "/@",
RowBox[{"GatherBy", "[",
RowBox[{"edgeweights", ",",
RowBox[{
RowBox[{"#", "[",
RowBox[{"[",
RowBox[{"1", ",", "1"}], "]"}], "]"}], "&"}]}], "]"}]}],
")"}]}]}], ";"}]], "Input"],
Cell[BoxData[{
RowBox[{
RowBox[{
RowBox[{"normalizededgeweights", "=",
RowBox[{
RowBox[{
RowBox[{
RowBox[{"DirectedEdge", "[",
RowBox[{
RowBox[{"#", "[",
RowBox[{"[",
RowBox[{"1", ",", "1", ",", "2"}], "]"}], "]"}], ",",
RowBox[{"#", "[",
RowBox[{"[",
RowBox[{"1", ",", "2", ",", "2"}], "]"}], "]"}]}], "]"}],
"\[Rule]",
RowBox[{
RowBox[{"#", "[",
RowBox[{"[", "2", "]"}], "]"}], "/",
RowBox[{"edgesout", "[",
RowBox[{"[",
RowBox[{
RowBox[{"#", "[",
RowBox[{"[",
RowBox[{"1", ",", "1", ",", "2"}], "]"}], "]"}], ",",
"2"}], "]"}], "]"}]}]}], "&"}], "/@", "edgeweights"}]}],
";"}], "\n"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{
RowBox[{"diskedLine", "[",
RowBox[{"{",
RowBox[{"line_", ",", "radii_"}], "}"}], "]"}], ":=",
RowBox[{"{",
RowBox[{
RowBox[{
RowBox[{"RegionIntersection", "[",
RowBox[{
RowBox[{"Line", "[", "line", "]"}], ",",
RowBox[{"Circle", "[",
RowBox[{
RowBox[{"line", "[",
RowBox[{"[", "1", "]"}], "]"}], ",",
RowBox[{"radii", "[",
RowBox[{"[", "1", "]"}], "]"}]}], "]"}]}], "]"}], "[",
RowBox[{"[",
RowBox[{"1", ",", "1"}], "]"}], "]"}], ",",
RowBox[{
RowBox[{"RegionIntersection", "[",
RowBox[{
RowBox[{"Line", "[", "line", "]"}], ",",
RowBox[{"Circle", "[",
RowBox[{
RowBox[{"line", "[",
RowBox[{"[", "2", "]"}], "]"}], ",",
RowBox[{"radii", "[",
RowBox[{"[", "2", "]"}], "]"}]}], "]"}]}], "]"}], "[",
RowBox[{"[",
RowBox[{"1", ",", "1"}], "]"}], "]"}]}], "}"}]}], ";"}],
"\n"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{"weightedArrow", "[",
RowBox[{"line_", ",", "weight_"}], "]"}], ":=",
RowBox[{"Module", "[",
RowBox[{
RowBox[{"{",
RowBox[{
"len", ",", "start", ",", "end", ",", "angle", ",", "thick",
",", "rec", ",", "mid"}], "}"}], ",",
RowBox[{
RowBox[{"start", "=",
RowBox[{"line", "[",
RowBox[{"[", "1", "]"}], "]"}]}], ";",
RowBox[{"end", "=",
RowBox[{"line", "[",
RowBox[{"[", "2", "]"}], "]"}]}], ";",
RowBox[{"mid", "=",
RowBox[{"Mean", "[", "line", "]"}]}], ";",
"\[IndentingNewLine]",
RowBox[{"len", "=",
RowBox[{"EuclideanDistance", "[",
RowBox[{"start", ",", "end"}], "]"}]}], ";",
"\[IndentingNewLine]",
RowBox[{"angle", "=",
RowBox[{"Arg", "[",
RowBox[{
RowBox[{"(",
RowBox[{"start", "-", "end"}], ")"}], ".",
RowBox[{"{",
RowBox[{"1", ",", "I"}], "}"}]}], "]"}]}], ";",
"\[IndentingNewLine]",
RowBox[{"thick", "=",
RowBox[{"weight", "/", "len"}]}], ";", "\[IndentingNewLine]",
RowBox[{"rec", "=",
RowBox[{
RowBox[{
RowBox[{"#", "+", "mid"}], "&"}], "/@",
RowBox[{"(",
RowBox[{
RowBox[{
RowBox[{
RowBox[{"RotationMatrix", "[", "angle", "]"}], ".", "#"}],
"&"}], "/@",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{
RowBox[{"-", "len"}], "/", "2"}], ",",
RowBox[{
RowBox[{"-", "thick"}], "/", "2"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"len", "/", "2"}], ",",
RowBox[{
RowBox[{"-", "thick"}], "/", "2"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"len", "/", "2"}], ",",
RowBox[{"thick", "/", "2"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{
RowBox[{"-", "len"}], "/", "2"}], ",",
RowBox[{"thick", "/", "2"}]}], "}"}]}], "}"}]}],
")"}]}]}], ";", "\[IndentingNewLine]",
RowBox[{"Polygon", "[", "rec", "]"}]}]}], "]"}]}],
";"}]}], "Input"],
Cell[BoxData[
RowBox[{"Labeled", "[",
RowBox[{
RowBox[{"Graph", "[",
RowBox[{
RowBox[{"Range", "[", "13", "]"}], ",",
RowBox[{"First", "/@", "normalizededgeweights"}], ",",
RowBox[{"EdgeStyle", "\[Rule]",
RowBox[{"Thread", "[",
RowBox[{
RowBox[{"First", "/@", "normalizededgeweights"}], "\[Rule]",
RowBox[{"(",
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"AbsoluteThickness", "[",
RowBox[{"15", " ",
RowBox[{"Last", "[", "#", "]"}]}], "]"}], ",",
RowBox[{"bookColorIntense", "[",
RowBox[{"First", "[",
RowBox[{"First", "[", "#", "]"}], "]"}], "]"}], ",",
RowBox[{"Arrowheads", "[",
RowBox[{
RowBox[{"Last", "[", "#", "]"}], "/", "15"}], "]"}]}],
"}"}], "&"}], "/@", "normalizededgeweights"}], ")"}]}],
"]"}]}], ",",
RowBox[{"VertexSize", "\[Rule]",
RowBox[{"Thread", "[",
RowBox[{
RowBox[{"First", "/@", "bookweights"}], "\[Rule]",
RowBox[{"(",
RowBox[{
RowBox[{
RowBox[{"1.5", " ",
RowBox[{
RowBox[{"Sqrt", "[", "#", "]"}], "/", "20"}]}], "&"}], "/@",
RowBox[{"(",
RowBox[{"Last", "/@", "bookweights"}], ")"}]}], ")"}]}],
"]"}]}], ",",
RowBox[{"VertexStyle", "\[Rule]",
RowBox[{"(",
RowBox[{
RowBox[{
RowBox[{"#", "\[Rule]",
RowBox[{"{",
RowBox[{
RowBox[{"bookColorIntense", "[", "#", "]"}], ",",
RowBox[{"EdgeForm", "[",
RowBox[{"Darker", "[",
RowBox[{
RowBox[{"bookColorIntense", "[", "#", "]"}], ",",
".2"}], "]"}], "]"}]}], "}"}]}], "&"}], "/@",
RowBox[{"Range", "[", "13", "]"}]}], ")"}]}], ",",
RowBox[{"GraphLayout", "\[Rule]",
RowBox[{"{",
RowBox[{
RowBox[{
"\"\<VertexLayout\>\"", "\[Rule]", " ",
"\"\<SpringElectricalEmbedding\>\""}], ",",
RowBox[{"\"\<SelfLoopRadius\>\"", "\[Rule]", " ", "1"}]}],
"}"}]}], ",",
RowBox[{"VertexLabels", "\[Rule]",
RowBox[{"Placed", "[",
RowBox[{"Automatic", ",", "Center"}], "]"}]}], ",",
RowBox[{"PerformanceGoal", "\[Rule]", "\"\<Quality\>\""}], ",",
RowBox[{"BaseStyle", "\[Rule]", "13"}]}], "]"}], ",",
RowBox[{"Row", "[",
RowBox[{
RowBox[{
RowBox[{
RowBox[{"Row", "[",
RowBox[{"#", ",",
RowBox[{"Spacer", "[", "0.005", "]"}]}], "]"}], "&"}], "/@",
RowBox[{"Transpose", "[",
RowBox[{"{",
RowBox[{
RowBox[{"bookColorIntense", "/@",
RowBox[{"{",
RowBox[{"6", ",", "10", ",", "13"}], "}"}]}], ",",
RowBox[{
RowBox[{
RowBox[{"Style", "[",
RowBox[{"#", ",",
RowBox[{
"FontFamily", "\[Rule]", "\"\<Source Sans Pro\>\""}],
",",
RowBox[{"GrayLevel", "[", "0.3", "]"}], ",",
RowBox[{"FontSize", "\[Rule]", "16"}]}], "]"}], "&"}], "/@",
RowBox[{"{",
RowBox[{
"\"\<2D geometry\>\"", ",", " ", "\"\<numbers\>\"", ",",
"\"\<3D geometry\>\""}], "}"}]}]}], "}"}], "]"}]}], ",",
RowBox[{"Spacer", "[", "20", "]"}]}], "]"}]}], "]"}]], "Input"]
}, Open ]]
|
The size of each node represents the number of theorems in each book. The thickness of each arrow represents the fraction of references in the proofs of those theorems going to different books. The self-loops are from theorems in a given book that refer to theorems in the same book. Needless to say, the self-loop is large for Book 1, since it doesn’t have any previous book to refer to. Book 7 again has a large self-loop, because it’s the first book about numbers, and doesn’t refer much to the earlier books (which are about 2D geometry).
It’s interesting to see that Books 7, 8 and 9—which are about numbers rather than geometry—“keep to themselves”, even though Book 10, which is also about numbers, is more central. It’s also interesting to see the interplay between the books on 2D and 3D geometry over on the right-hand side of the graph.
But, OK, what about individual theorems? What is their network of dependencies?
Here’s 1.5, whose proof is given in terms of 1.3 and 1.4, as well as the axioms P1, P2 and CN3:
✕
CloudGet["https://wolfr.am/PJKo9Lnq"]; EuclidGraphLarge[ Subgraph[euc, VertexOutComponent[euc, <|"Book" -> 1, "Theorem" -> 5|>, 1]]] |
But now we can continue this, and show what 1.3 and 1.4 depend on—all the way down to the axioms:
|
|