Abstract
We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski’s formal geometry. We used proofs as close as possible to those given by Euclid, but filling Euclid’s gaps and correcting errors. Euclid Book I has 48 propositions; we proved 235 theorems. The extras were partly “Book Zero”, preliminaries of a very fundamental nature, partly propositions that Euclid omitted but were used implicitly, partly advanced theorems that we found necessary to fill Euclid’s gaps, and partly just variants of Euclid’s propositions. We wrote these proofs in a simple fragment of first-order logic corresponding to Euclid’s logic, debugged them using a custom software tool, and then checked them in the well-known and trusted proof checkers HOL Light and Coq.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s Elements. Rev. Symb. Log. 2, 700–768 (2009)
Beeson, M.: A constructive version of Tarski’s geometry. Ann. Pure Appl. Logic 166, 1199–1273 (2015)
Beeson, M.: Constructive geometry and the parallel postulate. Bull. Symb. Log. 22, 1–104 (2016)
Bledsoe, W. W., Loveland, D.: Automated Theorem Proving: After 25 Years. American Mathematical Society, Providence (1983)
Boutry, P.: On the Formalization of Foundations of Geometry. PhD thesis, University of Strasbourg (2018)
Boutry, P., Braun, G., Narboux, J.: From Tarski to Descartes: formalization of the arithmetization of Euclidean geometry. In: Davenport, J.H., Ghourabi, F. (eds.) SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science, vol. 39 of EPiC Series in Computing, Tokyo, Japan, EasyChair, pp. 14–28 (2016)
Boutry, P., Braun, G., Narboux, J.: Formalization of the arithmetization of Euclidean plane geometry and applications. J. Symb. Comput. 90, 149–168 (2019). https://doi.org/10.1016/j.jsc.2018.04.007
Boutry, P., Gries, C., Narboux, J., Schreck, P.: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. J. Autom. Reason., p. 68. https://link.springer.com/article/10.1007%2Fs10817-017-9422-8 (2017)
Braun, G., Boutry, P., Narboux, J.: From Hilbert to Tarski. In: 11th International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2016, Strasbourg, France, p. 19 (2016)
Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry 2012 vol. 7993, Edinburgh, United Kingdom, Jacques Fleuriot, Springer, pp. 89–109 (2012)
Braun, G., Narboux, J.: A synthetic proof of Pappus’ theorem in Tarski’s geometry. J. Autom. Reason. 58, 23 (2017)
Chou, S. C.: Mechanical Geometry Theorem Proving. Kluwer Academic Publishers, Norwell (1987)
Chou, S. C.: An introduction to Wu’s method for mechanical theorem proving in geometry. J. Autom. Reason. 4, 237–267 (1988)
Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. World Scientific (1994)
Chou, S. C., Schelter, W. F.: Proving geometry theorems with rewrite rules. J. Autom. Reason. 2, 253–273 (1986)
Corbineau, P.: A declarative language for the Coq proof assistant. In: Types for Proofs and Programs, vol. 4941 of LNCS, Springer (2008)
Euclid: The Elements of Euclid, viz. the first six books, together with the eleventh and the twelfth, Nourse and Balfous, Edinburgh, 7th ed., 1787. Translated by Robert Simson. Available from Bibliotheque Nationale at http://gallica.bnf.fr/ark:/12148/bpt6k1163221v
Euclid: The Thirteen Books of the Elements. Dover, New York (1956). Three volumes. Includes commentary by the translator, Sir Thomas L. Heath
Gelernter, H.: Realization of a geometry theorem-proving machine. In: Feigenbaum, E., Feldman, J. (eds.) Computers and Thought, pp 134–152. McGraw-Hill, New York (1963)
Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of a geometry-theorem proving machine. In: Feigenbaum, E., Feldman, J. (eds.) Computers and Thought, pp 153–167. McGraw-Hill, New York (1963)
Greenberg, M. J.: Euclidean and non-Euclidean Geometries: Development and History, 4th edn. W. H. Freeman, New York (2008)
Gries, C.: Axiomes de continuité en géométrie neutre : Une étude méchanisée en Coq. University of Strasbourg, internship report (2017)
Gupta, H. N.: Contributions to the Axiomatic Foundations of Geometry. PhD Thesis, University of California, Berkeley (1965)
Hartshorne, R.: Geometry: Euclid and Beyond. Springer, New York (2000)
Hilbert, D.: Foundations of Geometry (Grundlagen der Geometrie). Open Court, La Salle, Illinois Second English edition, translated from the tenth German edition by Leo Unger. Original publication year (1899)
Kapur, D.: A refutational approach to geometry theorem proving. J. Artif. Intell. 37, 61–93 (1988)
Kutzler, B., Stifter, S.: Automated geometry theorem proving using Buchberger’s algorithm. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation (SYMSAC 86), Waterloo, 1986, B. Char, ed., pp. 209–214 (1986)
Manders, K.: The Euclidean diagram (1995). In: The Philosophy of Mathematical Practice, Paolo Mancosu. Oxford University Press ed. (2011)
Miller, N.: A Diagrammatic Formal System for Euclidean Geometry. PhD thesis, Cornell University (2001)
Miller, N.: Euclid and his twentieth century rivals: diagrams in the logic of Euclidean geometry. Studies in the theory and applications of diagrams, CSLI Publications, Stanford, Calif, 2007. OCLC: ocm71947628
Miller, N.: On the inconsistency of Mumma’s Eu. Notre Dame Journal of Formal Logic 53, 27–52 (2012)
Mollerup, J.: Die Beweise der ebenen Geometrie ohne Benutzung der Gleichheit und Ungleichheit der Winkel. Math. Ann. 58, 479–496 (1904)
Mumma, J.: Proofs, pictures, and Euclid. Synthese 175, 255–287 (2010)
Narboux, J., Janičić, P., Fleuriot, J.: Computer-assisted theorem proving in synthetic geometry. In: Sitharam, M., John, A.S., Sidman, J. (eds.) Handbook of Geometric Constraint Systems Principles, Chapman and Hall/CRC, ch. 2. in press (2018)
Pasch, M.: Vorlesung über Neuere Geometrie. Teubner, Leipzig (1882)
Peano, G.: Principii de Geometria. Fratelli Bocca, Torino (1889)
Potts, R.: Euclid’s Elements of Geometry [Books 1-6, 11,12] with Explanatory Notes; Together with a Selection of Geometrical Exercises. To which is Prefixed an Intr., Containing a Brief Outline of the History of Geometry. Oxford University Press, Oxford (1845)
Proclus: A Commentary on the First Book of Euclid. Princeton University Press, Princeton (1970)
Quaife, A.: Automated development of Tarski’s geometry. J. Autom. Reason. 5, 97–118 (1989)
Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie: Teil I: Ein axiomatischer Aufbau der euklidischen Geometrie. Teil II: Metamathematische Betrachtungen (Hochschultext). Springer–Verlag, 1983. Reprinted 2011 by Ishi Press, with a new foreword by Michael Beeson
Stojanovic Durdevic, S., Narboux, J., Janicic, P.: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry. Ann. Math. Artif. Intell. 73, 25 (2015)
Strommer, J.: Über die Kreisaxiome. Period. Math. Hung. 4, 3–16 (1973)
Tarski, A., Givant, S.: Tarski’s system of geometry. Bull. Symb. Log. 5, 175–214 (1999)
Veronese, G.: Fondamenti di geometria a più dimensioni e a più specie di unità rettilinee esposti in forma elementare. Lezioni per la scuola di magistero in matematica, Padova: Tipografia del Seminario, 1891 (1891)
Wu, W.-T.: On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sinica 21, reprinted in [4] (1978)
Wu, W.-T.: Mechanical Theorem Proving in Geometries: Basic Principles. Springer, Wien/ New York (1994)
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Appendices
Appendix A: Formal proof of Prop. I.1
The reader may compare the following proof to Euclid’s. The conclusion ELABC, that ABC is equilateral, is reached about halfway through, and that corresponds to the end of Euclid’s proof. The firsts half of our proof corresponds fairly naturally to Euclid’s, except for quoting the circle-circle axiom, and verifying that is hypotheses are satisfied.
The last half of our proof is devoted to proving that ABC is a triangle, that is, the three points are not collinear. Note the use of lemma partnotequalwhole. If Euclid had noticed the need to prove that ABC actually is a triangle, he would have justified it using the common notions, applied to equality (congruence) of lines. This version of “the part is not equal to the whole” is not an axiom for us, but a theorem.
At the request of the referee we present this proof in a typeset form rather than in its native Polish form. Obviously further mechanical processing can increase its superficial resemblance to Euclid’s style, but the point of our present work is simply its mechanically-checked correctness.
Proposition A.1 (Prop. I.1)
On a given finite straight line to construct an equilateral triangle.
Proof
Let J be such that J is the circle of center A and radius AB by postulate Euclid3.
B ≠ A by lemma inequalitysymmetric.
Let K be such that K is the circle of center B and radius BA by postulate Euclid3.
Let D be such that A is strictly between B and D ∧ AD≅AB by lemma localextension.
AD≅BA by lemma congruenceflip.
BA≅BA by common notion congruencereflexive.
D is outside circle K by definition of outside.
B = B by common notion equalityreflexive.
B is inside circle K by definition of inside.
AB≅AB by common notion congruencereflexive.
B is on circle J by definition of on.
D is on circle J by definition of on.
A = A by common notion equalityreflexive.
A is inside circle J by definition of inside.
LetC be such that C is on circle K ∧ C is on circle J by postulate circle-circle.
AC≅AB by axiom circle-center-radius.
AB≅AC by lemma congruencesymmetric.
BC≅BA by axiom circle-center-radius.
BC≅AB by lemma congruenceflip.
BC≅AC by lemma congruencetransitive.
AB≅BC by lemma congruencesymmetric.
AC≅CA by common notion equalityreverse.
BC≅CA by lemma congruencetransitive.
ABC is equilateral by definition of equilateral.
B ≠ C by axiom nocollapse.
C ≠ A by axiom nocollapse.
Let show that C is strictly between A and B does not hold by contradiction:
{
\({A}{C} \ncong {A}{B}\) by lemma partnotequalwhole.
CA≅AC by common notion equalityreverse.
CA≅AB by lemma congruencetransitive.
AC≅CA by common notion equalityreverse.
AC≅AB by lemma congruencetransitive.
We have a contradiction.
}
Let show that B is strictly between A and C does not hold by contradiction:
{
\({A}{B} \ncong {A}{C}\) by lemma partnotequalwhole.
AB≅CA by lemma congruencetransitive.
CA≅AC by common notion equalityreverse.
AB≅AC by lemma congruencetransitive.
We have a contradiction.
}
Let show that A is strictly between B and C does not hold by contradiction:
{
\({B}{A} \ncong {B}{C}\) by lemma partnotequalwhole.
BA≅AB by common notion equalityreverse.
BA≅BC by lemma congruencetransitive.
We have a contradiction.
}
Let show that ABC are collinear does not hold by contradiction:
{
A ≠ C by lemma inequalitysymmetric.
A = B∨A = C∨B = C∨A is strictly between B and C∨B is strictly between B and C∨C is strictly between A and B by definition of collinear.
We have a contradiction.
}
ABC is a triangle by definition of triangle. □
Appendix B: Axioms and definitions
The following formulas are presented in a format that can be cut and pasted, even from a pdf file.
1.1 Definitions
A and B are distinct points
A, B, and C are collinear
A, B, and C are not collinear
P is inside (some) circle J of center C and radius AB
P is outside (some) circle J of center U and radius VW
B is on (some) circle J of center U and radius XY
ABC is equilateral
ABC is a triangle
C lies on ray AB
AB is less than CD
B is the midpoint of AC
Angle ABC is equal to angle abc
DBF is a supplement of ABC
ABC is a right angle
PQ is perpendicular to AB at C and NCABP
PQ is perpendicular to AB
P is in the interior of angle ABC
P and Q are on opposite sides of AB
P and Q are on the same side of AB
ABC is isosceles with base BC
AB cuts CD in E
Triangle ABC is congruent to abc
Angle ABC is less than angle DEF
AB and CD are together greater than EF
AB, CD are together greater than EF,GH
ABC and DEF make together two right angles
AB meets CD
AB crosses CD
AB and CD are Tarski parallel
AB and CD are parallel
ABC and DEF are together equal to PQR
ABCD is a parallelogram
ABCD is a square
ABCD is a rectangle
ABCD and abcd are congruent rectangles
ABCD and abcd are equal rectangles
ABCD is a base rectangle of triangle BCE
ABC and abc are equal triangles
ABCD and abcd are equal quadrilaterals
1.2 Common notions
1.3 Axioms of betweenness and congruence
1.4 Postulates
1.5 Axioms for equal figures
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Beeson, M., Narboux, J. & Wiedijk, F. Proof-checking Euclid. Ann Math Artif Intell 85, 213–257 (2019). https://doi.org/10.1007/s10472-018-9606-x
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-018-9606-x