Theorem proving

Well, I forgot my own introduction in the first post, but maybe it is more important for me that I work in a great team. Balazs already wrote a few words about himself; I am also a mathematics teacher from Hungary, but currently working in Linz, Austria, personally with Markus and his student team.

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.

Related Posts

  • OpenGeoProver debuting 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 […]
  • Be intuitive Days are passing and the summer conference time is getting closer and closer. In two weeks we (Simon and I) will attend EACA 2012 in Spain, and then CADGME 2012 in Serbia. For both we are […]
  • 19 and makes theorems proven Back again in Austria; I've been to two additional conferences during the last two weeks. The first one, in Serbia, was about computer aided mathematics education, and the second one was […]
  • Google Summer of Code Mentor Summit Thanks to Google, this year we had 7 students for the Google Summer of Code program. This was the 3rd year we have been involved after 5 and 7 supported students since 2010. As an official […]
  • GeoGebra MathsJam video See the video from Matt Parker. Matt is the person behind the @standupmaths twitter and he organizes MathsJams. He got an interesting shape from Mike (@mike_geogebra) and now destroys it […]
Posted in Development Tagged with: , , , ,
One comment on “Theorem proving
  1. kovzol says:

    4.1.81.0 is out, so its webstart version can be used at http://www.geogebra.org/webstart/4.2/geogebra-42.jnlp now.

1 Pings/Trackbacks for "Theorem proving"
  1. […] Days are passing and the summer conference time is getting closer and closer. In two weeks we (Simon and I) will attend EACA 2012 in Spain, and then CADGME 2012 in Serbia. For both we are preparing with the new features of GeoGebra, namely the provers. […]

Follow

About GeoGebra

GeoGebra is free and multi-platform dynamic mathematics software for all levels of education that joins geometry, algebra, tables, graphing, statistics and calculus in one easy-to-use package. It has received several educational software awards in Europe and the USA.

Quick Facts

  • Graphics, algebra and tables are connected and fully dynamic
  • Easy-to-use interface, yet many powerful features
  • Authoring tool to create interactive learning materials as web pages
  • Available in many languages for our millions of users around the world
  • Free and open source software
© 2020 International GeoGebra Institute