Photo by Robin Smidsrød

The summit took place at the Google Headquarters in Mountain View. About 300 mentors worldwide came together to have an unconference about participant-driven topics including student selection process, events, financial questions of open source development, free software in education, and more. Lots of important FOSS took part in the sessions like LibreOffice, The GNU Project, KDE, Gnome, PHPBB, Joomla, Mediawiki, Inkscape and Xapian. GeoGebra was represented by Balázs Koren and Zoltán Kovács from Hungary and Austria.

Mentors from other mathematics related free software were also participating, namely Virgilio Gomez Rubio from the R project and Burcin Erocal from Sage. GeoGebra already has some kind of direct connections to both software, and this meeting was a good time to plan further developments between us.

As usual, Google offered a great hospitality to all participants. California was sunny during these days and it was a perfect time to make excursions to important places of the Silicon Valley and San Francisco as well.

San Francisco and the Golden Gate bridge from North

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.

Ted Kosan, a pioneer of converting computer algebra systems from different languages to others, was one of the first hard worker in this long story. Ted, the lead developer of MathPiper, also did a great effort on converting YaCAS into Java, back in 2008. Because of Reduce has been open sourced since December 2008, and a Java interface (JLisp) was also available for it, Ted decided to try to convert it to JavaScript by using the Google Web Toolkit “Java to JavaScript” compiler (GWT). His adventure was inspired by Gábor Ancsin, a former web designer, who had surprisingly great results in compiling the GeoGebra source code into JavaScript with GWT. Now Ted’s work is a part of Reduce under the name “JSLisp“, and it is also built into GeoGebra as “GGBReduce“. With Ted’s help we have been using the Java version of Reduce by inserting its bytecode stream for the desktop platform, and finally we were also able to put the same bytecode into GeoGebraWeb as a static text. (In fact, Ted was already finished with his prototype back in May 2011.)

To try it out, the user should simply go to the alpha test page of the web platform version of GeoGebra. Then enter

f(x)=x^2*sin(x)

into the input box, press ENTER, and as another command, enter

g(x)=f'(x)

In some seconds (depending on the internet connection and the machine speed, and also the browser) the output g(x)=x^2*cos(x)+2x*sin(x) will be shown in the Algebra View on the left. Google Chrome users may want to try to install GeoGebra from the Google webstore as well to make all of this work offline on their workstation, too.

Yes! No magic any longer – a full featured computer algebra system fits in HTML5 and JavaScript. The next step is to do it faster – to offer convenient use for smartphone users as well. A smartphone can be really slow, and have just limited resources, so this sounds another great challenge.