The EACA conference has just ended, but the hard development in theorem proving did not stop. Our Serbian contributor Ivan Petrović did very nice improvements on GeoGebra by working hard on the OpenGeoProver (OGP) prototype during the last week. Now the desktop version of GeoGebra has 5 possible ways to prove a statement, and OGP, the latest one, does a really good job.
Now the recent benchmarks show that Ivan’s prover (based on Predrag Janičić‘s GCLC, but fully rewritten in Java) gives the correct answer in 40 out of the 44 test cases, and beats the other provers in the most difficult computations, namely the Desargues’s theorem and the Simson line. In general, it has the second best average in computation time (Recio: 89, OGP: 315, Botana: 540, PureSymbolic: 2091 ms), and the best standard deviation (OGP: 250, Recio: 399, Botana: 2226, PureSymbolic: 9467 ms), which means OGP is the most stable prover engine for GeoGebra at the moment. (The 5th prover is the Auto method: it tries to find the best prover engine by using some heuristics. This is the default in GeoGebra.)