Proof Solver Geometry

Question

Are there any programs that can solve Geometry Problems?

An example of such a problem would be: The centroid of a triangle always divides its medians into two sections with a 1:2 ratio.

While that problem is very easy to solve by hand, I am wondering whether it can be automated in any way. Thanks in advance!

Answer 1

There are several such programs:

• Geometry Expert: http://www.mmrc.iss.ac.cn/gex/
• Java Geometry Expert: https://github.com/yezheng1981/Java-Geometry-Expert
• GCLC: http://poincare.matf.bg.ac.rs/~janicic/gclc/
• GeoTher: https://www-polsys.lip6.fr/~wang/
• Implementation of theorem proving inside GeoGebra (http://www.geogebra.org) and its experimental version GeoGebra Discovery (https://github.com/kovzol/geogebra-discovery)
• Implementation of the area method in Coq: https://github.com/coq-contribs/area-method
• A library of examples with automatic proofs: http://hilbert.mat.uc.pt/TGTP/index.php, http://hilbert.mat.uc.pt/GeoThms/

An overview of the different methods and implementations can be found in our chapter:

• Julien Narboux, Predrag Janičić and Jacques Fleuriot. Computer-assisted Theorem Proving in Synthetic Geometry. Meera Sitharam; Audrey St. John; Jessica Sidman. Handbook of Geometric Constraint Systems Principles, Chapman and Hall/CRC, In press, Discrete Mathematics and Its Applications, 1498738915. ⟨hal-01779452⟩

An overview of the implementation in GeoGebra can be found here:

• Francisco Botana, Markus Hohenwarter, Predrag Janičić, Zoltán Kovács, Ivan Petrović, Tomás Recio and Simon Weitzhofer. Automated Theorem Proving in GeoGebra: Current Achievements. Journal of Automated Reasoning volume 55, pages 39–59 (2015)

and a more recent publication on the same program is here:

• Z. Kovács, Tomás Recio, M. Pilar Vélez: Using Automated Reasoning Tools in GeoGebra in the Teaching and Learning of Proving in Geometry. International Journal of Technology in Mathematic Education. Vol. 25, no. 2. pp. 33-50. 2018. (https://core.ac.uk/download/pdf/188016037.pdf)

or here:

• Francisco Botana, Zoltán Kovács, Tomás Recio: A mechanical geometer. Mathematics in Computer Science, online Nov. 20, 2020. https://doi.org/10.1007/s11786-020-00497-7

Answer 2

With GeoGebra Discovery you can even ask GeoGebra for the relation of the two segments that the centroid produces in the median. The Relation tool "guesses" (but rigorously), and it is 2:1.

First, only numerically:

Then, the symbolic relation is shown:

Finally, if you do not need to "guess" the relation and you know it already, you can use directly the Prove command in GeoGebra (see the bottom of the picture: d=Prove(2k==j) and the answer is true...

The proof is algebraic geometry based, so it is not readable.