The Empirical Metamathematics of Euclid and Beyond

TL;DR

This paper empirically analyzes the dependency structures of Euclid's theorems and modern mathematical projects, revealing insights into the nature and exploration of metamathematical space.

Contribution

It introduces empirical methods to study the dependency structures in Euclid's Elements and modern mathematics, uncovering intrinsic features of metamathematical space.

Findings

Dependency signatures correlate with theorem power

Structural patterns in formalized mathematics

Historical analysis of mathematical exploration

Abstract

As an example of empirical metamathematics, we present a detailed study of the dependency structure of the 465 theorems in Euclid's Elements, finding empirical signatures of concepts such as the power of a theorem. We apply similar methods to a more exhaustive study of possible theorems in logic, as well as to the analysis of dependency structures in projects to formalize modern pure mathematics. We discuss the process of identifying both intrinsic features of metamathematical space, and features of its exploration through the historical progress of mathematics.