“The Empirical Metamathematics of Euclid and Beyond”, 2020-09-28 (; similar):
[Consideration of Euclid’s Elements as a network or directed acyclic graph of axioms, proofs, and theorems. Starting with the axioms, each proof relies on previously defined/proven elements; as such they form a network. What does this network look like? What does it reveal? What ‘nodes’ are most central, most reused elsewhere? Could the network be simplified or made more compact, by adding missing theorems or more complex ‘super-axioms’?
Wolfram uses Mathematica to parse the Elements and generate graph theory statistics about the 13 books, 131 definitions, and 465 theorems. There is clearly structure, and ‘popular’ theorems which are reused often, while some theorems are obscure and don’t come up again. Similarly, the books differ greatly in importance, and some books form groupings by themselves as relatively independent topics from the rest. As the books develop, they use more and more theorems, and fewer and fewer axioms: the overall structure implies that, after a slow start bootstrapping, a few critical theorems ‘unlock’ many of the later theorems. Interestingly, the ‘climax’, the theorem which requires the most earlier theorems, is Euclid’s proof that there are 5 Platonic solids (a concept that fascinated many Greco-Roman mathematicians and philosophers).
Similar questions could be asked of modern mathematics after formalization, and might yield an ‘empirical metamathematics’ showing how human mathematicians structure their theories and go about proving the theorems they choose to.]
View HTML (48MB):