Discovering geometry via the Discover command in GeoGebra Discovery

We present a new way to discover statements in a planar geometric figure by using GeoGebra Discovery, an experimental version of GeoGebra, the free dynamic mathematics software package. A new command "Discover" (which is also available as a tool) requires an input point of the figure---as output several properties of the figure are communicated by the program. That is, "Discover" reports a list of the observed geometric properties, including point equality, equal long segments, collinearity, concyclicity, parallelism and perpendicularity. All of the obtained statements are checked symbolically: this means that the verification is done with computer algebra means. The obtained properties are also highlighted with colors or dashed lines in the original figure. The discovery process can always be continued by creating new objects and selecting a new target point to discover. We focus on possible uses in a classroom: two basic examples are shown from an Austrian textbook first. Then some more difficult topics are introduced that are usually covered by the secondary school curriculum. As a final example, we consider the discovery of a more advanced theorem, namely, a proposition according to Napoleon. We learn that discovery can lead to unexpected results, but this is an important characteristic of mathematics. In the paper we give some references to related software systems and the applied mathematical background as well.