Advertisement

Proof-checking Euclid

  • Michael Beeson
  • Julien Narboux
  • Freek WiedijkEmail author
Open Access
Article

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.

Keywords

Euclid Proof-checking Euclidean geometry HOL light Coq 

Mathematics Subject Classification (2010)

03B30 51M05 

Notes

References

  1. 1.
    Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s Elements. Rev. Symb. Log. 2, 700–768 (2009)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Beeson, M.: A constructive version of Tarski’s geometry. Ann. Pure Appl. Logic 166, 1199–1273 (2015)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Beeson, M.: Constructive geometry and the parallel postulate. Bull. Symb. Log. 22, 1–104 (2016)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Bledsoe, W. W., Loveland, D.: Automated Theorem Proving: After 25 Years. American Mathematical Society, Providence (1983)Google Scholar
  5. 5.
    Boutry, P.: On the Formalization of Foundations of Geometry. PhD thesis, University of Strasbourg (2018)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    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 MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    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)
  9. 9.
    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)Google Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    Braun, G., Narboux, J.: A synthetic proof of Pappus’ theorem in Tarski’s geometry. J. Autom. Reason. 58, 23 (2017)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Chou, S. C.: Mechanical Geometry Theorem Proving. Kluwer Academic Publishers, Norwell (1987)CrossRefGoogle Scholar
  13. 13.
    Chou, S. C.: An introduction to Wu’s method for mechanical theorem proving in geometry. J. Autom. Reason. 4, 237–267 (1988)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. World Scientific (1994)Google Scholar
  15. 15.
    Chou, S. C., Schelter, W. F.: Proving geometry theorems with rewrite rules. J. Autom. Reason. 2, 253–273 (1986)CrossRefGoogle Scholar
  16. 16.
    Corbineau, P.: A declarative language for the Coq proof assistant. In: Types for Proofs and Programs, vol. 4941 of LNCS, Springer (2008)Google Scholar
  17. 17.
    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
  18. 18.
    Euclid: The Thirteen Books of the Elements. Dover, New York (1956). Three volumes. Includes commentary by the translator, Sir Thomas L. HeathzbMATHGoogle Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    Greenberg, M. J.: Euclidean and non-Euclidean Geometries: Development and History, 4th edn. W. H. Freeman, New York (2008)zbMATHGoogle Scholar
  22. 22.
    Gries, C.: Axiomes de continuité en géométrie neutre : Une étude méchanisée en Coq. University of Strasbourg, internship report (2017)Google Scholar
  23. 23.
    Gupta, H. N.: Contributions to the Axiomatic Foundations of Geometry. PhD Thesis, University of California, Berkeley (1965)Google Scholar
  24. 24.
    Hartshorne, R.: Geometry: Euclid and Beyond. Springer, New York (2000)CrossRefGoogle Scholar
  25. 25.
    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)Google Scholar
  26. 26.
    Kapur, D.: A refutational approach to geometry theorem proving. J. Artif. Intell. 37, 61–93 (1988)MathSciNetCrossRefGoogle Scholar
  27. 27.
    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)Google Scholar
  28. 28.
    Manders, K.: The Euclidean diagram (1995). In: The Philosophy of Mathematical Practice, Paolo Mancosu. Oxford University Press ed. (2011)Google Scholar
  29. 29.
    Miller, N.: A Diagrammatic Formal System for Euclidean Geometry. PhD thesis, Cornell University (2001)Google Scholar
  30. 30.
    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: ocm71947628Google Scholar
  31. 31.
    Miller, N.: On the inconsistency of Mumma’s Eu. Notre Dame Journal of Formal Logic 53, 27–52 (2012)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Mollerup, J.: Die Beweise der ebenen Geometrie ohne Benutzung der Gleichheit und Ungleichheit der Winkel. Math. Ann. 58, 479–496 (1904)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Mumma, J.: Proofs, pictures, and Euclid. Synthese 175, 255–287 (2010)MathSciNetCrossRefGoogle Scholar
  34. 34.
    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)Google Scholar
  35. 35.
    Pasch, M.: Vorlesung über Neuere Geometrie. Teubner, Leipzig (1882)zbMATHGoogle Scholar
  36. 36.
    Peano, G.: Principii de Geometria. Fratelli Bocca, Torino (1889)zbMATHGoogle Scholar
  37. 37.
    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)Google Scholar
  38. 38.
    Proclus: A Commentary on the First Book of Euclid. Princeton University Press, Princeton (1970)zbMATHGoogle Scholar
  39. 39.
    Quaife, A.: Automated development of Tarski’s geometry. J. Autom. Reason. 5, 97–118 (1989)MathSciNetCrossRefGoogle Scholar
  40. 40.
    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 BeesonGoogle Scholar
  41. 41.
    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)MathSciNetzbMATHGoogle Scholar
  42. 42.
    Strommer, J.: Über die Kreisaxiome. Period. Math. Hung. 4, 3–16 (1973)CrossRefGoogle Scholar
  43. 43.
    Tarski, A., Givant, S.: Tarski’s system of geometry. Bull. Symb. Log. 5, 175–214 (1999)MathSciNetCrossRefGoogle Scholar
  44. 44.
    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)Google Scholar
  45. 45.
    Wu, W.-T.: On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sinica 21, reprinted in [4] (1978)MathSciNetGoogle Scholar
  46. 46.
    Wu, W.-T.: Mechanical Theorem Proving in Geometries: Basic Principles. Springer, Wien/ New York (1994)CrossRefGoogle Scholar

Copyright information

© The Author(s) 2019

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.

Authors and Affiliations

  1. 1.Department of MathematicsSan Jose State UniversityAptosUSA
  2. 2.ICube, UMR 7357 CNRSUniversity of StrasbourgIllkirchFrance
  3. 3.Institute for Computing and Information SciencesRadboud UniversityNijmegenThe Netherlands

Personalised recommendations