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.
