Sightseeing in Belgrade with Ivan, Gábor and Simon

In Serbia I took part at many nice talks. Maybe the best one, Alfred Wassermann’s new project Sketchometry was a real joy to see. The beta version already recognizes several gestures from the user, both by mouse on a PC or fingers on a tablet. By clicking the + sign on the bottom right, one can start to try this free product on ones own very quickly. Alfred confessed that the first minute was usually a bad experience for some users, but after then the usage became really intuitive and joyful. Anyway, this is really cool, as Gábor (the lead web developer at GeoGebra) mentioned after the introductory talk.

Sketchometry uses JSXGraph as its underlying DGS, and also Darko Drakulic, a contributor of GeoGebra in developing a numerical method for locus line visualization for Google Summer of Code (GSoC) 2011, wrote a nice frontend for it, and gave a talk about his development at the conference. JSXGraph, Wassermann’s main project in the recent years, seems to be a reliable backend for such lightweight GUIs. This is an important issue for smartphones, and at GeoGebra we also plan to reduce the application size as much as possible.

So, I’m back in Austria now, but the life did not stop here, either. Our fresh GSoC 2012 student, Damien Desfontaines did very good improvements on the area method for the OpenGeoProver subsystem. Now his brand new prover is capable of proving 18 theorems or statements from the 44 test cases. This result is remarkable enough if we consider his age (Damien is 19 years old!), the time he spent with the implementation (not more than 3 weeks), and that his work gives far the fastest computation for Desargues’s theorem (142 milliseconds).

Ivan Petrović, PhD student at University of Belgrade

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.

Predrag Janičić, associate professor at University of Belgrade

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.)

The official announcement of our joint work will be on 22 June at the CADGME conference in Novi Sad, Serbia.

Even during the last week there were lots of improvements on the user interface. Now GeoGebra accepts statements in a∥b, c⊥d, E≟F (or E==F) format, and both segments and lines can be used in many proofs. The non-degeneracy conditions are also reported for almost all investigations. These are maybe nuances for a researcher, but important details for most users, for example students: GeoGebra must be intuitive in all subtopics of the mathematics. This is what we try to focus on: to ease understanding of difficult things.

This screenshot shows a non-degeneracy condition for the triangle midsegment theorem: if the points A and B are different, then the theorem is true. Here we used the "parallel" sign to define the statement. The URL shows that Google hosts the web version of GeoGebra, but also an offline version can be installed for the Google Chrome browser.

Both of my kids are also GeoGebra fans, but they are too young to really understand the difference between proof and verification yet. A proof is a theoretical confirmation that a statement (for example, “the bisector lines of a triangle are concurrent”) is always true. A verification is usually an experiment, that the statement is indeed true, by choosing a large set of examples.

GeoGebra is not the first software which provides proving. The first pieces of software were written back in the 1980’s. But oddly enough, many of the first scientific papers were also written by researchers of University of Linz, lead by Professor Bruno Buchberger, founder of the Gröbner basis theory.

Now GeoGebra has several built-in methods to decide if a statement is true in general or not, and one of the used methods is based on Gröbner bases. To avoid heavy computations on a single workstation, we can outsource them to another software, namely Singular, which runs as a web service remotely. On the other hand, we also use a sophisticated method to avoid symbolic computations completely. Professor Tomas Recio, a Spanish expert of algebraic geometry, developed this idea, and Simon Weitzhofer (mentioned in my first post) implemented it in Java recently.

Luckily enough, even other colleagues joined us from different countries. Professor Francisco Botana, a pioneer in open source based mathematics, also from Spain, and Professor Predrag Janicic from University of Belgrade, lead developer of GCLC, offered their help in extending GeoGebra with state-of-the-art methods to provide fast computations. Also Ivan Petrovic, a PhD student of Predrag, works on the open sourced, Java based OpenGeoProver, to enhance it to be an optional prover engine for GeoGebra. We also have a Google Summer of Code 2012 student, Damien Desfontaines from Paris, France, in our group, who helps Ivan to implement the area method, to extend the set of applicable statements for proving. One day maybe we will have readable proofs as well, since the fast algorithms usually don’t give acceptable output for a human. But currently we are really satisfied with some yes/no/unknown result, which should also be used in both experimenting and teaching mathematics.

The basics are working already good, fast and intuitively enough. See this table for an overview: Botana’s method is the Singular based Gröbner basis calculation, pure symbolic method is just dealing with parametric polynomials in Java internally, the OpenGeoProver backend is not listed yet. (The numbers mean milliseconds.) One can also try Recio’s method (and as fallback, the pure symbolic method) in the web version of GeoGebra, or wait for the desktop version (4.1.81.0 should be stable enough, but it is not released yet at the moment), or just watch this YouTube video. For those who are interested in the details, the documentation of the Prove and ProveDetails commands will also help.