
SOME HISTORICAL NOTES
From: Stephen Wolfram, A New Kind of Science Notes for Chapter 12: The Principle of Computational Equivalence
Section: Implications for Mathematics and Its Foundations
Page 1176
Empirical metamathematics. One can imagine a network representing some field of mathematics, with nodes corresponding to theorems and connections corresponding to proofs, gradually getting filled in as the field develops. Typical rough characterizations of mathematical results  independent of their detailed history  might then end up being something like the following:
lemma: short theorem appearing at an intermediate stage in a proof
corollary: theorem connected by a short proof to an existing theorem
easy theorem: theorem having a short proof
difficult theorem: theorem having a long proof
elegant theorem: theorem whose statement is short and somewhat unique
interesting theorem (see page 817): theorem that cannot readily be deduced from earlier theorems, but is well connected
boring theorem: theorem for which there are many others very much like it
useful theorem: theorem that leads to many new ones
powerful theorem: theorem that substantially reduces the lengths of proofs needed for many others
surprising theorem: theorem that appears in an otherwise sparse part of the network of theorems
deep theorem: theorem that connects components of the network of theorems that are otherwise far away
important theorem: theorem that allows a broad new area of the network to be reached.
The picture below shows the network of theorems associated with Euclid’s Elements. Each stated theorem is represented by a node connected to the theorems used in its stated proof. (Only the shortest connection from each theorem is shown explicitly.) The axioms (postulates and common notions) are given in the first column on the left, and successive columns then show theorems with progressively longer proofs. (Explicit annotations giving theorems used in proofs were apparently added to editions of Euclid only in the past few centuries; the picture below extends the usual annotations in a few cases.) The theorem with the longest proof is the one that states that there are only five Platonic solids.
Stephen Wolfram, A New Kind of Science (Wolfram Media, 2002), page 1176.
© 2002, Stephen Wolfram, LLC

