Showing Proofs, Assessing Difficulty with GeoGebra Discovery

See [1] for a general description and references. The goal of the current contribution is to present some ongoing work regarding two different, but related, important improvements of GeoGebra Discovery. One, to visualize the different steps that GG Discovery performs with a given geometric statement until it declares its truth (or failure). Two, to test, through different elementary examples, the suitability of an original proposal to evaluate the interest, complexity or difficulty of a given statement. Let us advance that our proposal involves the notion of syzygy of a set of polynomials. The relevance of showing details about each of the steps performed by our automated reasoning algorithms implemented in GG Discovery is quite evident. In fact, as a consequence of the result in [2], describing the formalization of the arithmetization of Euclidean plane geometry, proofs of geometric statements obtained using algebraic geometry algorithms are also valid on the synthetic geometry realm.