The portfolio prover in GeoGebra 5

GeoGebra is open source mathematics education software being used in thousands of schools worldwide. Its forthcoming new version 5 will support automatic geometry theorem proving by using various methods which are already well known, but not widely used in an education software. GeoGebra's new embedded prover system chooses one of the available methods and translates the problem constructed by the end user as the input for the selected method, similarly to portfolio solvers. The applicable methods include Wu's method, the Buchberger-Kapur method, the Area method and Recio's exact check method, some of them as embedded algorithms, others as outsourced computations. Since GeoGebra maintains the development in an open-sourced way by collaborating with the OpenGeoProver, Singular and Giac projects as well, further enhancements can be expected by a larger community, including implementing other methods as well.