Bridging Classical and Modern Approaches to Thales' Theorem
Piotr Błaszczyk, Anna Petiurenko
TL;DR
This work bridges Euclid's proportion theory in Book VI with 20th-century foundations (Hilbert, Hartshorne, Borsuk–Szmielew, Birkhoff, Millman–Parker) and nonstandard approaches, with Thales' theorem $($VI.2$)$ as the central reference. It analyzes two reconstruction strategies—arithmetic of line segments and real-number arithmetic—and demonstrates how each leads to a rigorous, deductive reconstruction of Euclid's theory, including automated proofs via the Area Method and the GCLC prover. The paper also extends these ideas to non-Archimedean settings, showing Thales' theorem in the hyperreal plane ${\mathbb{R}}^*\times{\mathbb{R}}^*$ and discussing generalizations to nonstandard analysis. Overall, it provides a unified view of similarity and proportion across synthetic, metric, and nonstandard geometries, offering insights for automated reasoning and foundational studies. The results highlight how classical geometry remains coherent under diverse axiomatizations and demonstrates practical computational tools for mechanical proofs in geometry.
Abstract
In this paper, we reconstruct Euclid's theory of similar triangles, as developed in Book VI of the \textit{Elements}, along with its 20th-century counterparts, formulated within the systems of Hilbert, Birkhoff, Borsuk and Szmielew, Millman and Parker, as well as Hartshorne. In the final sections, we present recent developments concerning non-Archimedean fields and mechanized proofs. Thales' theorem (VI.2) serves as the reference point in our comparisons. It forms the basis of Euclid's system and follows from VI.1 the only proposition within the theory of similar triangles that explicitly applies the definition of proportion. Instead of the ancient proportion, modern systems adopt the arithmetic of line segments or real numbers. Accordingly, they adopt other propositions from Euclid's Book VI, such as VI.4, VI.6, or VI.9, as a basis. In §\,10, we present a system that, while meeting modern criteria of rigor, reconstructs Euclid's theory and mimics its deductive structure, beginning with VI.1. This system extends to automated proofs of Euclid's propositions from Book VI. Systems relying on real numbers provide the foundation for trigonometry as applied in modern mathematics. In §\,9, we prove Thales' theorem in geometry over the hyperreal numbers. Just as Hilbert managed to prove Thales' theorem without referencing the Archimedean axiom, so do we by applying the arithmetic of the non-Archimedean field of hyperreal numbers.