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.